feat: Hoeffding's lemma

[tukamilano]

Formalize Hoeffding's lemma using the property of cumulant.

Co-authored-by: Yuma Mizuno [email protected]

[github-actions[bot]]

PR summary ca9bfada13

Import changes exceeding 2%

%	File
+5.46%	Mathlib.Probability.Moments.Basic

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Probability.Moments.Basic	2088	2202	+114 (+5.46%)
Mathlib.Probability.Moments.MGFAnalytic	2250	2258	+8 (+0.36%)

Import changes for all files

Files	Import difference
Mathlib.Probability.Moments.SubGaussian	1
Mathlib.Probability.Moments.ComplexMGF Mathlib.Probability.Moments.MGFAnalytic	8
Mathlib.Probability.Distributions.Gaussian	9
Mathlib.Probability.Moments.Basic	114
Mathlib.Probability.Hoeffding (new file)	2259

---

Declarations diff

+ cgf_deriv_one + cgf_deriv_two + cgf_zero_deriv + extracted_1 + hoeffding + hoeffding_nonneg + integrableExpSet_eq_univ_of_mem_Icc + integrable_expt_bound + integral_tilted' + tilt_var_bound

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

[tukamilano]

Thanks for the PR! It will require some changes because apparently you missed that we have definitions for the moment and cumulant generating functions. See ProbabilityTheory.mgf. You should use those definitions, and move their properties to the Moments file.

I got it. I'll move the lemmas about the first and derivatives of mgf and cgf to Probability/Moments file.

[tukamilano]

Thank you for writing many comments. It will take some time to fix everything, so please wait a moment

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib4#20151~~ By Dependent Issues (🤖). Happy coding!

[RemyDegenne]

I merged master but did not make other changes to reuse the newly merged results from #20151 . If you don't mind I'll make another commit with those changes later today.

[YaelDillies]

~~Sorry if this was already discussed above, but can you generalise from bounded random variables to subgaussian random variables?~~ Got confused

[tukamilano]

Thank you for these comments.

[mathlib4-merge-conflict-bot]

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

[YaelDillies]

Hoeffding's lemma was merged in #26744. Thank you for the PR regardless and feel free to open further PRs from your project!