Skip to content

[Merged by Bors] - feat: convergence in distribution and continuous mapping theorem#30540

Closed
RemyDegenne wants to merge 9 commits intoleanprover-community:masterfrom
RemyDegenne:RD_continuousMapping
Closed

[Merged by Bors] - feat: convergence in distribution and continuous mapping theorem#30540
RemyDegenne wants to merge 9 commits intoleanprover-community:masterfrom
RemyDegenne:RD_continuousMapping

Conversation

@RemyDegenne
Copy link
Copy Markdown
Contributor

@RemyDegenne RemyDegenne commented Oct 14, 2025 •
edited
Loading

  • Define convergence in distribution of random variables: this is the weak convergence of their laws.
  • Prove the continuous mapping theorem for convergence in distribution and continuous functions.

Open in Gitpod

@RemyDegenne RemyDegenne mentioned this pull request Oct 14, 2025
Closed
6 tasks
@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 14, 2025 •
edited
Loading

PR summary 1d861322df

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.MeasureTheory.Function.ConvergenceInDistribution (new file) 2279

Declarations diff

+ TendstoInDistribution
+ TendstoInDistribution.continuous_comp
+ tendstoInDistribution_const
+ tendstoInDistribution_unique

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

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

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

No changes to technical debt.

You can run this locally as

./scripts/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).

@github-actions github-actions bot added the t-measure-probability Measure theory / Probability theory label Oct 14, 2025
sgouezel
sgouezel reviewed Oct 16, 2025
View reviewed changes
@sgouezel sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 16, 2025
@RemyDegenne RemyDegenne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 21, 2025
EtienneC30
EtienneC30 reviewed Oct 25, 2025
View reviewed changes
Copy link
Copy Markdown
Member

@EtienneC30 EtienneC30 left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice!
maintainer delegate

@github-actions
Copy link
Copy Markdown

github-actions bot commented Oct 25, 2025

🚀 Pull request has been placed on the maintainer queue by EtienneC30.

@ghost ghost added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Oct 25, 2025
sgouezel
sgouezel reviewed Oct 27, 2025
View reviewed changes
@sgouezel sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. and removed maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. labels Oct 27, 2025
@RemyDegenne RemyDegenne removed the awaiting-author A reviewer has asked the author a question or requested changes. label Oct 28, 2025
@sgouezel
Copy link
Copy Markdown
Contributor

sgouezel commented Oct 29, 2025

bors r+
Thanks!

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Oct 29, 2025
mathlib-bors bot pushed a commit that referenced this pull request Oct 29, 2025
@RemyDegenne
feat: convergence in distribution and continuous mapping theorem (#30540
942e977 
)

- Define convergence in distribution of random variables: this is the weak convergence of their laws.
- Prove the continuous mapping theorem for convergence in distribution and continuous functions.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Oct 29, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: convergence in distribution and continuous mapping theorem [Merged by Bors] - feat: convergence in distribution and continuous mapping theorem Oct 29, 2025
@mathlib-bors mathlib-bors bot closed this Oct 29, 2025
BeibeiX0 pushed a commit to BeibeiX0/mathlib4 that referenced this pull request Nov 7, 2025
@RemyDegenne @BeibeiX0
feat: convergence in distribution and continuous mapping theorem (lea…
3f24961 
…nprover-community#30540)

- Define convergence in distribution of random variables: this is the weak convergence of their laws.
- Prove the continuous mapping theorem for convergence in distribution and continuous functions.

Co-authored-by: Remy Degenne <remydegenne@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@sgouezel sgouezel sgouezel left review comments

@EtienneC30 EtienneC30 EtienneC30 left review comments

Assignees

No one assigned

Labels

ready-to-merge This PR has been sent to bors. t-measure-probability Measure theory / Probability theory

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@RemyDegenne @sgouezel @EtienneC30