[Merged by Bors] - feat(Probability/Moments): add lemmas about moment generating functions #19886

Vilin97 · 2024-12-11T08:23:00Z

Add mgf_ident_distrib, mgf_sum_iid.
These are some of the supporting lemmas we have proved on our way to formalizing the central limit theorem.

Co-authored-by: Siyuan Ge jamesgsy@uw.edu

github-actions · 2024-12-11T08:23:55Z

PR summary c767f0b86e

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Probability.Moments	1948	1952	+4 (+0.21%)

Import changes for all files

Files	Import difference
`Mathlib.Probability.Moments`	4

Declarations diff

+ mgf_congr_of_identDistrib
+ mgf_sum_of_identDistrib

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

Mathlib/Probability/Moments.lean

sgouezel

I didn't ask that you should remove the result for the Gaussian, only that you move it to the file about the Gaussian. I think it's definitely a good result to have!

Mathlib/Probability/Moments.lean

Vilin97 · 2024-12-20T14:43:22Z

@sgouezel , I just moved the gaussian mgf lemma in another PR: #19896.

I addressed all your comments.

Vilin97 · 2024-12-23T21:01:48Z

@sgouezel , friendly ping. Thank you for your attention!

YaelDillies

Thank you for the PR! Should be easy to get in

Mathlib/Probability/Moments.lean

Vilin97 · 2024-12-30T19:55:39Z

Thanks, @YaelDillies. I applied your suggestions.

YaelDillies

Thank you for implementing the changes! Here are a few more suggestions

Mathlib/Probability/Moments.lean

YaelDillies

Thanks!

maintainer delegate

Mathlib/Probability/Moments.lean

github-actions · 2024-12-31T07:52:53Z

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

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

RemyDegenne · 2025-01-03T07:57:23Z

Thanks!
bors r+

RemyDegenne · 2025-01-04T08:30:05Z

It looks like bors did not react? Let's try again.
bors r+

…ns (#19886) Add `mgf_ident_distrib`, `mgf_sum_iid`. These are some of the supporting lemmas we have proved on our way to formalizing the central limit theorem. Co-authored-by: Siyuan Ge <jamesgsy@uw.edu>

mathlib-bors · 2025-01-04T08:39:14Z

Pull request successfully merged into master.

Build succeeded:

* origin/master: (133 commits) chore(1000): remove nonexistent fields (#20493) chore(CategoryTheory/Adjunction.Basic, CategoryTheory/Equivalence): change definition of `Adjunction.comp` and `Equivalence.trans` (#20490) feat(Asymptotics): add `Asymptotics.*.*Prod` lemmas (#20458) feat: a conditional kernel is almost everywhere a probability measure (#20430) feat: if `f` is a measurable group hom, then every point has a neighborhood `s` such that `f '' s` is bounded (#20304) feat: `Ico`, `Ioc`, and `Ioo` are not closed or compact (#20479) chore: drop redundant hypothesis in `Module.Dual.eq_of_preReflection_mapsTo` (#20492) feat(FaaDiBruno): derive `DecidableEq` (#20482) chore(SetTheory/Ordinal/Basic): `{x // x < y}` → `Iio y` (#20413) chore: generalize `FormalMultilinearSeries.ofScalars_norm` to `Seminormed` (#20351) chore(MvPolynomial/Localization): golf using TensorProduct (#20309) chore(Combinatorics/Enumerative/Partition): auto-derive DecidableEq (#20277) chore(CategoryTheory): make relevant parameters explicit in `Arrow.homMk`. (#20259) feat: add `IsStarNormal (↑x⁻¹ : R)` instance for `x : Rˣ` (#20091) fix: Stop cancelling builds of master (#20435) chore: update Mathlib dependencies 2025-01-05 (#20485) feat(SetTheory/Cardinal/Arithmetic): miscellaneous cardinality lemmas (#18933) chore: bump toolchain to v4.16.0-rc1, and merge bump/v4.16.0 (#20464) chore: bot validates lean-toolchain on bump/v4.X.0 branches (#20478) feat: shorthand lemmas for the L1 norm (#20383) chore: remove unnecessary adaptation notes (#20467) chore(Algebra/Category/MonCat/Colimits): remove smallness condition (#20473) chore(SetTheory/Ordinal/Arithmetic): `IsLeftCancelAdd Ordinal` (#19888) feat(Algebra): more on `OrthogonalIdempotents` (#18195) feat(Radical): `(radical a).natDegree ≤ a.natDegree` (#20468) feat(Polynomial): `(a^n)' = 0` iff `a' = 0` when `n` doesn't divide the characteristic (#20190) feat(Algebra/Lie): add Lie's theorem (#13480) chore(RingTheory/Generators): make algebra instance a def (#14265) feat(Topology/Group): Lemmas about profinite group (#20282) feat: the empty set is a topological basis iff the space is empty (#20441) chore: make uniqueness of conditionally complete linearly ordered archimedean fields independent of the construction of `Real` (#20242) chore: `inherit_doc`s for notations (#20376) chore: split AEEqOfIntegral into two files, one for each integral type (#20405) chore: split Kernel/MeasurableIntegral (#20427) feat(MeasureTheory/Group/Measure): add ContinuousMulEquiv.isHaarMeasure_map (#20469) fix(Mathlib.Tactic.CC.Datatypes): `cc` raises panic (#20422) feat(Probability/Moments): add lemmas about moment generating functions (#19886) feat(Algebra/Order/AddGroupWithTop): lemmas about LinearOrderedAddCommGroupWithTop (#18954) chore: bump toolchain to v4.15.0 (#20461) chore: update Mathlib dependencies 2025-01-04 (#20463) fix: make `Prod` projection delaborators respond to options, add option to disable (#20455) chore(Algebra): Improve attribute generation (#20451) feat(Polynomial): `(C a * p).degree = p.degree` if `a * p.leadingCoeff ≠ 0` (#20446) feat: add `ENNReal.finStronglyMeasurable_of_measurable` (#20404) doc(Algebra/Lie/Weights/Basic): fix typo (#20450) chore(1000): remove `identifiers` (#20445) feat: add sumPiEquivProdPi and piUnique (#20195) feat: add fst_compProd_apply (#20429) chore: use unsigned measures for Lebesgue decomposition (#20400) feat: Two lemmas on divisibility and coprimality of `expand` (#20143) ...

Vilin97 added 5 commits December 8, 2024 00:26

Add mgf_smul_left.

1384913

Reorder the variables.

2e46ac1

Add three lemmas about mgf.

a076818

Rename lemma.

cf4f4fa

Fix indentation.

c5eac66

github-actions bot added new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! large-import Automatically added label for PRs with a significant increase in transitive imports labels Dec 11, 2024

github-actions bot added the t-measure-probability Measure theory / Probability theory label Dec 11, 2024

Vilin97 added RFC Request for comment and removed t-measure-probability Measure theory / Probability theory large-import Automatically added label for PRs with a significant increase in transitive imports labels Dec 11, 2024

sgouezel reviewed Dec 11, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

sgouezel added awaiting-author A reviewer has asked the author a question or requested changes. t-measure-probability Measure theory / Probability theory and removed RFC Request for comment labels Dec 11, 2024

Fix indentation and remove mgf_gaussian.

eafe8b9

Vilin97 commented Dec 11, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Show resolved Hide resolved

Vilin97 changed the title ~~feat(Probability/Moments): add three lemmas about moment generating functions~~ feat(Probability/Moments): add lemmas about moment generating functions Dec 11, 2024

Merge remote-tracking branch 'origin/master' into vilin97-mgf

c423f2d

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 11, 2024

sgouezel reviewed Dec 11, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

sgouezel added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 12, 2024

Make mgf_sum_iid more general.

3eee7c4

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 20, 2024

Vilin97 requested a review from sgouezel December 22, 2024 18:23

YaelDillies reviewed Dec 28, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 28, 2024

Fix theorem names.

bfa2de6

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024

Vilin97 requested a review from YaelDillies December 30, 2024 19:55

YaelDillies reviewed Dec 30, 2024

View reviewed changes

YaelDillies added the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024

Apply suggestions.

35dfc75

Vilin97 removed the awaiting-author A reviewer has asked the author a question or requested changes. label Dec 30, 2024

YaelDillies reviewed Dec 30, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Outdated Show resolved Hide resolved

Apply suggestions.

9d4de64

YaelDillies approved these changes Dec 31, 2024

View reviewed changes

Mathlib/Probability/Moments.lean Show resolved Hide resolved

github-actions bot added the maintainer-merge A reviewer has approved the changed; awaiting maintainer approval. label Dec 31, 2024

Add issue number.

c767f0b

Co-authored-by: Kyle Miller <kmill31415@gmail.com>

leanprover-community-mathlib4-bot added the ready-to-merge This PR has been sent to bors. label Jan 3, 2025

mathlib-bors bot changed the title ~~feat(Probability/Moments): add lemmas about moment generating functions~~ [Merged by Bors] - feat(Probability/Moments): add lemmas about moment generating functions Jan 4, 2025

mathlib-bors bot closed this Jan 4, 2025

mathlib-bors bot deleted the vilin97-mgf branch January 4, 2025 08:39

[Merged by Bors] - feat(Probability/Moments): add lemmas about moment generating functions #19886

[Merged by Bors] - feat(Probability/Moments): add lemmas about moment generating functions #19886

Uh oh!

Conversation

Vilin97 commented Dec 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions bot commented Dec 11, 2024 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

PR summary c767f0b86e

Import changes for modified files

Declarations diff

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

sgouezel left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vilin97 commented Dec 20, 2024

Uh oh!

Vilin97 commented Dec 23, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Vilin97 commented Dec 30, 2024

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

YaelDillies left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

github-actions bot commented Dec 31, 2024

Uh oh!

RemyDegenne commented Jan 3, 2025

Uh oh!

RemyDegenne commented Jan 4, 2025

Uh oh!

mathlib-bors bot commented Jan 4, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

7 participants

Vilin97 commented Dec 11, 2024 •

edited

Loading

github-actions bot commented Dec 11, 2024 •

edited

Loading