Skip to content

feat(Probability): multivariate CLT (and Cramèr-Wold)#37279

Open
imalinowskip wants to merge 18 commits intoleanprover-community:masterfrom
imalinowskip:ivo-clt-multivariate
Open

feat(Probability): multivariate CLT (and Cramèr-Wold)#37279
imalinowskip wants to merge 18 commits intoleanprover-community:masterfrom
imalinowskip:ivo-clt-multivariate

Conversation

@imalinowskip
Copy link
Copy Markdown

@imalinowskip imalinowskip commented Mar 27, 2026

Depends on #36208

Open in Gitpod

@github-actions github-actions bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label Mar 27, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@github-actions github-actions bot added the large-import Automatically added label for PRs with a significant increase in transitive imports label Mar 27, 2026
@github-actions
Copy link
Copy Markdown

github-actions bot commented Mar 27, 2026 •
edited
Loading

PR summary 8f1377de1f

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.Probability.CramerWold (new file) 2660
Mathlib.Probability.MultivariateCentralLimitTheorem (new file) 2725

Declarations diff

+ aemeasurable_dotProduct
+ aemeasurable_dotProduct'
+ bounded_continuous_exp_inner_mul_I
+ bounded_continuous_exp_ofReal_mul_I
+ bounded_continuous_exp_ofReal_mul_I_eq_cexp
+ central_limit_multivariate
+ cexp_bound_exact
+ charFun_tendsto_if_inner_tendsto
+ complex_dist_zero_eq_abs
+ complex_dist_zero_eq_abs'
+ continuous_exp_ofReal_mul_I
+ cramerWold
+ isProbabilityMeasure_standardGaussianRealMultivariate
+ measurable_dotProduct
+ measurable_dotProduct'
+ rv_tendsto_if_charFun_tendsto
+ standardGaussianRealMultivariate
+ tendstoInDistribution_sqrt_inv_mul_sum

You can run this locally as follows 
## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

Increase in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
635 2 erw

Current commit 8d9d3b7f9b
Reference commit 8f1377de1f

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@RemyDegenne RemyDegenne added the t-measure-probability Measure theory / Probability theory label Mar 27, 2026
@mathlib-merge-conflicts mathlib-merge-conflicts bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Mar 28, 2026
@mathlib-merge-conflicts
Copy link
Copy Markdown

mathlib-merge-conflicts bot commented Mar 28, 2026

This pull request has conflicts, please merge master and resolve them.

@imalinowskip imalinowskip changed the title WIP: multivariate CLT and Cramer-Wold feat(Probability): multivariate CLT (and Cramèr-Wold) Mar 28, 2026
@github-actions github-actions bot removed merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) large-import Automatically added label for PRs with a significant increase in transitive imports labels Mar 28, 2026
@imalinowskip imalinowskip force-pushed the ivo-clt-multivariate branch from a0fb415 to f2a2e15 Compare March 28, 2026 20:17
@imalinowskip imalinowskip force-pushed the ivo-clt-multivariate branch from a080bbf to 4e4825b Compare March 29, 2026 15:31
@imalinowskip imalinowskip force-pushed the ivo-clt-multivariate branch from 2e90c3e to f829434 Compare March 29, 2026 19:16
@imalinowskip imalinowskip marked this pull request as ready for review April 3, 2026 19:06
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

@RemyDegenne RemyDegenne

Labels

new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@imalinowskip @RemyDegenne