Mathlib.Probability
Probability helpers staged for Mathlib: Bernoulli and signed two-point laws, Gaussian calculations, convergence in distribution, kernel composition, finite marked Poisson experiments, and Stein-method CLT tools.
CertifiedFiniteMarkovExpectation 102 core · 81 supporting · 7 submodules Exact rational interval arithmetic for finite-state Markov kernels, certified normal-CDF transition probabilities, stationary-reward enclosures, and strict policy comparisons. ConvergingTogether 4 core · 4 supporting · 2 submodules This namespace collects the reusable pieces for the converging-together theorem. FiniteMarkedPoissonPartition 2 to review
48 core · 61 supporting · 6 submodules Finite marked Poisson experiment infrastructure: finite samples, exact partition splitting, canonical mark-ordered superposition, retained independent prefixes, depoissonization bridges, and the finite-measure KL identity. Kernel 10 core · 9 supporting · 4 submodules Kernel-measure probability helpers: graph-map product identities and composition-product assembly lemmas for conditional-law arguments. PoissonAddOnePoincare 13 core · 18 supporting · 4 submodules Poisson concentration infrastructure: scalar add-one Poincaré variance bounds, countable-series and L² closure tools, and tensorization over finite independent Poisson products. SteinMethod 15 core · 31 supporting · 6 submodules Stein-method normal-approximation helpers: Stein equation solutions, uniform bounds, local-dependence estimates, and dependency-graph CLTs.
StdNormalCDF 5 core · 14 supporting This file provides self-contained one-dimensional standard-normal analysis. ★ stdNormalCDF_continuous★ probit_stdNormalCDF
Standard normal CDF and probit
This file provides self-contained one-dimensional standard-normal analysis. It
names the standard-normal density stdNormalPDF, CDF stdNormalCDF, and
probit inverse probit. It proves CDF symmetry, monotonicity, endpoint
limits, continuity, strict monotonicity, positivity, the strict upper bound by
one, and the two exact inversion identities stdNormalCDF_probit and
probit_stdNormalCDF.
def stdNormalPDF reviewed
⚑ flagged
Causalean.Mathlib
For each real number , the standard-normal density at is .
Definition (Lean source)
def stdNormalCDF reviewed
⚑ flagged
Causalean.Mathlib
For each real number , the standard-normal cumulative distribution function at is the probability that a mean-zero, variance-one normal random variable is at most .
Definition (Lean source)
lemma stdNormalCDF_continuous reviewed
⚑ flagged
Causalean.Mathlib
The standard normal CDF Φ is continuous: the standard normal has no atoms.
Formal statement
conclusion
Proof (Lean source)
@[fun_prop]
lemma stdNormalCDF_continuous : Continuous stdNormalCDF := by
haveI : NullSingletonClass (gaussianReal 0 1) :=
nullSingletonClass_gaussianReal (v := 1) one_ne_zero
exact cdf_continuous_of_noAtoms (gaussianReal 0 1)
def probit reviewed
⚑ flagged
Causalean.Mathlib
For each real number , the probit at is the infimum of the real numbers for which the standard-normal cumulative distribution function at is at least .
Definition (Lean source)
lemma probit_stdNormalCDF reviewed
⚑ flagged
Causalean.Mathlib
For any real score x, applying the probit transform to Φ(x) recovers x: the probit function Φ⁻¹ is a left inverse of the standard normal CDF Φ.
Formal statement
Proof (Lean source)
lemma probit_stdNormalCDF (x : ℝ) : probit (stdNormalCDF x) = x := by
rw [probit]
have hset : {y : ℝ | stdNormalCDF x ≤ stdNormalCDF y} = Ici x := by
ext y
exact stdNormalCDF_strictMono.le_iff_le
rw [hset, csInf_Ici]
14 supporting declarations (lemmas, instances)
-
stdNormalPDF_deflemma — The named standard-normal density is Mathlib's real Gaussian density with mean zero and variance one.Proof (Lean source)
-
stdNormalCDF_deflemma — The named standard-normal CDF is Mathlib's CDF for the standard real Gaussian law.Proof (Lean source)
-
stdNormalCDF_monotonelemma — Φ is monotone (inherited from the StieltjesFunction structure of cdf).conclusionProof (Lean source)
lemma stdNormalCDF_monotone : Monotone stdNormalCDF := by intro a b hab exact (monotone_cdf (gaussianReal 0 1)) hab -
stdNormalCDF_nonneglemma — Φ(x) ∈ [0,1].Proof (Lean source)
lemma stdNormalCDF_nonneg (x : ℝ) : 0 ≤ stdNormalCDF x := cdf_nonneg _ x -
stdNormalCDF_le_onelemma — The standard-normal CDF is at most one at every real point.Proof (Lean source)
lemma stdNormalCDF_le_one (x : ℝ) : stdNormalCDF x ≤ 1 := cdf_le_one _ x -
cdf_neg_of_map_neglemma — The CDF of an atomless probability measure invariant under reflection is symmetric.hypothesesProof (Lean source)
lemma cdf_neg_of_map_neg {μ : Measure ℝ} [IsProbabilityMeasure μ] [NullSingletonClass μ] (hmap : μ.map (fun x : ℝ => -x) = μ) (t : ℝ) : cdf μ (-t) = 1 - cdf μ t := by have hreal : ∀ s : ℝ, cdf μ s = μ.real (Iic s) := by intro s; exact cdf_eq_real _ s -- Reflection symmetry of the law: `Φ(-t) = μ.real (Ici t)`. have hpre : (fun x : ℝ => -x) ⁻¹' Iic (-t) = Ici t := by ext x; simp have step1 : cdf μ (-t) = μ.real (Ici t) := by rw [hreal (-t)] conv_lhs => rw [← hmap] rw [MeasureTheory.map_measureReal_apply measurable_neg measurableSet_Iic, hpre] rw [step1, ← Set.compl_Iio, MeasureTheory.measureReal_compl measurableSet_Iio, MeasureTheory.measureReal_congr MeasureTheory.Iio_ae_eq_Iic, MeasureTheory.probReal_univ, hreal t] -
stdNormalCDF_neglemma — Symmetry of the standard normal CDF: Φ(−t) = 1 − Φ(t), from the reflection symmetry of the Gaussian law and its atomlessness.Proof (Lean source)
lemma stdNormalCDF_neg (t : ℝ) : stdNormalCDF (-t) = 1 - stdNormalCDF t := by have hmap : (gaussianReal 0 1).map (fun x : ℝ => -x) = gaussianReal 0 1 := by rw [gaussianReal_map_neg, neg_zero] haveI : NullSingletonClass (gaussianReal 0 1) := nullSingletonClass_gaussianReal (v := 1) one_ne_zero exact cdf_neg_of_map_neg hmap t -
stdNormalCDF_tendsto_atBotlemma — Φ → 0 at -∞.conclusionProof (Lean source)
-
stdNormalCDF_tendsto_atToplemma — Φ → 1 at +∞.conclusionProof (Lean source)
-
cdf_continuous_of_noAtomslemma — The CDF of an atomless real probability measure is continuous.Proof (Lean source)
@[fun_prop] lemma cdf_continuous_of_noAtoms (μ : Measure ℝ) [IsProbabilityMeasure μ] [NullSingletonClass μ] : Continuous (cdf μ) := by set f := cdf μ with hf refine continuous_iff_continuousAt.2 fun x => ?_ refine (f.mono.continuousAt_iff_leftLim_eq_rightLim).2 ?_ rw [f.rightLim_eq x] have hjump : f.measure {x} = ofReal (f x - Function.leftLim (f : ℝ → ℝ) x) := f.measure_singleton x have hμx : f.measure {x} = 0 := by rw [hf, ProbabilityTheory.measure_cdf] exact measure_singleton x rw [hμx, eq_comm, ENNReal.ofReal_eq_zero] at hjump have hle : Function.leftLim (f : ℝ → ℝ) x ≤ f x := f.mono.leftLim_le (le_refl x) linarith [hjump, hle] -
stdNormalCDF_strictMonolemma — Φ is strictly monotone: the standard normal has full support.conclusionProof (Lean source)
lemma stdNormalCDF_strictMono : StrictMono stdNormalCDF := by intro a b hab have hfi : IntervalIntegrable (gaussianPDFReal 0 1) volume a b := (integrable_gaussianPDFReal 0 1).intervalIntegrable have hposInt : 0 < ∫ x in a..b, gaussianPDFReal 0 1 x := intervalIntegral.intervalIntegral_pos_of_pos hfi (fun x => gaussianPDFReal_pos 0 1 x one_ne_zero) hab have hposSet : 0 < ∫ x in Ioc a b, gaussianPDFReal 0 1 x := by simpa [intervalIntegral.integral_of_le hab.le] using hposInt have hμpos : 0 < (gaussianReal 0 1) (Ioc a b) := by rw [gaussianReal_apply_eq_integral (μ := 0) (v := 1) one_ne_zero] exact ENNReal.ofReal_pos.mpr hposSet have hmeasure : (gaussianReal 0 1) (Ioc a b) = ofReal (cdf (gaussianReal 0 1) b - cdf (gaussianReal 0 1) a) := by calc (gaussianReal 0 1) (Ioc a b) = (cdf (gaussianReal 0 1)).measure (Ioc a b) := by rw [ProbabilityTheory.measure_cdf (gaussianReal 0 1)] _ = ofReal (cdf (gaussianReal 0 1) b - cdf (gaussianReal 0 1) a) := by rw [StieltjesFunction.measure_Ioc] have hdiff : 0 < cdf (gaussianReal 0 1) b - cdf (gaussianReal 0 1) a := by exact ENNReal.ofReal_pos.mp (by simpa [hmeasure] using hμpos) exact sub_pos.mp hdiff -
stdNormalCDF_poslemma — 0 < Φ(x) for every real x (full support of the Gaussian).Proof (Lean source)
lemma stdNormalCDF_pos (x : ℝ) : 0 < stdNormalCDF x := by have hlt := stdNormalCDF_strictMono (by linarith : x - 1 < x) have hnon := stdNormalCDF_nonneg (x - 1) linarith -
stdNormalCDF_lt_onelemma — Φ(x) < 1 for every real x.Proof (Lean source)
lemma stdNormalCDF_lt_one (x : ℝ) : stdNormalCDF x < 1 := by have hlt := stdNormalCDF_strictMono (by linarith : x < x + 1) have hle := stdNormalCDF_le_one (x + 1) linarith -
stdNormalCDF_probitlemma — Φ(Φ⁻¹(p)) = p for p ∈ (0,1) (exact inversion, using continuity + strict monotonicity).Proof (Lean source)
lemma stdNormalCDF_probit {p : ℝ} (h0 : 0 < p) (h1 : p < 1) : stdNormalCDF (probit p) = p := by obtain ⟨a, ha⟩ := Filter.eventually_atBot.mp (stdNormalCDF_tendsto_atBot.eventually_lt_const h0) obtain ⟨b, hb⟩ := Filter.eventually_atTop.mp (stdNormalCDF_tendsto_atTop.eventually_const_lt h1) have hab : a < b := by by_contra hnot have hba : b ≤ a := le_of_not_gt hnot have hmono := stdNormalCDF_monotone hba linarith [ha a le_rfl, hb b le_rfl, hmono] have hpIcc : p ∈ Icc (stdNormalCDF a) (stdNormalCDF b) := ⟨(ha a le_rfl).le, (hb b le_rfl).le⟩ have hpimage : p ∈ stdNormalCDF '' Icc a b := intermediate_value_Icc hab.le stdNormalCDF_continuous.continuousOn hpIcc rcases hpimage with ⟨x, _hxI, hxeq⟩ have hset : {y : ℝ | p ≤ stdNormalCDF y} = Ici x := by ext y change p ≤ stdNormalCDF y ↔ x ≤ y rw [← hxeq] exact stdNormalCDF_strictMono.le_iff_le have hprobit : probit p = x := by rw [probit, hset, csInf_Ici] rw [hprobit, hxeq]
BernoulliMeasure 5 core · 17 supporting This file defines the Bernoulli law on the real line, supported on 0 and 1, and proves its basic probability, support, integral, absolute-continuity, and KL-divergence facts. ★ bernoulliLaw_klDiv_toReal★ bernoulliLaw_klDiv_le_four_sq_sub
Bernoulli measures
This file defines the Bernoulli law on the real line, supported on 0 and
1, and proves its basic probability, support, integral, absolute-continuity,
and KL-divergence facts. It also provides the corresponding Bool-valued law and
its measurability, probability, integral, bind, and map formulas.
def bernoulliLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability
For any real number interpreted as a success parameter, the real-valued Bernoulli measure assigns mass to and mass to .
lemma bernoulliLaw_klDiv_toReal reviewed
⚑ flagged
Causalean.Mathlib.Probability
Let be a Bernoulli success probability with , and let be a reference success probability with . Then the Kullback–Leibler divergence from the Bernoulli() law to the Bernoulli() law equals , the usual two-point KL formula: a success contribution plus a failure contribution.
Formal statement
hypotheses
p q :
ℝ
hp0 :
0 ≤ p
hp1 :
p ≤ 1
hq0 :
0 < q
hq1 :
q < 1
conclusion
Proof (Lean source)
lemma bernoulliLaw_klDiv_toReal {p q : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1)
(hq0 : 0 < q) (hq1 : q < 1) :
(klDiv (bernoulliLaw p) (bernoulliLaw q)).toReal
= p * log (p / q) + (1 - p) * log ((1 - p) / (1 - q)) := by
classical
haveI hp_prob : IsProbabilityMeasure (bernoulliLaw p) :=
bernoulliLaw_isProbabilityMeasure hp0 hp1
haveI hq_prob : IsProbabilityMeasure (bernoulliLaw q) :=
bernoulliLaw_isProbabilityMeasure hq0.le hq1.le
let g : ℝ → ENNReal :=
fun x =>
if x = 1 then ofReal (p / q)
else ofReal ((1 - p) / (1 - q))
have hg : Measurable g := by
dsimp [g]
exact Measurable.ite (measurableSet_singleton (1 : ℝ)) measurable_const measurable_const
have hq_ne0 : ofReal q ≠ 0 := by
intro h
have hle := ENNReal.ofReal_eq_zero.mp h
linarith
have h1q_ne0 : ofReal (1 - q) ≠ 0 := by
intro h
have hle := ENNReal.ofReal_eq_zero.mp h
linarith
have hwd : bernoulliLaw p = (bernoulliLaw q).withDensity g := by
ext s hs
rw [withDensity_apply _ hs]
rw [← lintegral_indicator hs g]
unfold bernoulliLaw
dsimp [g]
rw [lintegral_add_measure]
rw [lintegral_smul_measure, lintegral_smul_measure]
simp only [lintegral_dirac]
by_cases h1 : (1 : ℝ) ∈ s
· by_cases h0 : (0 : ℝ) ∈ s
· simp [h1, h0, ENNReal.ofReal_div_of_pos hq0,
ENNReal.ofReal_div_of_pos (sub_pos.mpr hq1),
ENNReal.mul_div_cancel hq_ne0 ENNReal.ofReal_ne_top,
ENNReal.mul_div_cancel h1q_ne0 ENNReal.ofReal_ne_top]
· simp [h1, h0, ENNReal.ofReal_div_of_pos hq0,
ENNReal.mul_div_cancel hq_ne0 ENNReal.ofReal_ne_top]
· by_cases h0 : (0 : ℝ) ∈ s
· simp [h1, h0, ENNReal.ofReal_div_of_pos (sub_pos.mpr hq1),
ENNReal.mul_div_cancel h1q_ne0 ENNReal.ofReal_ne_top]
· simp [h1, h0]
have hac : bernoulliLaw p ≪ bernoulliLaw q := by
rw [hwd]
exact withDensity_absolutelyContinuous (bernoulliLaw q) g
have hrn : (bernoulliLaw p).rnDeriv (bernoulliLaw q) =ᵐ[bernoulliLaw q] g := by
rw [hwd]
exact Measure.rnDeriv_withDensity (bernoulliLaw q) hg
rw [InformationTheory.toReal_klDiv_eq_integral_klFun hac]
trans ∫ x, klFun (g x).toReal ∂(bernoulliLaw q)
· exact integral_congr_ae <| by
filter_upwards [hrn] with x hx
rw [hx]
rw [bernoulliLaw_integral hq0.le hq1.le]
dsimp [g]
have hpq_nonneg : 0 ≤ p / q := div_nonneg hp0 hq0.le
have hcp_nonneg : 0 ≤ (1 - p) / (1 - q) :=
div_nonneg (sub_nonneg.mpr hp1) (sub_nonneg.mpr hq1.le)
simp only [↓reduceIte, zero_ne_one]
rw [ENNReal.toReal_ofReal hpq_nonneg, ENNReal.toReal_ofReal hcp_nonneg]
have hqne : q ≠ 0 := hq0.ne'
have h1qne : 1 - q ≠ 0 := sub_ne_zero.mpr hq1.ne'
have hA :
q * klFun (p / q) = p * log (p / q) + q - p := by
rw [InformationTheory.klFun_apply]
field_simp [hqne]
have hB :
(1 - q) * klFun ((1 - p) / (1 - q))
= (1 - p) * log ((1 - p) / (1 - q)) + (1 - q) - (1 - p) := by
rw [InformationTheory.klFun_apply]
field_simp [h1qne]
rw [hA, hB]
ring
lemma bernoulliLaw_klDiv_le_four_sq_sub reviewed
⚑ flagged
Causalean.Mathlib.Probability
If both success probabilities and lie in the middle half of the unit interval, and , then the Kullback–Leibler divergence from the Bernoulli() law to the Bernoulli() law is at most four times the squared difference of the probabilities, .
Formal statement
hypotheses
p q :
ℝ
hp_lo :
(1 : ℝ) / 4 ≤ p
hp_hi :
p ≤ 3 / 4
hq_lo :
(1 : ℝ) / 4 ≤ q
hq_hi :
q ≤ 3 / 4
conclusion
≤ ofReal (4 * (p - q) ^ 2)
Proof (Lean source)
lemma bernoulliLaw_klDiv_le_four_sq_sub {p q : ℝ}
(hp_lo : (1 : ℝ) / 4 ≤ p) (hp_hi : p ≤ 3 / 4)
(hq_lo : (1 : ℝ) / 4 ≤ q) (hq_hi : q ≤ 3 / 4) :
klDiv (bernoulliLaw p) (bernoulliLaw q)
≤ ofReal (4 * (p - q) ^ 2) := by
have hp0 : 0 < p := by linarith
have hp1 : p < 1 := by linarith
have hq0 : 0 < q := by linarith
have hq1 : q < 1 := by linarith
have hac : bernoulliLaw p ≪ bernoulliLaw q :=
bernoulliLaw_ac_of_reference_interior hq0 hq1
have hint : Integrable (llr (bernoulliLaw p) (bernoulliLaw q)) (bernoulliLaw p) :=
bernoulliLaw_llr_integrable
have hfinite :
klDiv (bernoulliLaw p) (bernoulliLaw q) ≠ ⊤ :=
InformationTheory.klDiv_ne_top hac hint
rw [← ENNReal.ofReal_toReal hfinite]
exact ENNReal.ofReal_le_ofReal <| by
rw [bernoulliLaw_klDiv_toReal hp0.le hp1.le hq0 hq1]
exact bernoulli_kl_le_four_sq_sub_of_mem_quarter_band
hp_lo hp_hi hq_lo hq_hi
def bernoulliBool reviewed
⚑ flagged
Causalean.Mathlib.Probability
For any real number interpreted as a success parameter, the Boolean-valued Bernoulli measure assigns mass to true and mass to false.
def binomialWeight reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a nonnegative number of trials, a real success parameter, and a nonnegative count, the binomial weight is .
17 supporting declarations (lemmas, instances)
-
bernoulliLaw_integrallemma — Two-point integral for the custom bernoulliLaw: since bernoulliLaw p = ENNReal.ofReal p • dirac 1 + ENNReal.ofReal (1-p) • dirac 0, its integral splits via integral_add_measure / integral_smul_measure / integral_dirac into the two-point weighted sum, with 0 ≤ p ≤ 1 collapsing the ENNReal → ℝ coercions to p and 1 - p.hypothesesp :ℝhp0 :0 ≤ php1 :p ≤ 1f :ℝ → ℝconclusion∫ y, f y ∂(bernoulliLaw p) = p * f 1 + (1 - p) * f 0Proof (Lean source)
lemma bernoulliLaw_integral {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : ℝ → ℝ) : ∫ y, f y ∂(bernoulliLaw p) = p * f 1 + (1 - p) * f 0 := by unfold bernoulliLaw rw [integral_add_measure] · rw [integral_smul_measure, integral_smul_measure] simp [hp0, sub_nonneg.mpr hp1, smul_eq_mul] · exact Integrable.smul_measure (μ := Measure.dirac (1 : ℝ)) (c := ofReal p) (integrable_dirac (f := f) (a := (1 : ℝ)) (by simp [enorm])) (by simp) · exact Integrable.smul_measure (μ := Measure.dirac (0 : ℝ)) (c := ofReal (1 - p)) (integrable_dirac (f := f) (a := (0 : ℝ)) (by simp [enorm])) (by simp) -
bernoulliLaw_isProbabilityMeasurelemma — The custom bernoulliLaw is a probability measure for 0 ≤ p ≤ 1: its total mass is p + (1 - p) = 1.Proof (Lean source)
lemma bernoulliLaw_isProbabilityMeasure {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : IsProbabilityMeasure (bernoulliLaw p) := by rw [isProbabilityMeasure_iff] unfold bernoulliLaw rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp only [Measure.dirac_apply, Set.indicator_of_mem, Set.mem_univ, Pi.one_apply, smul_eq_mul, mul_one] rw [← ENNReal.ofReal_add hp0 (sub_nonneg.mpr hp1)] norm_num -
bernoulliLaw_ae_nonneglemma — The Bernoulli law on the real line is almost surely nonnegative, since all of its mass is placed at 0 and 1.Proof (Lean source)
lemma bernoulliLaw_ae_nonneg {p : ℝ} : 0 ≤ᵐ[bernoulliLaw p] (fun y : ℝ => y) := by change (bernoulliLaw p) {y : ℝ | ¬ 0 ≤ y} = 0 have hset : {y : ℝ | ¬ 0 ≤ y} = {y | y < 0} := by ext y simp [not_le] rw [hset] unfold bernoulliLaw rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp -
bernoulliLaw_ae_le_onelemma — The Bernoulli law on the real line is almost surely at most one, since all of its mass is placed at 0 and 1.Proof (Lean source)
lemma bernoulliLaw_ae_le_one {p : ℝ} : (fun y : ℝ => y) ≤ᵐ[bernoulliLaw p] fun _ => (1 : ℝ) := by change (bernoulliLaw p) {y : ℝ | ¬ y ≤ 1} = 0 have hset : {y : ℝ | ¬ y ≤ 1} = {y | 1 < y} := by ext y simp [not_le] rw [hset] unfold bernoulliLaw rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp -
bernoulliLaw_ae_zero_or_onelemma — A draw from the real-valued Bernoulli law is almost surely either 0 or 1.hypothesesp :ℝconclusion∀ᵐ y ∂bernoulliLaw p, y = 0 ∨ y = 1Proof (Lean source)
lemma bernoulliLaw_ae_zero_or_one {p : ℝ} : ∀ᵐ y ∂bernoulliLaw p, y = 0 ∨ y = 1 := by change (bernoulliLaw p) {y : ℝ | ¬ (y = 0 ∨ y = 1)} = 0 unfold bernoulliLaw rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp -
bernoulliLaw_ac_of_reference_interiorlemma — A Bernoulli law is absolutely continuous with respect to any Bernoulli law whose success probability is strictly between zero and one.Proof (Lean source)
lemma bernoulliLaw_ac_of_reference_interior {p q : ℝ} (hq0 : 0 < q) (hq1 : q < 1) : bernoulliLaw p ≪ bernoulliLaw q := by have hq_ne0 : ofReal q ≠ 0 := by intro h have hle := ENNReal.ofReal_eq_zero.mp h linarith have h1q_ne0 : ofReal (1 - q) ≠ 0 := by intro h have hle := ENNReal.ofReal_eq_zero.mp h linarith refine Measure.AbsolutelyContinuous.mk ?_ intro s hs hzero unfold bernoulliLaw at hzero ⊢ rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] at hzero ⊢ by_cases h1 : (1 : ℝ) ∈ s · exfalso by_cases h0 : (0 : ℝ) ∈ s · simp [h1, h0, hq_ne0] at hzero · simp [h1, h0, hq_ne0] at hzero · by_cases h0 : (0 : ℝ) ∈ s · exfalso simp [h1, h0, h1q_ne0] at hzero · simp [h1, h0] -
bernoulliLaw_llr_integrablelemma — The log-likelihood ratio between any two real-parameter Bernoulli laws is integrable under the first law.Proof (Lean source)
@[fun_prop] lemma bernoulliLaw_llr_integrable {p q : ℝ} : Integrable (llr (bernoulliLaw p) (bernoulliLaw q)) (bernoulliLaw p) := by unfold bernoulliLaw rw [integrable_add_measure] constructor · exact Integrable.smul_measure (μ := Measure.dirac (1 : ℝ)) (c := ofReal p) (integrable_dirac (f := llr (ofReal p • Measure.dirac (1 : ℝ) + ofReal (1 - p) • Measure.dirac (0 : ℝ)) (bernoulliLaw q)) (a := (1 : ℝ)) (by simp [enorm])) (by simp) · exact Integrable.smul_measure (μ := Measure.dirac (0 : ℝ)) (c := ofReal (1 - p)) (integrable_dirac (f := llr (ofReal p • Measure.dirac (1 : ℝ) + ofReal (1 - p) • Measure.dirac (0 : ℝ)) (bernoulliLaw q)) (a := (0 : ℝ)) (by simp [enorm])) (by simp) -
bernoulliLaw_lintegral_ofReallemma — ℝ≥0∞/lintegral analogue of bernoulliLaw_integral: a Bernoulli law integrates an ℝ≥0∞-valued function as the two-point weighted sum.Proof (Lean source)
lemma bernoulliLaw_lintegral_ofReal {p : ℝ} (f : ℝ → ENNReal) : ∫⁻ y, f y ∂(bernoulliLaw p) = ofReal p * f 1 + ofReal (1 - p) * f 0 := by unfold bernoulliLaw rw [lintegral_add_measure] · simp [lintegral_smul_measure, mul_comm] -
measurable_bernoulliBoollemma — The Bool-valued Bernoulli distribution varies measurably with its success probability, so a measurable probability parameter can be used to construct a measurable kernel.conclusionProof (Lean source)
@[fun_prop] lemma measurable_bernoulliBool : Measurable bernoulliBool := by unfold bernoulliBool fun_prop -
bernoulliBool_isProbabilityMeasurelemma — A Bool-valued Bernoulli distribution is a probability distribution whenever its success probability lies between zero and one.Proof (Lean source)
lemma bernoulliBool_isProbabilityMeasure {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) : IsProbabilityMeasure (bernoulliBool p) := by rw [isProbabilityMeasure_iff] unfold bernoulliBool rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp only [Measure.dirac_apply, Set.indicator_of_mem, Set.mem_univ, Pi.one_apply, smul_eq_mul, mul_one] rw [← ENNReal.ofReal_add hp0 (sub_nonneg.mpr hp1)] convert ENNReal.ofReal_one using 2 all_goals ring -
bernoulliBool_integrallemma — The expectation of a real-valued function of a Bool-valued Bernoulli draw is its value at success times the success probability plus its value at failure times the failure probability.hypothesesProof (Lean source)
lemma bernoulliBool_integral {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) (f : Bool → ℝ) : ∫ z, f z ∂bernoulliBool p = p * f true + (1 - p) * f false := by unfold bernoulliBool rw [integral_add_measure] · rw [integral_smul_measure, integral_smul_measure] simp [hp0, sub_nonneg.mpr hp1, smul_eq_mul] · exact Integrable.smul_measure (μ := Measure.dirac true) (c := ofReal p) (integrable_dirac (f := f) (a := true) (by simp [enorm])) (by simp) · exact Integrable.smul_measure (μ := Measure.dirac false) (c := ofReal (1 - p)) (integrable_dirac (f := f) (a := false) (by simp [enorm])) (by simp) -
bernoulliBool_bindlemma — Drawing a Bool-valued Bernoulli variable and then selecting a distribution according to its value produces the corresponding success-probability mixture of the two distributions.hypothesesProof (Lean source)
lemma bernoulliBool_bind {β : Type*} [MeasurableSpace β] (p : ℝ) (K : Bool → Measure β) : (bernoulliBool p).bind K = ofReal p • K true + ofReal (1 - p) • K false := by ext A hA rw [Measure.bind_apply hA (measurable_of_finite _).aemeasurable] unfold bernoulliBool rw [lintegral_add_measure, lintegral_smul_measure, lintegral_smul_measure] simp [Measure.add_apply, Measure.smul_apply, smul_eq_mul] -
bernoulliBool_maplemma — Transforming a Bool-valued Bernoulli draw produces a two-point distribution concentrated on the transformed success and failure values with their original probabilities.hypothesesProof (Lean source)
lemma bernoulliBool_map {β : Type*} [MeasurableSpace β] (p : ℝ) (f : Bool → β) : (bernoulliBool p).map f = ofReal p • Measure.dirac (f true) + ofReal (1 - p) • Measure.dirac (f false) := by have hf : Measurable f := measurable_of_finite f unfold bernoulliBool rw [Measure.map_add _ _ hf, Measure.map_smul, Measure.map_smul] rw [Measure.map_dirac' hf, Measure.map_dirac' hf] -
sum_bernoulli_eq_binomiallemma — A Bernoulli-weighted sum of any function of the success count equals the corresponding sum against the binomial mass function.hypothesesProof (Lean source)
lemma sum_bernoulli_eq_binomial {ι : Type*} [Fintype ι] [DecidableEq ι] (p : Real) (F : Nat → Real) : (∑ b : ι → Bool, (∏ i, if b i then p else 1 - p) * F (Finset.univ.filter fun i => b i = true).card) = ∑ j ∈ range (card ι + 1), binomialWeight (card ι) p j * F j := by classical rw [Fintype.sum_equiv (boolFunEquivFinset ι) _ (fun s : Finset ι => p ^ s.card * (1 - p) ^ (card ι - s.card) * F s.card) (fun b => by rw [prod_bernoulli_eq_card] rfl)] rw [show (Finset.univ : Finset (Finset ι)) = Finset.univ.powerset by ext s simp] rw [Finset.sum_powerset] apply Finset.sum_congr rfl intro j hj rw [Finset.sum_powersetCard j Finset.univ (fun j => p ^ j * (1 - p) ^ (card ι - j) * F j)] simp only [Finset.card_univ, binomialWeight] ring -
totalized_inverse_count_lelemma — The reciprocal of a positive integer, totalized to zero at the origin, is at most twice the reciprocal of its successor.Proof (Lean source)
lemma totalized_inverse_count_le (j : Nat) : (if 0 < j then (j : Real)⁻¹ else 0) ≤ 2 * ((j : Real) + 1)⁻¹ := by by_cases hj : 0 < j · rw [if_pos hj, ← div_eq_mul_inv] have hjR : (0 : Real) < j := by exact_mod_cast hj have hj1R : (0 : Real) < (j : Real) + 1 := by positivity apply (le_div_iff₀ hj1R).2 calc (j : Real)⁻¹ * ((j : Real) + 1) = 1 + (j : Real)⁻¹ := by field_simp _ ≤ 2 := by have hinv : (j : Real)⁻¹ ≤ 1 := (inv_le_one₀ hjR).2 (by exact_mod_cast hj) linarith · simp [hj] positivity -
binomial_totalized_inverse_count_lelemma — When the success probability is positive and at most one, the binomial expectation of the zero-safe inverse success count is at most twice the reciprocal of the trial count plus one times that probability.hypothesesconclusionProof (Lean source)
lemma binomial_totalized_inverse_count_le (m : Nat) (p : Real) (hp : 0 < p) (hp1 : p ≤ 1) : (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j then (j : Real)⁻¹ else 0)) ≤ 2 / (((m + 1 : Nat) : Real) * p) := by -- Proof route: compare `1/j` with `2/(j+1)`, shift `choose m j`, -- and evaluate the resulting binomial row by `add_pow`. let d : Real := ((m + 1 : Nat) : Real) * p let S : Real := ∑ j ∈ range (m + 1), binomialWeight m p j * ((j : Real) + 1)⁻¹ have hq : 0 ≤ 1 - p := sub_nonneg.mpr hp1 have hd : 0 < d := by dsimp [d] positivity have hterm (j : Nat) (hj : j ∈ range (m + 1)) : d * (binomialWeight m p j * ((j : Real) + 1)⁻¹) = (Nat.choose (m + 1) (j + 1) : Real) * p ^ (j + 1) * (1 - p) ^ ((m + 1) - (j + 1)) := by have hjlt : j < m + 1 := Finset.mem_range.mp hj have hsub : (m + 1) - (j + 1) = m - j := by omega have hc : (((m + 1 : Nat) : Real) * (Nat.choose m j : Real)) = (Nat.choose (m + 1) (j + 1) : Real) * ((j + 1 : Nat) : Real) := by exact_mod_cast Nat.add_one_mul_choose_eq m j dsimp [d] rw [binomialWeight, hsub, pow_succ] field_simp calc ((m + 1 : Nat) : Real) * (Nat.choose m j : Real) * (1 - p) ^ (m - j) = ((((m + 1 : Nat) : Real) * (Nat.choose m j : Real)) * (1 - p) ^ (m - j)) := by ring _ = (((Nat.choose (m + 1) (j + 1) : Real) * ((j + 1 : Nat) : Real)) * (1 - p) ^ (m - j)) := by rw [hc] _ = (1 - p) ^ (m - j) * ((j : Real) + 1) * (Nat.choose (m + 1) (j + 1) : Real) := by push_cast; ring have hid : d * S = 1 - (1 - p) ^ (m + 1) := by dsimp [S] rw [Finset.mul_sum] calc (∑ j ∈ range (m + 1), d * (binomialWeight m p j * ((j : Real) + 1)⁻¹)) = ∑ j ∈ range (m + 1), p ^ (j + 1) * (1 - p) ^ ((m + 1) - (j + 1)) * (Nat.choose (m + 1) (j + 1) : Real) := by apply Finset.sum_congr rfl intro j hj rw [hterm j hj] ring _ = (p + (1 - p)) ^ (m + 1) - (1 - p) ^ (m + 1) := by rw [add_pow] rw [Finset.sum_range_succ' (fun k => p ^ k * (1 - p) ^ ((m + 1) - k) * (Nat.choose (m + 1) k : Real)) (m + 1)] simp _ = 1 - (1 - p) ^ (m + 1) := by ring have hS : S ≤ 1 / d := by apply (le_div_iff₀ hd).2 rw [mul_comm S d, hid] have hpow := pow_nonneg hq (m + 1) linarith calc (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j then (j : Real)⁻¹ else 0)) ≤ ∑ j ∈ range (m + 1), binomialWeight m p j * (2 * ((j : Real) + 1)⁻¹) := by apply Finset.sum_le_sum intro j hj apply mul_le_mul_of_nonneg_left (totalized_inverse_count_le j) dsimp [binomialWeight] positivity _ = 2 * S := by dsimp [S] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj ring _ ≤ 2 * (1 / d) := by nlinarith _ = 2 / (((m + 1 : Nat) : Real) * p) := by dsimp [d] ring -
binomial_inverse_two_arms_interior_lelemma — If the overlap margin is positive and the success probability lies between that margin and one minus the margin, the binomial expectation of the two inverse arm counts on the interior event is at most four divided by the trial count plus one times the margin.hypothesesProof (Lean source)
lemma binomial_inverse_two_arms_interior_le (m : Nat) (p epsilon : Real) (hepsilon : 0 < epsilon) (hlo : epsilon ≤ p) (hhi : p ≤ 1 - epsilon) : (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j ∧ j < m then (j : Real)⁻¹ + ((m - j : Nat) : Real)⁻¹ else 0)) ≤ 4 / (((m + 1 : Nat) : Real) * epsilon) := by -- Apply the preceding estimate to successes with parameter `p` and to -- failures with parameter `1-p`; deleting the two endpoints only lowers -- the nonnegative sums. Then use both overlap inequalities. have hp : 0 < p := lt_of_lt_of_le hepsilon hlo have hp1 : p ≤ 1 := by linarith have hq : 0 < 1 - p := by linarith have hq1 : 1 - p ≤ 1 := by linarith have hinter (j : Nat) : (if 0 < j ∧ j < m then (j : Real)⁻¹ + ((m - j : Nat) : Real)⁻¹ else 0) ≤ (if 0 < j then (j : Real)⁻¹ else 0) + (if 0 < m - j then ((m - j : Nat) : Real)⁻¹ else 0) := by by_cases hj : 0 < j ∧ j < m · have hmj : 0 < m - j := Nat.sub_pos_of_lt hj.2 simp [hj, hmj] · rw [if_neg hj] positivity have hfail : (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < m - j then ((m - j : Nat) : Real)⁻¹ else 0)) = ∑ j ∈ range (m + 1), binomialWeight m (1 - p) j * (if 0 < j then (j : Real)⁻¹ else 0) := by rw [← Finset.sum_range_reflect (fun j => binomialWeight m p j * (if 0 < m - j then ((m - j : Nat) : Real)⁻¹ else 0)) (m + 1)] apply Finset.sum_congr rfl intro j hj have hjlt : j < m + 1 := Finset.mem_range.mp hj have hjle : j ≤ m := by omega have hreflect : m + 1 - 1 - j = m - j := by omega have hcancel : m - (m - j) = j := by omega rw [hreflect, binomialWeight, binomialWeight, hcancel, Nat.choose_symm hjle] congr 1 ring have hsuccess := binomial_totalized_inverse_count_le m p hp hp1 have hfailure := binomial_totalized_inverse_count_le m (1 - p) hq hq1 have hn : (0 : Real) < ((m + 1 : Nat) : Real) := by positivity have hnepsilon : ((m + 1 : Nat) : Real) * epsilon ≤ ((m + 1 : Nat) : Real) * p := mul_le_mul_of_nonneg_left hlo hn.le have hnqepsilon : ((m + 1 : Nat) : Real) * epsilon ≤ ((m + 1 : Nat) : Real) * (1 - p) := by apply mul_le_mul_of_nonneg_left _ hn.le linarith have hinvp : 1 / (((m + 1 : Nat) : Real) * p) ≤ 1 / (((m + 1 : Nat) : Real) * epsilon) := one_div_le_one_div_of_le (mul_pos hn hepsilon) hnepsilon have hinvq : 1 / (((m + 1 : Nat) : Real) * (1 - p)) ≤ 1 / (((m + 1 : Nat) : Real) * epsilon) := one_div_le_one_div_of_le (mul_pos hn hepsilon) hnqepsilon calc (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j ∧ j < m then (j : Real)⁻¹ + ((m - j : Nat) : Real)⁻¹ else 0)) ≤ ∑ j ∈ range (m + 1), binomialWeight m p j * ((if 0 < j then (j : Real)⁻¹ else 0) + (if 0 < m - j then ((m - j : Nat) : Real)⁻¹ else 0)) := by apply Finset.sum_le_sum intro j hj apply mul_le_mul_of_nonneg_left (hinter j) dsimp [binomialWeight] positivity _ = (∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < j then (j : Real)⁻¹ else 0)) + ∑ j ∈ range (m + 1), binomialWeight m p j * (if 0 < m - j then ((m - j : Nat) : Real)⁻¹ else 0) := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro j hj ring _ ≤ 2 / (((m + 1 : Nat) : Real) * p) + 2 / (((m + 1 : Nat) : Real) * (1 - p)) := by rw [hfail] linarith _ ≤ 4 / (((m + 1 : Nat) : Real) * epsilon) := by rw [show 2 / (((m + 1 : Nat) : Real) * p) = 2 * (1 / (((m + 1 : Nat) : Real) * p)) by ring, show 2 / (((m + 1 : Nat) : Real) * (1 - p)) = 2 * (1 / (((m + 1 : Nat) : Real) * (1 - p))) by ring, show 4 / (((m + 1 : Nat) : Real) * epsilon) = 4 * (1 / (((m + 1 : Nat) : Real) * epsilon)) by ring] linarith
CovarianceCauchySchwarz 1 core · 1 supporting For square-integrable statistics X and Y under a finite measure, the squared covariance is at most the product of the variances (covariance_sq_le_variance_mul), equivalently the absolute covariance is at most the product ★ abs_covariance_le_sqrt_mul
Cauchy–Schwarz for covariance
For square-integrable statistics X and Y under a finite measure, the squared covariance is at
most the product of the variances (covariance_sq_le_variance_mul), equivalently the absolute
covariance is at most the product of the standard deviations (abs_covariance_le_sqrt_mul). This
is the covariance form of the Cauchy–Schwarz inequality, filling a gap in Mathlib's covariance API.
theorem abs_covariance_le_sqrt_mul reviewed
⚑ flagged
Causalean.Mathlib
Cauchy–Schwarz for covariance. Under a finite measure, if is square-integrable and is square-integrable, then the absolute value of their covariance is at most the product of their standard deviations, .
Proof (Lean source)
theorem abs_covariance_le_sqrt_mul [IsFiniteMeasure μ] {X Y : Ω → ℝ}
(hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) :
|covariance X Y μ| ≤ sqrt (variance X μ) * sqrt (variance Y μ) := by
have h := covariance_sq_le_variance_mul hX hY
rw [← Real.sqrt_mul (variance_nonneg X μ), ← Real.sqrt_sq_eq_abs]
exact Real.sqrt_le_sqrt h
1 supporting declaration (lemmas, instances)
-
covariance_sq_le_variance_multheorem — Cauchy–Schwarz for covariance (squared form). For square-integrable statistics under a finite measure, the squared covariance is at most the product of the two variances.Proof (Lean source)
theorem covariance_sq_le_variance_mul [IsFiniteMeasure μ] {X Y : Ω → ℝ} (hX : MemLp X 2 μ) (hY : MemLp Y 2 μ) : covariance X Y μ ^ 2 ≤ variance X μ * variance Y μ := by have hquad : ∀ t : ℝ, 0 ≤ variance X μ - 2 * t * covariance X Y μ + t ^ 2 * variance Y μ := by intro t have hsub : MemLp (t • Y) 2 μ := hY.const_smul t have h := variance_nonneg (fun ω => X ω - (t • Y) ω) μ rw [variance_fun_sub hX hsub, variance_smul, covariance_smul_right] at h simpa [Pi.smul_apply, smul_eq_mul, mul_assoc] using h by_cases hvar : variance Y μ = 0 · have hcov : covariance X Y μ = 0 := by by_contra hcov have h := hquad ((variance X μ + 1) / (2 * covariance X Y μ)) rw [hvar] at h have hvalue : variance X μ - 2 * ((variance X μ + 1) / (2 * covariance X Y μ)) * covariance X Y μ = -1 := by field_simp [hcov] ring rw [hvalue] at h norm_num at h simp [hvar, hcov] · have hvarpos : 0 < variance Y μ := lt_of_le_of_ne (variance_nonneg Y μ) (Ne.symm hvar) apply (div_le_iff₀ hvarpos).mp have h := hquad (covariance X Y μ / variance Y μ) have hvalue : variance X μ - 2 * (covariance X Y μ / variance Y μ) * covariance X Y μ + (covariance X Y μ / variance Y μ) ^ 2 * variance Y μ = variance X μ - covariance X Y μ ^ 2 / variance Y μ := by field_simp [hvar] ring rw [hvalue] at h linarith
DarmoisSkitovich 2 core · 4 supporting This file develops the finite-variance Darmois–Skitovich theorem, starting from its simplest non-degenerate instance, Bernstein's theorem: if two independent real random variables X and Y (with finite second moments) are ★ gaussianForm_of_funeq★ bernstein
The Darmois–Skitovich theorem (finite-variance case): Bernstein's theorem
This file develops the finite-variance Darmois–Skitovich theorem, starting from
its simplest non-degenerate instance, Bernstein's theorem: if two independent
real random variables X and Y (with finite second moments) are such that their
sum X + Y and difference X − Y are independent, then X and Y are each
Gaussian. This is the analytic engine behind the identifiability of linear
non-Gaussian causal models (LiNGAM, Shimizu et al. 2006): non-Gaussian
disturbances are exactly what break the rotational symmetry that Bernstein's
theorem characterizes.
The proof works at the level of characteristic functions f = charFun (P.map X)
and g = charFun (P.map Y):
1. bernstein_charFun_funeq — the functional equation obtained by computing
the joint characteristic function of (X, Y) two ways (directly, and through
the independent pair (X + Y, X − Y)):
f (u+v) · g (u−v) = f u · g u · f v · g (−v).
2. charFun_eventually_ne_zero — f and g are nonzero on a neighbourhood of
0, so the logarithmic derivatives f'/f, g'/g are defined there.
3. gaussianForm_of_funeq / bernstein_charFun_gaussian_nhds_zero — the
analytic core: working with the logarithmic derivative h_f = f'/f (no
Complex.log, hence no branch cuts), differentiate the functional equation
once in each of u and v to get h_f'(u+v) = h_g'(u−v); as (u+v, u−v)
ranges over a neighbourhood of 0, both are one constant, so h_f is affine
and f is a Gaussian characteristic function near 0.
4. A doubling bootstrap (the instance f (2t) = f t ^ 2 · g t · g (−t) of the
functional equation) propagates the Gaussian form from a neighbourhood of 0
to all of ℝ; Measure.ext_of_charFun then identifies the law as Gaussian.
The proof is organized into those four steps: a characteristic-function
functional equation, neighbourhood nonvanishing, the local Gaussian-form
argument, and the doubling bootstrap to a global Gaussian law. The supporting
infrastructure comes from Mathlib's charFun, differentiability, independent
sum, measure-extensionality, and real Gaussian characteristic-function APIs.
lemma gaussianForm_of_funeq reviewed
⚑ flagged
Causalean.Mathlib.Probability
Pure analytic core: the Bernstein functional equation forces a Gaussian form. Let f, g : ℝ → ℂ be functions that are twice continuously differentiable and equal to 1 at the origin, and suppose they satisfy the Bernstein functional equation f (u+v) · g (u−v) = f u · g u · (f v · g (−v)) for all real u, v. Then there is a single constant c such that, on a neighbourhood of 0, f t = exp (f'(0)·t + c·t²/2) and g t = exp (g'(0)·t + c·t²/2), with the same c in both formulas.
Formal statement
Proof (Lean source)
lemma gaussianForm_of_funeq {f g : ℝ → ℂ}
(hf : ContDiff ℝ 2 f) (hg : ContDiff ℝ 2 g) (hf0 : f 0 = 1) (hg0 : g 0 = 1)
(hfe : ∀ u v : ℝ, f (u + v) * g (u - v) = f u * g u * (f v * g (-v))) :
∃ c : ℂ,
(∀ᶠ t in nhds (0 : ℝ), f t = exp (deriv f 0 * t + c * t ^ 2 / 2)) ∧
(∀ᶠ t in nhds (0 : ℝ), g t = exp (deriv g 0 * t + c * t ^ 2 / 2)) := by
let lf : ℝ → ℂ := fun t => deriv f t / f t
let lg : ℝ → ℂ := fun t => deriv g t / g t
have hfD : Differentiable ℝ f :=
(hf.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
have hgD : Differentiable ℝ g :=
(hg.of_le (by norm_num : (1 : WithTop ℕ∞) ≤ 2)).differentiable_one
have hdfD : Differentiable ℝ (deriv f) := hf.differentiable_deriv_two
have hdgD : Differentiable ℝ (deriv g) := hg.differentiable_deriv_two
have hf_ne : ∀ᶠ t in nhds (0 : ℝ), f t ≠ 0 :=
hf.continuous.continuousAt.eventually_ne (by simp [hf0] : f 0 ≠ 0)
have hg_ne : ∀ᶠ t in nhds (0 : ℝ), g t ≠ 0 :=
hg.continuous.continuousAt.eventually_ne (by simp [hg0] : g 0 ≠ 0)
have hlf0 : lf 0 = deriv f 0 := by simp [lf, hf0]
have hlg0 : lg 0 = deriv g 0 := by simp [lg, hg0]
have hlfDiffAt : ∀ {x : ℝ}, f x ≠ 0 → DifferentiableAt ℝ lf x := by
intro x hx
exact (hdfD x).div (hfD x) hx
have hlgDiffAt : ∀ {x : ℝ}, g x ≠ 0 → DifferentiableAt ℝ lg x := by
intro x hx
exact (hdgD x).div (hgD x) hx
have hD1 : ∀ u v : ℝ,
deriv f (u + v) * g (u - v) + f (u + v) * deriv g (u - v) =
(deriv f u * g u + f u * deriv g u) * (f v * g (-v)) := by
intro u v
have hleftF : (fun x : ℝ => f (x + v) * g (x - v)) =
(fun x : ℝ => f x * g x * (f v * g (-v))) := by
funext x
exact hfe x v
have hfp : HasDerivAt (fun x : ℝ => f (x + v)) (deriv f (u + v)) u := by
simpa using (hfD (u + v)).hasDerivAt.comp_add_const u v
have hgm : HasDerivAt (fun x : ℝ => g (x - v)) (deriv g (u - v)) u := by
simpa using (hgD (u - v)).hasDerivAt.comp_sub_const u v
have hleft : HasDerivAt (fun x : ℝ => f (x + v) * g (x - v))
(deriv f (u + v) * g (u - v) + f (u + v) * deriv g (u - v)) u := by
exact hfp.fun_mul hgm
have hfu : HasDerivAt (fun x : ℝ => f x) (deriv f u) u := (hfD u).hasDerivAt
have hgu : HasDerivAt (fun x : ℝ => g x) (deriv g u) u := (hgD u).hasDerivAt
have hright : HasDerivAt (fun x : ℝ => f x * g x * (f v * g (-v)))
((deriv f u * g u + f u * deriv g u) * (f v * g (-v))) u := by
exact (hfu.fun_mul hgu).mul_const (f v * g (-v))
have hright' : HasDerivAt (fun x : ℝ => f (x + v) * g (x - v))
((deriv f u * g u + f u * deriv g u) * (f v * g (-v))) u := by
simpa [hleftF] using hright
exact hleft.unique hright'
have hE1_at : ∀ u v : ℝ,
f (u + v) ≠ 0 → g (u - v) ≠ 0 → f u ≠ 0 → g u ≠ 0 →
f v ≠ 0 → g (-v) ≠ 0 →
lf (u + v) + lg (u - v) = lf u + lg u := by
intro u v hfp hgm hfu hgu hfv hgnv
have hD1' := hD1 u v
have hFE := hfe u v
dsimp [lf, lg]
calc
deriv f (u + v) / f (u + v) + deriv g (u - v) / g (u - v)
= (deriv f (u + v) * g (u - v) + f (u + v) * deriv g (u - v)) /
(f (u + v) * g (u - v)) := by
field_simp [hfp, hgm]
_ = ((deriv f u * g u + f u * deriv g u) * f v * g (-v)) /
(f u * g u * f v * g (-v)) := by
rw [hD1', hFE]
ring
_ = (deriv f u * g u + f u * deriv g u) / (f u * g u) := by
field_simp [hfu, hgu, hfv, hgnv]
_ = deriv f u / f u + deriv g u / g u := by
field_simp [hfu, hgu]
have hsecondLogDeriv :
∃ c : ℂ,
(∀ᶠ t in nhds (0 : ℝ), deriv lf t = c) ∧
(∀ᶠ t in nhds (0 : ℝ), deriv lg t = c) := by
let c : ℂ := deriv lg 0
have hpair_ne : ∀ᶠ p : ℝ × ℝ in nhds ((0, 0) : ℝ × ℝ),
f (p.1 + p.2) ≠ 0 ∧ g (p.1 - p.2) ≠ 0 ∧
f p.1 ≠ 0 ∧ g p.1 ≠ 0 ∧ f p.2 ≠ 0 ∧ g (-p.2) ≠ 0 := by
have h_add : Tendsto (fun p : ℝ × ℝ => p.1 + p.2)
(nhds ((0, 0) : ℝ × ℝ)) (nhds (0 : ℝ)) := by
have hc : Continuous (fun p : ℝ × ℝ => p.1 + p.2) :=
continuous_fst.add continuous_snd
simpa using hc.tendsto ((0, 0) : ℝ × ℝ)
have h_sub : Tendsto (fun p : ℝ × ℝ => p.1 - p.2)
(nhds ((0, 0) : ℝ × ℝ)) (nhds (0 : ℝ)) := by
have hc : Continuous (fun p : ℝ × ℝ => p.1 - p.2) :=
continuous_fst.sub continuous_snd
simpa using hc.tendsto ((0, 0) : ℝ × ℝ)
have h_fst : Tendsto (fun p : ℝ × ℝ => p.1)
(nhds ((0, 0) : ℝ × ℝ)) (nhds (0 : ℝ)) := by
simpa [ContinuousAt] using (continuous_fst.continuousAt (x := ((0, 0) : ℝ × ℝ)))
have h_snd : Tendsto (fun p : ℝ × ℝ => p.2)
(nhds ((0, 0) : ℝ × ℝ)) (nhds (0 : ℝ)) := by
simpa [ContinuousAt] using (continuous_snd.continuousAt (x := ((0, 0) : ℝ × ℝ)))
have h_neg_snd : Tendsto (fun p : ℝ × ℝ => -p.2)
(nhds ((0, 0) : ℝ × ℝ)) (nhds (0 : ℝ)) := by
have hc : Continuous (fun p : ℝ × ℝ => -p.2) := continuous_snd.neg
simpa using hc.tendsto ((0, 0) : ℝ × ℝ)
filter_upwards [h_add.eventually hf_ne, h_sub.eventually hg_ne,
h_fst.eventually hf_ne, h_fst.eventually hg_ne,
h_snd.eventually hf_ne, h_neg_snd.eventually hg_ne] with p h1 h2 h3 h4 h5 h6
exact ⟨h1, h2, h3, h4, h5, h6⟩
have hderiv_pair : ∀ᶠ p : ℝ × ℝ in nhds ((0, 0) : ℝ × ℝ),
deriv lf (p.1 + p.2) = deriv lg (p.1 - p.2) := by
filter_upwards [hpair_ne] with p hp
rcases hp with ⟨hfp, hgm, hfu, hgu, hfv, hgnv⟩
let u : ℝ := p.1
let v : ℝ := p.2
have hEq : (fun w : ℝ => lf (u + w) + lg (u - w))
=ᶠ[nhds v] fun _ : ℝ => lf u + lg u := by
have hfu' : f u ≠ 0 := by simpa [u] using hfu
have hgu' : g u ≠ 0 := by simpa [u] using hgu
have h1 : ∀ᶠ w in nhds v, f (u + w) ≠ 0 :=
((hf.continuous.continuousAt.comp
((continuous_const.add continuous_id).continuousAt))).eventually_ne
(by simpa [u, v] using hfp)
have h2 : ∀ᶠ w in nhds v, g (u - w) ≠ 0 :=
((hg.continuous.continuousAt.comp
((continuous_const.sub continuous_id).continuousAt))).eventually_ne
(by simpa [u, v] using hgm)
have h3 : ∀ᶠ w in nhds v, f w ≠ 0 :=
hf.continuous.continuousAt.eventually_ne (by simpa [v] using hfv)
have h4 : ∀ᶠ w in nhds v, g (-w) ≠ 0 :=
(hg.continuous.continuousAt.comp continuous_neg.continuousAt).eventually_ne
(by simpa [v] using hgnv)
filter_upwards [h1, h2, h3, h4] with w hw1 hw2 hw3 hw4
exact hE1_at u w hw1 hw2 hfu' hgu' hw3 hw4
have hlfp : HasDerivAt (fun w : ℝ => lf (u + w)) (deriv lf (u + v)) v := by
simpa using (hlfDiffAt (by simpa [u, v] using hfp)).hasDerivAt.comp_const_add u v
have hlgm : HasDerivAt (fun w : ℝ => lg (u - w)) (-(deriv lg (u - v))) v := by
simpa using (hlgDiffAt (by simpa [u, v] using hgm)).hasDerivAt.comp_const_sub u v
have hleft : HasDerivAt (fun w : ℝ => lf (u + w) + lg (u - w))
(deriv lf (u + v) - deriv lg (u - v)) v := by
exact (hlfp.fun_add hlgm).congr_deriv (by ring)
have hconst : HasDerivAt (fun _ : ℝ => lf u + lg u)
(deriv lf (u + v) - deriv lg (u - v)) v :=
hleft.congr_of_eventuallyEq hEq.symm
have hzero : HasDerivAt (fun _ : ℝ => lf u + lg u) 0 v := hasDerivAt_const v _
have hsub : deriv lf (u + v) - deriv lg (u - v) = 0 := hconst.unique hzero
have hres : deriv lf (u + v) = deriv lg (u - v) := sub_eq_zero.mp hsub
simpa [u, v] using hres
have hlfDeriv : ∀ᶠ t in nhds (0 : ℝ), deriv lf t = c := by
have hline : Tendsto (fun t : ℝ => (t / 2, t / 2))
(nhds (0 : ℝ)) (nhds ((0, 0) : ℝ × ℝ)) := by
simpa [ContinuousAt] using ((continuous_id.div_const (2 : ℝ)).prodMk
(continuous_id.div_const (2 : ℝ))).continuousAt (x := (0 : ℝ))
filter_upwards [hline.eventually hderiv_pair] with t ht
have ht' : deriv lf (t / 2 + t / 2) = deriv lg (t / 2 - t / 2) := ht
have hsum : t / 2 + t / 2 = t := by ring
have hsub : t / 2 - t / 2 = 0 := by ring
simpa [c, hsum, hsub] using ht'
have hlgDeriv : ∀ᶠ t in nhds (0 : ℝ), deriv lg t = c := by
have hlf0c : deriv lf 0 = c := hlfDeriv.self_of_nhds
have hline : Tendsto (fun t : ℝ => (t / 2, -(t / 2)))
(nhds (0 : ℝ)) (nhds ((0, 0) : ℝ × ℝ)) := by
simpa [ContinuousAt] using ((continuous_id.div_const (2 : ℝ)).prodMk
((continuous_id.div_const (2 : ℝ)).neg)).continuousAt (x := (0 : ℝ))
filter_upwards [hline.eventually hderiv_pair] with t ht
have ht' : deriv lf (t / 2 + -(t / 2)) = deriv lg (t / 2 - -(t / 2)) := ht
have hsum : t / 2 + -(t / 2) = 0 := by ring
have hsub : t / 2 - -(t / 2) = t := by ring
have ht0 : deriv lf 0 = deriv lg t := by simpa [hsum, hsub] using ht'
exact ht0.symm.trans hlf0c
exact ⟨c, hlfDeriv, hlgDeriv⟩
obtain ⟨c, hlfDeriv, hlgDeriv⟩ := hsecondLogDeriv
have hlogAffine :
(∀ᶠ t in nhds (0 : ℝ), lf t = deriv f 0 + c * t) ∧
(∀ᶠ t in nhds (0 : ℝ), lg t = deriv g 0 + c * t) := by
have hAffDeriv : ∀ a x : ℂ, ∀ t : ℝ,
HasDerivAt (fun s : ℝ => a + x * s) x t := by
intro a x t
have hcoe : HasDerivAt (fun s : ℝ => (s : ℂ)) 1 t :=
HasDerivAt.ofReal_comp (hasDerivAt_id t)
exact ((hcoe.const_mul x).const_add a).congr_deriv (by ring)
constructor
· rcases Metric.eventually_nhds_iff_ball.mp (hlfDeriv.and hf_ne) with ⟨r, hr, hball⟩
have hlfOn : DifferentiableOn ℝ lf (ball (0 : ℝ) r) := by
intro x hx
exact (hlfDiffAt (hball x hx).2).differentiableWithinAt
have hAffOn : DifferentiableOn ℝ (fun t : ℝ => deriv f 0 + c * t)
(ball (0 : ℝ) r) := by
intro x hx
exact ((hAffDeriv (deriv f 0) c x).differentiableAt).differentiableWithinAt
have hEqOn : EqOn lf (fun t : ℝ => deriv f 0 + c * t)
(ball (0 : ℝ) r) := by
refine Metric.isOpen_ball.eqOn_of_deriv_eq (convex_ball (0 : ℝ) r).isPreconnected
hlfOn hAffOn ?_ (Metric.mem_ball_self hr) ?_
· intro x hx
have hxder : deriv lf x = c := (hball x hx).1
have hmodel : deriv (fun t : ℝ => deriv f 0 + c * t) x = c :=
(hAffDeriv (deriv f 0) c x).deriv
rw [hxder, hmodel]
· simp [hlf0]
refine Metric.eventually_nhds_iff_ball.mpr ⟨r, hr, fun t ht => ?_⟩
exact hEqOn ht
· rcases Metric.eventually_nhds_iff_ball.mp (hlgDeriv.and hg_ne) with ⟨r, hr, hball⟩
have hlgOn : DifferentiableOn ℝ lg (ball (0 : ℝ) r) := by
intro x hx
exact (hlgDiffAt (hball x hx).2).differentiableWithinAt
have hAffOn : DifferentiableOn ℝ (fun t : ℝ => deriv g 0 + c * t)
(ball (0 : ℝ) r) := by
intro x hx
exact ((hAffDeriv (deriv g 0) c x).differentiableAt).differentiableWithinAt
have hEqOn : EqOn lg (fun t : ℝ => deriv g 0 + c * t)
(ball (0 : ℝ) r) := by
refine Metric.isOpen_ball.eqOn_of_deriv_eq (convex_ball (0 : ℝ) r).isPreconnected
hlgOn hAffOn ?_ (Metric.mem_ball_self hr) ?_
· intro x hx
have hxder : deriv lg x = c := (hball x hx).1
have hmodel : deriv (fun t : ℝ => deriv g 0 + c * t) x = c :=
(hAffDeriv (deriv g 0) c x).deriv
rw [hxder, hmodel]
· simp [hlg0]
refine Metric.eventually_nhds_iff_ball.mpr ⟨r, hr, fun t ht => ?_⟩
exact hEqOn ht
have hsolve :
(∀ᶠ t in nhds (0 : ℝ), f t = exp (deriv f 0 * t + c * t ^ 2 / 2)) ∧
(∀ᶠ t in nhds (0 : ℝ), g t = exp (deriv g 0 * t + c * t ^ 2 / 2)) := by
have hExpDeriv : ∀ a : ℂ, ∀ t : ℝ,
HasDerivAt (fun s : ℝ => exp (a * s + c * s ^ 2 / 2))
((a + c * t) * exp (a * t + c * t ^ 2 / 2)) t := by
intro a t
have hcoe : HasDerivAt (fun s : ℝ => (s : ℂ)) 1 t :=
HasDerivAt.ofReal_comp (hasDerivAt_id t)
have hinner : HasDerivAt (fun s : ℝ => a * s + c * s ^ 2 / 2) (a + c * t) t :=
((hcoe.const_mul a).fun_add
(((hcoe.fun_pow 2).const_mul c).div_const 2)).congr_deriv (by norm_num; ring)
simpa [mul_comm, mul_left_comm, mul_assoc] using hinner.cexp
constructor
· let Ef : ℝ → ℂ := fun t => exp (deriv f 0 * t + c * t ^ 2 / 2)
-- … truncated; follow the source link for the rest …
theorem bernstein reviewed
⚑ flagged
Causalean.Mathlib.Probability
Bernstein's theorem (finite-variance Darmois–Skitovich, two variables). Let X and Y be real random variables that are independent and each have finite second moment. If their sum X + Y and difference X − Y are independent, then both X and Y have Gaussian laws.
Formal statement
Proof (Lean source)
theorem bernstein
(mX : Measurable X) (mY : Measurable Y)
(hX2 : MemLp X 2 P) (hY2 : MemLp Y 2 P)
(hXY : IndepFun X Y P) (hUV : IndepFun (X + Y) (X - Y) P) :
IsGaussian (P.map X) ∧ IsGaussian (P.map Y) := by
-- Assembly: `bernstein_charFun_gaussian_nhds_zero` gives the local Gaussian forms
-- for both `f = charFun (P.map X)` and `g = charFun (P.map Y)` with shared `σ²`.
-- Extend each to all of `ℝ` by the doubling instance `f (2t) = f t ^ 2 · g t · g (−t)`
-- of `bernstein_charFun_funeq` (induction on `2ⁿ`-scaled neighbourhoods), then
-- identify the law via `Measure.ext_of_charFun` against `gaussianReal mf σ²`
-- (resp. `gaussianReal mg σ²`) and conclude `IsGaussian` from the `gaussianReal`
-- instance / `isGaussian_iff_gaussian_charFun`.
obtain ⟨mf, mg, σ2, hσ, hXloc, hYloc⟩ :=
bernstein_charFun_gaussian_nhds_zero (P := P) (X := X) (Y := Y)
mX mY hX2 hY2 hXY hUV
haveI : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map mX.aemeasurable
haveI : IsProbabilityMeasure (P.map Y) := Measure.isProbabilityMeasure_map mY.aemeasurable
let Φf : ℝ → ℂ := fun t => exp (mf * t * I - σ2 * t ^ 2 / 2)
let Φg : ℝ → ℂ := fun t => exp (mg * t * I - σ2 * t ^ 2 / 2)
let EqAt : ℝ → Prop := fun t =>
charFun (P.map X) t = Φf t ∧ charFun (P.map Y) t = Φg t
have hloc : ∀ᶠ t in nhds (0 : ℝ), EqAt t := by
filter_upwards [hXloc, hYloc] with t htX htY
exact ⟨htX, htY⟩
have DBLf : ∀ t : ℝ, charFun (P.map X) (2 * t) =
charFun (P.map X) t ^ 2 * charFun (P.map Y) t * charFun (P.map Y) (-t) := by
intro t
have h := bernstein_charFun_funeq (P := P) (X := X) (Y := Y) mX mY hXY hUV t t
calc
charFun (P.map X) (2 * t)
= charFun (P.map X) (t + t) := by rw [show (2 : ℝ) * t = t + t by ring]
_ = charFun (P.map X) t ^ 2 * charFun (P.map Y) t * charFun (P.map Y) (-t) := by
simpa [sq, mul_assoc, mul_left_comm, mul_comm] using h
have DBLg : ∀ t : ℝ, charFun (P.map Y) (2 * t) =
charFun (P.map Y) t ^ 2 * charFun (P.map X) t * charFun (P.map X) (-t) := by
intro t
have h := bernstein_charFun_funeq (P := P) (X := X) (Y := Y) mX mY hXY hUV t (-t)
calc
charFun (P.map Y) (2 * t)
= charFun (P.map Y) (t - (-t)) := by rw [show (2 : ℝ) * t = t - (-t) by ring]
_ = charFun (P.map Y) t ^ 2 * charFun (P.map X) t * charFun (P.map X) (-t) := by
simpa [sq, mul_assoc, mul_left_comm, mul_comm] using h
have TDBLf : ∀ t : ℝ, Φf (2 * t) = Φf t ^ 2 * Φg t * Φg (-t) := by
intro t
simp only [Φf, Φg]
simp only [pow_two]
rw [← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add]
congr 1
norm_num
ring_nf
have TDBLg : ∀ t : ℝ, Φg (2 * t) = Φg t ^ 2 * Φf t * Φf (-t) := by
intro t
simp only [Φf, Φg]
simp only [pow_two]
rw [← Complex.exp_add, ← Complex.exp_add, ← Complex.exp_add]
congr 1
norm_num
ring_nf
have step : ∀ t : ℝ, EqAt t → EqAt (-t) → EqAt (2 * t) := by
intro t ht hnt
constructor
· calc
charFun (P.map X) (2 * t)
= charFun (P.map X) t ^ 2 * charFun (P.map Y) t * charFun (P.map Y) (-t) :=
DBLf t
_ = Φf t ^ 2 * Φg t * Φg (-t) := by rw [ht.1, ht.2, hnt.2]
_ = Φf (2 * t) := (TDBLf t).symm
· calc
charFun (P.map Y) (2 * t)
= charFun (P.map Y) t ^ 2 * charFun (P.map X) t * charFun (P.map X) (-t) :=
DBLg t
_ = Φg t ^ 2 * Φf t * Φf (-t) := by rw [ht.2, ht.1, hnt.1]
_ = Φg (2 * t) := (TDBLg t).symm
have grow : ∀ n : ℕ, ∀ t : ℝ, EqAt t → EqAt (-t) →
EqAt ((2 : ℝ) ^ n * t) ∧ EqAt (-((2 : ℝ) ^ n * t)) := by
intro n
induction n with
| zero =>
intro t ht hnt
simpa using intro ht hnt
| succ n ih =>
intro t ht hnt
obtain ⟨ha, hna⟩ := ih t ht hnt
have h2a : EqAt (2 * ((2 : ℝ) ^ n * t)) := step ((2 : ℝ) ^ n * t) ha hna
have h2na : EqAt (2 * (-((2 : ℝ) ^ n * t))) := by
exact step (-((2 : ℝ) ^ n * t)) hna (by simpa using ha)
constructor
· simpa [pow_succ, mul_assoc, mul_left_comm, mul_comm] using h2a
· simpa [pow_succ, mul_assoc, mul_left_comm, mul_comm] using h2na
have hkey : ∀ s : ℝ, EqAt s := by
intro s
have hseq : Tendsto (fun n : ℕ => s / (2 : ℝ) ^ n) atTop (nhds 0) := by
have hpow : Tendsto (fun n : ℕ => (2 : ℝ) ^ n) atTop atTop :=
tendsto_pow_atTop_atTop_of_one_lt (by norm_num : (1 : ℝ) < 2)
simpa [div_eq_mul_inv] using
(tendsto_const_nhds.mul (tendsto_inv_atTop_zero.comp hpow) :
Tendsto (fun n : ℕ => s * (((2 : ℝ) ^ n)⁻¹)) atTop (nhds (s * 0)))
have hz : ∀ᶠ n in atTop, EqAt (s / (2 : ℝ) ^ n) := hseq.eventually hloc
have hnz : ∀ᶠ n in atTop, EqAt (-(s / (2 : ℝ) ^ n)) := by
have hlocNeg : ∀ᶠ t in nhds (-(0 : ℝ)), EqAt t := by simpa using hloc
exact hseq.neg.eventually hlocNeg
obtain ⟨n, hn⟩ := (hz.and hnz).exists
have hgrow := grow n (s / (2 : ℝ) ^ n) hn.1 hn.2
have hpow_ne : (2 : ℝ) ^ n ≠ 0 := pow_ne_zero n (by norm_num : (2 : ℝ) ≠ 0)
have hs_eq : (2 : ℝ) ^ n * (s / (2 : ℝ) ^ n) = s := by
field_simp [hpow_ne]
simpa [hs_eq] using hgrow.1
have hμX : P.map X = gaussianReal mf σ2.toNNReal := by
refine Measure.ext_of_charFun ?_
funext t
rw [(hkey t).1, charFun_gaussianReal]
simp only [Φf]
congr 1
rw [Real.coe_toNNReal σ2 hσ]
ring
have hμY : P.map Y = gaussianReal mg σ2.toNNReal := by
refine Measure.ext_of_charFun ?_
funext t
rw [(hkey t).2, charFun_gaussianReal]
simp only [Φg]
congr 1
rw [Real.coe_toNNReal σ2 hσ]
ring
constructor
· rw [hμX]
infer_instance
· rw [hμY]
infer_instance
4 supporting declarations (lemmas, instances)
-
bernstein_charFun_funeqlemma — Functional equation for Bernstein's theorem. If X and Y are independent and the pair (X + Y, X − Y) is independent, then the characteristic functions f = charFun (P.map X) and g = charFun (P.map Y) satisfy f (u+v) · g (u−v) = f u · g u · f v · g (−v) for all u, v.Proof (Lean source)
lemma bernstein_charFun_funeq (mX : Measurable X) (mY : Measurable Y) (hXY : IndepFun X Y P) (hUV : IndepFun (X + Y) (X - Y) P) (u v : ℝ) : charFun (P.map X) (u + v) * charFun (P.map Y) (u - v) = charFun (P.map X) u * charFun (P.map Y) u * (charFun (P.map X) v * charFun (P.map Y) (-v)) := by have hscale : ∀ (Z : Ω → ℝ), Measurable Z → ∀ a t : ℝ, charFun (P.map (fun ω => a * Z ω)) t = charFun (P.map Z) (a * t) := by intro Z mZ a t rw [← charFun_map_mul (μ := P.map Z) a t] rw [Measure.map_map] · rfl · exact measurable_const_mul a · exact mZ have hlin : ∀ {Z W : Ω → ℝ}, Measurable Z → Measurable W → IndepFun Z W P → ∀ a b : ℝ, charFun (P.map (fun ω => a * Z ω + b * W ω)) (1 : ℝ) = charFun (P.map Z) a * charFun (P.map W) b := by intro Z W mZ mW hZW a b have hind : IndepFun (fun ω => a * Z ω) (fun ω => b * W ω) P := hZW.comp (measurable_const_mul a) (measurable_const_mul b) have h := hind.charFun_map_fun_add_eq_mul ((mZ.const_mul a).aemeasurable) ((mW.const_mul b).aemeasurable) have h1 := congrFun h (1 : ℝ) rw [Pi.mul_apply] at h1 rw [hscale Z mZ a 1, hscale W mW b 1] at h1 simpa using h1 have mAdd : Measurable (X + Y) := by fun_prop have mSub : Measurable (X - Y) := by fun_prop have hAdd : ∀ t : ℝ, charFun (P.map (X + Y)) t = charFun (P.map X) t * charFun (P.map Y) t := by intro t calc charFun (P.map (X + Y)) t = charFun (P.map (fun ω => t * (X + Y) ω)) (1 : ℝ) := by rw [hscale (X + Y) mAdd t 1] simp _ = charFun (P.map (fun ω => t * X ω + t * Y ω)) (1 : ℝ) := by congr 2 funext ω simp [Pi.add_apply] ring _ = charFun (P.map X) t * charFun (P.map Y) t := hlin mX mY hXY t t have hSub : ∀ t : ℝ, charFun (P.map (X - Y)) t = charFun (P.map X) t * charFun (P.map Y) (-t) := by intro t calc charFun (P.map (X - Y)) t = charFun (P.map (fun ω => t * (X - Y) ω)) (1 : ℝ) := by rw [hscale (X - Y) mSub t 1] simp _ = charFun (P.map (fun ω => t * X ω + (-t) * Y ω)) (1 : ℝ) := by congr 2 funext ω simp [Pi.sub_apply] ring _ = charFun (P.map X) t * charFun (P.map Y) (-t) := hlin mX mY hXY t (-t) calc charFun (P.map X) (u + v) * charFun (P.map Y) (u - v) = charFun (P.map (fun ω => (u + v) * X ω + (u - v) * Y ω)) (1 : ℝ) := by exact (hlin mX mY hXY (u + v) (u - v)).symm _ = charFun (P.map (fun ω => u * (X + Y) ω + v * (X - Y) ω)) (1 : ℝ) := by congr 2 funext ω simp [Pi.add_apply, Pi.sub_apply] ring _ = charFun (P.map (X + Y)) u * charFun (P.map (X - Y)) v := hlin mAdd mSub hUV u v _ = charFun (P.map X) u * charFun (P.map Y) u * (charFun (P.map X) v * charFun (P.map Y) (-v)) := by rw [hAdd u, hSub v] -
charFun_eventually_ne_zerolemma — The characteristic function of a probability measure on ℝ is nonzero on a neighbourhood of 0: it is continuous and equals 1 at 0. This is what makes the logarithmic derivative (charFun μ)' / charFun μ well defined near 0.Proof (Lean source)
lemma charFun_eventually_ne_zero (μ : Measure ℝ) [IsProbabilityMeasure μ] : ∀ᶠ t in nhds (0 : ℝ), charFun μ t ≠ 0 := by exact (continuous_charFun (μ := μ)).continuousAt.eventually_ne (by simp : charFun μ 0 ≠ 0) -
charFun_contDiff_twolemma — charFun of a pushforward with a finite second moment is C². This is a specialisation of contDiff_charFun (the characteristic function is Cⁿ whenever the n-th moment is finite), transferring MemLp Z 2 P to MemLp id 2 (P.map Z) along the pushforward map.hypothesesProof (Lean source)
lemma charFun_contDiff_two {Z : Ω → ℝ} [IsFiniteMeasure P] (hZ : MemLp Z 2 P) : ContDiff ℝ 2 (charFun (P.map Z)) := by refine contDiff_charFun (μ := P.map Z) ?_ exact (memLp_map_measure_iff aestronglyMeasurable_id hZ.aestronglyMeasurable.aemeasurable).2 (by simpa [Function.comp_def] using hZ) -
bernstein_charFun_gaussian_nhds_zerolemma — Analytic core of Bernstein's theorem. Under the Bernstein hypotheses with finite second moments, the characteristic functions of X and Y coincide, on a neighbourhood of 0, with Gaussian characteristic functions that share one variance σ² ≥ 0 (with means mf, mg). The shared σ² — a consequence of the single constant c from gaussianForm_of_funeq — is exactly what the doubling bootstrap in bernstein needs to extend the Gaussian form to all of ℝ.hypothesesProof (Lean source)
lemma bernstein_charFun_gaussian_nhds_zero (mX : Measurable X) (mY : Measurable Y) (hX2 : MemLp X 2 P) (hY2 : MemLp Y 2 P) (hXY : IndepFun X Y P) (hUV : IndepFun (X + Y) (X - Y) P) : ∃ mf mg σ2 : ℝ, 0 ≤ σ2 ∧ (∀ᶠ t in nhds (0 : ℝ), charFun (P.map X) t = exp (mf * t * I - σ2 * t ^ 2 / 2)) ∧ (∀ᶠ t in nhds (0 : ℝ), charFun (P.map Y) t = exp (mg * t * I - σ2 * t ^ 2 / 2)) := by let μX := P.map X let μY := P.map Y let f := charFun μX let g := charFun μY haveI : IsProbabilityMeasure μX := Measure.isProbabilityMeasure_map mX.aemeasurable haveI : IsProbabilityMeasure μY := Measure.isProbabilityMeasure_map mY.aemeasurable have hf : ContDiff ℝ 2 f := by simpa [f, μX] using charFun_contDiff_two (P := P) (Z := X) hX2 have hg : ContDiff ℝ 2 g := by simpa [g, μY] using charFun_contDiff_two (P := P) (Z := Y) hY2 have hf0 : f 0 = 1 := by simp [f] have hg0 : g 0 = 1 := by simp [g] have hfe : ∀ u v : ℝ, f (u + v) * g (u - v) = f u * g u * (f v * g (-v)) := by intro u v simpa [f, g, μX, μY] using bernstein_charFun_funeq mX mY hXY hUV u v obtain ⟨c, hXform, hYform⟩ := gaussianForm_of_funeq hf hg hf0 hg0 hfe have hXee : f =ᶠ[nhds (0 : ℝ)] fun t : ℝ => exp (deriv f 0 * t + c * t ^ 2 / 2) := hXform have hYee : g =ᶠ[nhds (0 : ℝ)] fun t : ℝ => exp (deriv g 0 * t + c * t ^ 2 / 2) := hYform have hμX2 : MemLp id 2 μX := by exact (memLp_map_measure_iff aestronglyMeasurable_id mX.aemeasurable).2 (by simpa [μX, Function.comp_def] using hX2) have hμX1 : MemLp id 1 μX := hμX2.mono_exponent (by norm_num) have hμY2 : MemLp id 2 μY := by exact (memLp_map_measure_iff aestronglyMeasurable_id mY.aemeasurable).2 (by simpa [μY, Function.comp_def] using hY2) have hμY1 : MemLp id 1 μY := hμY2.mono_exponent (by norm_num) let mf : ℝ := ∫ x, x ∂μX let mg : ℝ := ∫ y, y ∂μY let σ2 : ℝ := variance id μX have hderivX : deriv f 0 = I * (mf : ℂ) := by have hiter := iteratedDeriv_charFun_zero (μ := μX) (n := 1) (by simpa using hμX1) rw [← iteratedDeriv_one] simpa [f, mf] using hiter have hderivY : deriv g 0 = I * (mg : ℂ) := by have hiter := iteratedDeriv_charFun_zero (μ := μY) (n := 1) (by simpa using hμY1) rw [← iteratedDeriv_one] simpa [g, mg] using hiter have hsecondX : iteratedDeriv 2 f 0 = - ((∫ x, x ^ 2 ∂μX : ℝ) : ℂ) := by have hiter := iteratedDeriv_charFun_zero (μ := μX) (n := 2) hμX2 simpa [f] using hiter have hmodelEval (a b : ℂ) : iteratedDeriv 2 (fun t : ℝ => exp (a * t + b * t ^ 2 / 2)) 0 = b + a ^ 2 := by simp only [iteratedDeriv_succ, iteratedDeriv_zero] have hderivModel : deriv (fun t : ℝ => exp (a * t + b * t ^ 2 / 2)) = fun t : ℝ => (a + b * t) * exp (a * t + b * t ^ 2 / 2) := by funext t have hcoe : HasDerivAt (fun y : ℝ => (y : ℂ)) 1 t := HasDerivAt.ofReal_comp (hasDerivAt_id t) have hp : HasDerivAt (fun t : ℝ => a * (t : ℂ) + b * (t : ℂ) ^ 2 / 2) (a + b * (t : ℂ)) t := by exact ((hcoe.const_mul a).fun_add (((hcoe.fun_pow 2).const_mul b).div_const 2)).congr_deriv (by norm_num; ring) convert hp.cexp.deriv using 1 ; ring rw [hderivModel] have hcoe0 : HasDerivAt (fun y : ℝ => (y : ℂ)) 1 0 := HasDerivAt.ofReal_comp (hasDerivAt_id 0) have hp0 : HasDerivAt (fun t : ℝ => a * (t : ℂ) + b * (t : ℂ) ^ 2 / 2) a 0 := by exact ((hcoe0.const_mul a).fun_add (((hcoe0.fun_pow 2).const_mul b).div_const 2)).congr_deriv (by norm_num) have hlin0 : HasDerivAt (fun t : ℝ => a + b * (t : ℂ)) b 0 := by exact ((hcoe0.const_mul b).const_add a).congr_deriv (by ring) have hexp0 : HasDerivAt (fun t : ℝ => exp (a * t + b * t ^ 2 / 2)) a 0 := by exact hp0.cexp.congr_deriv (by norm_num) have hmul := (hlin0.fun_mul hexp0).deriv rw [hmul] norm_num ring have hmodelSecondX : iteratedDeriv 2 f 0 = c + (deriv f 0) ^ 2 := by calc iteratedDeriv 2 f 0 = iteratedDeriv 2 (fun t : ℝ => exp (deriv f 0 * t + c * t ^ 2 / 2)) 0 := hXee.iteratedDeriv_eq 2 _ = c + (deriv f 0) ^ 2 := hmodelEval (deriv f 0) c have hsigma : σ2 = (∫ x, x ^ 2 ∂μX) - mf ^ 2 := by simpa [σ2, mf] using (variance_eq_sub (μ := μX) (X := id) hμX2) have hc : c = - (σ2 : ℂ) := by rw [hsecondX, hderivX] at hmodelSecondX have hc' : c = - ((∫ x, x ^ 2 ∂μX : ℝ) : ℂ) - (I * (mf : ℂ)) ^ 2 := by calc c = (c + (I * (mf : ℂ)) ^ 2) - (I * (mf : ℂ)) ^ 2 := by ring _ = - ((∫ x, x ^ 2 ∂μX : ℝ) : ℂ) - (I * (mf : ℂ)) ^ 2 := by rw [← hmodelSecondX] rw [hc', hsigma] rw [Complex.ext_iff] have hI2 : I ^ 2 = (-1 : ℂ) := by rw [sq, Complex.I_mul_I] constructor · ring_nf rw [hI2] norm_num ring · ring_nf rw [hI2] norm_num refine ⟨mf, mg, σ2, variance_nonneg id μX, ?_, ?_⟩ · refine hXee.mono ?_ intro t ht change f t = exp ((mf : ℂ) * t * I - (σ2 : ℂ) * t ^ 2 / 2) rw [ht] rw [hderivX, hc] ring_nf · refine hYee.mono ?_ intro t ht change g t = exp ((mg : ℂ) * t * I - (σ2 : ℂ) * t ^ 2 / 2) rw [ht] rw [hderivY, hc] ring_nf
FiniteCellConditionalMomentBridge 7 core · 6 supporting This module provides generic probability tools for conditioning on a measurable positive-mass cell by normalizing its restricted measure. ★ normalizedRestricted_crossMomentMatrix_eq_outer
Finite-cell conditional moments
This module provides generic probability tools for conditioning on a measurable
positive-mass cell by normalizing its restricted measure. It turns bounded-test
factorization into independence and into finite-coordinate moment factorization.
The causal transfer of an outcome bound from an observed arm to a potential outcome
built on these tools lives in Causalean.PO.Assumptions.ArmSupportTransfer.
def normalizedRestrict reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, a measure on it, and a cell in that sample space, the normalized restricted measure is the measure restricted to the cell and scaled by the reciprocal of the measure of that cell.
Definition (Lean source)
parameters
def
given by
(P C)⁻¹ • P.restrict C
def normalizedRestrictedIntegral reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, a real normed vector-valued outcome space, a measure, a cell, and a function on the sample space, the normalized restricted integral is the integral of the function with respect to the normalized restricted measure of that cell.
Definition (Lean source)
parameters
def
normalizedRestrictedIntegral P C f :
E
given by
∫ ω, f ω ∂normalizedRestrict P C
def BoundedTestFactorization reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, two measurable value spaces, a measure, and two random elements, the bounded-test factorization condition holds exactly when, for every pair of measurable bounded real-valued test functions on the two value spaces, the integral of their product after applying the two random elements equals the product of their separate integrals.
Definition (Lean source)
parameters
Ω S T :
μ :
Measure Ω
X :
Ω → S
Y :
Ω → T
φ :
S → ℝ
ψ :
T → ℝ
(∃ K : ℝ, ∀ x, |φ x| ≤ K)
(∃ L : ℝ, ∀ y, |ψ y| ≤ L)
def
BoundedTestFactorization μ X Y :
Prop
given by
(∫ ω, φ (X ω) * ψ (Y ω) ∂μ) = (∫ ω, φ (X ω) ∂μ) * (∫ ω, ψ (Y ω) ∂μ)
def NormalizedRestrictedBoundedTestFactorization reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, two measurable value spaces, a measure, a cell, and two random elements, the normalized restricted bounded-test factorization condition is bounded-test factorization of those random elements under the normalized restriction of the measure to the cell.
Definition (Lean source)
parameters
def
NormalizedRestrictedBoundedTestFactorization P C X Y :
Prop
given by
BoundedTestFactorization (normalizedRestrict P C) X Y
def firstMomentVector reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, a finite vector dimension, a measure, and a finite-dimensional real random vector, the first-moment vector has at each coordinate the integral of the corresponding coordinate of the random vector.
Definition (Lean source)
parameters
def
given by
fun i => ∫ ω, X ω i ∂μ
def crossMomentMatrix reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a measurable sample space, two finite vector dimensions, a measure, and two finite-dimensional real random vectors, the cross-moment matrix has at each ordered pair of coordinates the integral of the product of the corresponding coordinates of the two random vectors.
theorem normalizedRestricted_crossMomentMatrix_eq_outer reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a measurable positive-mass cell, measurable finite-coordinate random vectors, integrable individual coordinates, and factorization of every bounded measurable test under the normalized cell law, the complete normalized cross-moment matrix is the outer product of the two normalized first-moment vectors.
Formal statement
hypotheses
Ω :
C :
Set Ω
hC :
hCpos :
0 < P C
hX :
hY :
hXint :
∀ i, Integrable (fun ω => X ω i) (normalizedRestrict P C)
hYint :
∀ j, Integrable (fun ω => Y ω j) (normalizedRestrict P C)
hfactor :
conclusion
crossMomentMatrix (normalizedRestrict P C) X Y
= vecMulVec (firstMomentVector (normalizedRestrict P C) X) (firstMomentVector (normalizedRestrict P C) Y)
Proof (Lean source)
theorem normalizedRestricted_crossMomentMatrix_eq_outer
{Ω : Type*} [MeasurableSpace Ω]
{P : Measure Ω} [IsProbabilityMeasure P]
{C : Set Ω} (hC : MeasurableSet C) (hCpos : 0 < P C)
{m n : ℕ} {X : Ω → Fin m → ℝ} {Y : Ω → Fin n → ℝ}
(hX : Measurable X) (hY : Measurable Y)
(hXint : ∀ i, Integrable (fun ω => X ω i) (normalizedRestrict P C))
(hYint : ∀ j, Integrable (fun ω => Y ω j) (normalizedRestrict P C))
(hfactor : NormalizedRestrictedBoundedTestFactorization P C X Y) :
crossMomentMatrix (normalizedRestrict P C) X Y =
vecMulVec
(firstMomentVector (normalizedRestrict P C) X)
(firstMomentVector (normalizedRestrict P C) Y) := by
ext i j
exact (normalizedRestricted_coordinate_factorization hC hCpos hX hY hXint hYint
hfactor i j).2
6 supporting declarations (lemmas, instances)
-
normalizedRestrict_isProbabilityMeasuretheorem — For a finite sampling measure, a measurable cell with strictly positive mass has a normalized restricted law that is a probability measure.Proof (Lean source)
theorem normalizedRestrict_isProbabilityMeasure {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsFiniteMeasure P] {C : Set Ω} (hC : MeasurableSet C) (hCpos : 0 < P C) : IsProbabilityMeasure (normalizedRestrict P C) := by have hCne : P C ≠ 0 := ne_of_gt hCpos have hCtop : P C ≠ ⊤ := measure_ne_top P C refine ⟨?_⟩ simp only [normalizedRestrict, Measure.smul_apply, Measure.restrict_apply_univ] exact ENNReal.inv_mul_cancel hCne hCtop -
normalizedRestrict_applytheorem — For a positive-mass cell and a measurable event, the normalized cell law of that event is its intersection mass divided by the cell mass.hypothesesconclusionnormalizedRestrict P C A = (P C)⁻¹ * P (A ∩ C)Proof (Lean source)
theorem normalizedRestrict_apply {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsFiniteMeasure P] {C A : Set Ω} (hCpos : 0 < P C) (hA : MeasurableSet A) : normalizedRestrict P C A = (P C)⁻¹ * P (A ∩ C) := by simp [normalizedRestrict, Measure.smul_apply, Measure.restrict_apply hA] -
normalizedRestrictedIntegral_eqtheorem — On a positive-mass cell, integrating a function under the normalized cell law is the restricted integral rescaled by the reciprocal cell mass.hypothesesconclusionnormalizedRestrictedIntegral P C f = (P C).toReal⁻¹ • ∫ ω in C, f ω ∂PProof (Lean source)
theorem normalizedRestrictedIntegral_eq {Ω E : Type*} [MeasurableSpace Ω] [NormedAddCommGroup E] [NormedSpace ℝ E] {P : Measure Ω} [IsFiniteMeasure P] {C : Set Ω} (hCpos : 0 < P C) (f : Ω → E) : normalizedRestrictedIntegral P C f = (P C).toReal⁻¹ • ∫ ω in C, f ω ∂P := by simp [normalizedRestrictedIntegral, normalizedRestrict, MeasureTheory.integral_smul_measure, ENNReal.toReal_inv] -
ae_normalizedRestrict_ifftheorem — On a positive-mass cell, an almost-sure assertion holds under the normalized cell law exactly when it holds under the unnormalized restricted measure.hypothesesconclusion(∀ᵐ ω ∂normalizedRestrict P C, p ω) ↔ (∀ᵐ ω ∂P.restrict C, p ω)Proof (Lean source)
theorem ae_normalizedRestrict_iff {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsFiniteMeasure P] {C : Set Ω} (hCpos : 0 < P C) {p : Ω → Prop} : (∀ᵐ ω ∂normalizedRestrict P C, p ω) ↔ (∀ᵐ ω ∂P.restrict C, p ω) := by have hscale : 0 < (P C)⁻¹ ∧ (P C)⁻¹ < ⊤ := ⟨ ENNReal.inv_pos.mpr (measure_ne_top P C), ENNReal.inv_lt_top.mpr hCpos⟩ rw [normalizedRestrict] exact Measure.ae_ennreal_smul_measure_iff hscale.1.ne' -
indepFun_of_boundedTestFactorizationtheorem — Under a probability law, measurable random elements whose all bounded measurable real-valued tests factor are independent.hypothesesconclusionIndepFun X Y μProof (Lean source)
theorem indepFun_of_boundedTestFactorization {Ω S T : Type*} [MeasurableSpace Ω] [MeasurableSpace S] [MeasurableSpace T] {μ : Measure Ω} [IsProbabilityMeasure μ] {X : Ω → S} {Y : Ω → T} (hX : Measurable X) (hY : Measurable Y) (hfactor : BoundedTestFactorization μ X Y) : IndepFun X Y μ := by rw [indepFun_iff_indepSet_preimage hX hY] intro s t hs ht have hsX : MeasurableSet (X ⁻¹' s) := hX hs have htY : MeasurableSet (Y ⁻¹' t) := hY ht rw [indepSet_iff_measure_inter_eq_mul hsX htY μ] apply (ENNReal.toReal_eq_toReal_iff' (measure_ne_top μ (X ⁻¹' s ∩ Y ⁻¹' t)) (ENNReal.mul_ne_top (measure_ne_top μ (X ⁻¹' s)) (measure_ne_top μ (Y ⁻¹' t)))).mp rw [ENNReal.toReal_mul, ← measureReal_def, ← measureReal_def, ← measureReal_def, ← integral_indicator_one (hsX.inter htY), ← integral_indicator_one hsX, ← integral_indicator_one htY] have hfac := hfactor (s.indicator (fun _ => (1 : ℝ))) (t.indicator (fun _ => (1 : ℝ))) (measurable_const.indicator hs) (measurable_const.indicator ht) ⟨1, by intro x; by_cases hx : x ∈ s <;> simp [indicator, hx]⟩ ⟨1, by intro y; by_cases hy : y ∈ t <;> simp [indicator, hy]⟩ have hscomp : (fun ω => s.indicator (fun _ => (1 : ℝ)) (X ω)) = (X ⁻¹' s).indicator (fun _ => 1) := by funext ω by_cases hx : X ω ∈ s <;> simp [indicator, hx] have htcomp : (fun ω => t.indicator (fun _ => (1 : ℝ)) (Y ω)) = (Y ⁻¹' t).indicator (fun _ => 1) := by funext ω by_cases hy : Y ω ∈ t <;> simp [indicator, hy] have hprod : (fun ω => s.indicator (fun _ => (1 : ℝ)) (X ω) * t.indicator (fun _ => (1 : ℝ)) (Y ω)) = (X ⁻¹' s ∩ Y ⁻¹' t).indicator (fun _ => 1) := by funext ω by_cases hx : X ω ∈ s <;> by_cases hy : Y ω ∈ t <;> simp [indicator, hx, hy] rw [hprod, hscomp, htcomp] at hfac exact hfac -
normalizedRestricted_coordinate_factorizationtheorem — For a measurable positive-mass cell, measurable finite-coordinate random vectors, integrable individual coordinates, and factorization of every bounded measurable test under the normalized cell law, each coordinate product is integrable and its cell cross moment factors into the two cell first moments.hypothesesΩ :C :Set ΩhC :hCpos :0 < P ChX :hY :hXint :∀ i, Integrable (fun ω => X ω i) (normalizedRestrict P C)hYint :∀ j, Integrable (fun ω => Y ω j) (normalizedRestrict P C)hfactor :i j :conclusionconclusion 1Integrable (fun ω => X ω i * Y ω j) (normalizedRestrict P C)conclusion 2normalizedRestrictedIntegral P C (fun ω => X ω i * Y ω j)= normalizedRestrictedIntegral P C (fun ω => X ω i) * normalizedRestrictedIntegral P C (fun ω => Y ω j)Proof (Lean source)
theorem normalizedRestricted_coordinate_factorization {Ω : Type*} [MeasurableSpace Ω] {P : Measure Ω} [IsProbabilityMeasure P] {C : Set Ω} (hC : MeasurableSet C) (hCpos : 0 < P C) {m n : ℕ} {X : Ω → Fin m → ℝ} {Y : Ω → Fin n → ℝ} (hX : Measurable X) (hY : Measurable Y) (hXint : ∀ i, Integrable (fun ω => X ω i) (normalizedRestrict P C)) (hYint : ∀ j, Integrable (fun ω => Y ω j) (normalizedRestrict P C)) (hfactor : NormalizedRestrictedBoundedTestFactorization P C X Y) : ∀ i j, Integrable (fun ω => X ω i * Y ω j) (normalizedRestrict P C) ∧ normalizedRestrictedIntegral P C (fun ω => X ω i * Y ω j) = normalizedRestrictedIntegral P C (fun ω => X ω i) * normalizedRestrictedIntegral P C (fun ω => Y ω j) := by let _ : IsProbabilityMeasure (normalizedRestrict P C) := normalizedRestrict_isProbabilityMeasure hC hCpos have hInd : IndepFun X Y (normalizedRestrict P C) := indepFun_of_boundedTestFactorization hX hY hfactor intro i j have hcoordInd : IndepFun (fun ω => X ω i) (fun ω => Y ω j) (normalizedRestrict P C) := by simpa only [Function.comp_def] using hInd.comp (measurable_pi_apply i) (measurable_pi_apply j) constructor · change Integrable ((fun ω => X ω i) * (fun ω => Y ω j)) (normalizedRestrict P C) exact hcoordInd.integrable_mul (hXint i) (hYint j) · simpa only [normalizedRestrictedIntegral, Pi.mul_apply] using hcoordInd.integral_mul_eq_mul_integral (hXint i).1 (hYint j).1
FiniteMarkovOscillation 5 core · 7 supporting This module provides the backward action of a finite stochastic matrix on functions and the duality between total-variation contraction of distributions and oscillation contraction of functions. ★ oscillationBound_markovOperatorIter
Finite Markov operators and oscillation contraction
This module provides the backward action of a finite stochastic matrix on functions and the
duality between total-variation contraction of distributions and oscillation contraction of
functions. It reuses the finite probability vectors and forward Markov steps from
CertifiedFiniteMarkovExpectation.FiniteKernel.
def markovOperator reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkovOscillation
Given a finite transition matrix, a real-valued function, and a starting state, the backward Markov operator is the transition-weighted sum of the function.
Definition (Lean source)
parameters
def
markovOperator P f s :
ℝ
given by
∑ s', P s s' * f s'
def markovOperatorIter reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkovOscillation
Given a finite transition matrix, the iterated backward Markov operator applies the matrix a specified number of times to a real-valued function.
Definition (Lean source)
def OscillationBound reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkovOscillation
Given an upper bound and a real-valued function, the function has pairwise oscillation at most that bound when every two values differ by at most it.
Definition (Lean source)
parameters
S :
Type*
B :
ℝ
f :
S → ℝ
x y :
def
OscillationBound B f :
Prop
given by
|f x - f y| ≤ B
lemma oscillationBound_markovOperatorIter reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkovOscillation
Given a finite stochastic matrix, a nonnegative contraction coefficient, half-ℓ¹ contraction of its forward action, an initial oscillation bound, and a number of steps, the iterated backward operator's oscillation is bounded by the coefficient raised to the number of steps times the initial bound, which decays geometrically when the coefficient is below one.
Formal statement
hypotheses
S :
P :
S → S → ℝ
hP :
∀ s, IsProbabilityVector (P s)
alpha B :
ℝ
halpha :
0 ≤ alpha
hcontract :
∀ p q
and
then
(1 / 2 : ℝ) * ∑ s, |markovStep p P s - markovStep q P s|
≤ alpha * ((1 / 2 : ℝ) * ∑ s, |p s - q s|)
f :
S → ℝ
hf :
OscillationBound B f
n :
conclusion
OscillationBound (alpha ^ n * B) (markovOperatorIter P n f)
Proof (Lean source)
lemma oscillationBound_markovOperatorIter {S : Type*} [Fintype S] [Nonempty S]
(P : S → S → ℝ) (hP : ∀ s, IsProbabilityVector (P s))
{alpha B : ℝ} (halpha : 0 ≤ alpha)
(hcontract : ∀ p q, IsProbabilityVector p → IsProbabilityVector q →
(1 / 2 : ℝ) * ∑ s, |markovStep p P s - markovStep q P s| ≤
alpha * ((1 / 2 : ℝ) * ∑ s, |p s - q s|))
{f : S → ℝ} (hf : OscillationBound B f) (n : Nat) :
OscillationBound (alpha ^ n * B) (markovOperatorIter P n f) := by
induction n with
| zero => simpa [markovOperatorIter] using hf
| succ n ih =>
simpa [markovOperatorIter, pow_succ, mul_assoc, mul_left_comm, mul_comm] using
oscillationBound_markovOperator P hP halpha hcontract ih
def nonemptyOfProbabilityVector reviewed
⚑ flagged
Causalean.Mathlib.Probability.FiniteMarkovOscillation
Given a real vector on a finite carrier that is a probability vector, the carrier is nonempty.
Definition (Lean source)
parameters
def
nonemptyOfProbabilityVector p hp :
Nonempty S
given by
by classical by_contra hempty haveI : IsEmpty S := not_nonempty_iff.mp hempty have := hp.2 simpa using this
7 supporting declarations (lemmas, instances)
-
markovOperatorIter_succlemma — For a finite transition matrix, a step count, and a function, the successor iterate is one backward Markov step after the preceding iterate.hypothesesconclusionProof (Lean source)
lemma markovOperatorIter_succ {S : Type*} [Fintype S] (P : S → S → ℝ) (n : Nat) (f : S → ℝ) : markovOperatorIter P (n + 1) f = markovOperator P (markovOperatorIter P n f) := rfl -
oscillationBound_nonneglemma — If a function has an oscillation bound, that bound is nonnegative.Proof (Lean source)
lemma oscillationBound_nonneg {S : Type*} [Nonempty S] {B : ℝ} {f : S → ℝ} (h : OscillationBound B f) : 0 ≤ B := by let x : S := choice inferInstance simpa using h x x -
abs_sum_sub_mul_le_oscillation_halfL1lemma — Given two finite probability vectors and a function with oscillation at most B, the difference of their expectations is at most B times half their ℓ¹ distance.hypothesesconclusion|∑ s, (p s - q s) * f s| ≤ B * ((1 / 2 : ℝ) * ∑ s, |p s - q s|)Proof (Lean source)
lemma abs_sum_sub_mul_le_oscillation_halfL1 {S : Type*} [Fintype S] [Nonempty S] {p q : S → ℝ} (hp : IsProbabilityVector p) (hq : IsProbabilityVector q) {B : ℝ} {f : S → ℝ} (hf : OscillationBound B f) : |∑ s, (p s - q s) * f s| ≤ B * ((1 / 2 : ℝ) * ∑ s, |p s - q s|) := by obtain ⟨imin, -, hmin⟩ := Finset.exists_min_image univ f Finset.univ_nonempty obtain ⟨imax, -, hmax⟩ := Finset.exists_max_image univ f Finset.univ_nonempty have hB0 := oscillationBound_nonneg hf have hspan : f imax - f imin ≤ B := by have := hf imax imin exact (le_abs_self (f imax - f imin)).trans this let c : ℝ := (f imin + f imax) / 2 have hcenter (s : S) : |f s - c| ≤ B / 2 := by have hlo : f imin ≤ f s := hmin s (Finset.mem_univ s) have hhi : f s ≤ f imax := hmax s (Finset.mem_univ s) rw [abs_le] constructor <;> dsimp [c] <;> linarith have hsum0 : ∑ s, (p s - q s) = 0 := by rw [Finset.sum_sub_distrib, hp.2, hq.2, sub_self] calc |∑ s, (p s - q s) * f s| = |∑ s, (p s - q s) * (f s - c)| := by congr 1 rw [show (∑ s, (p s - q s) * (f s - c)) = (∑ s, (p s - q s) * f s) - (∑ s, (p s - q s)) * c by calc _ = ∑ s, ((p s - q s) * f s - (p s - q s) * c) := by apply Finset.sum_congr rfl intro s _ ring _ = (∑ s, (p s - q s) * f s) - ∑ s, (p s - q s) * c := by rw [Finset.sum_sub_distrib] _ = _ := by rw [← Finset.sum_mul]] rw [hsum0, zero_mul, sub_zero] _ ≤ ∑ s, |(p s - q s) * (f s - c)| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ s, |p s - q s| * (B / 2) := by apply Finset.sum_le_sum intro s _ rw [abs_mul] exact mul_le_mul_of_nonneg_left (hcenter s) (abs_nonneg _) _ = B * ((1 / 2 : ℝ) * ∑ s, |p s - q s|) := by simp only [← Finset.sum_mul] ring -
isProbabilityVector_indicatorlemma — For a state, its point mass is a finite probability vector.Proof (Lean source)
lemma isProbabilityVector_indicator {S : Type*} [Fintype S] [DecidableEq S] (x : S) : IsProbabilityVector (fun y : S ↦ if y = x then 1 else 0) := by constructor · intro y by_cases hy : y = x <;> simp [hy] · simp -
halfL1_indicator_sub_indicator_le_onelemma — For two states, half the ℓ¹ distance between their point masses is at most one.hypothesesS :x y :Sconclusion(1 / 2 : ℝ) * ∑ z, |(if z = x then 1 else 0) - (if z = y then 1 else 0)| ≤ 1Proof (Lean source)
lemma halfL1_indicator_sub_indicator_le_one {S : Type*} [Fintype S] [DecidableEq S] (x y : S) : (1 / 2 : ℝ) * ∑ z, |(if z = x then 1 else 0) - (if z = y then 1 else 0)| ≤ 1 := by let px : S → ℝ := fun z ↦ if z = x then 1 else 0 let py : S → ℝ := fun z ↦ if z = y then 1 else 0 have hpoint (z : S) : |px z - py z| ≤ px z + py z := by calc _ ≤ |px z| + |py z| := abs_sub _ _ _ = _ := by rw [abs_of_nonneg, abs_of_nonneg] · by_cases hz : z = y <;> simp [py, hz] · by_cases hz : z = x <;> simp [px, hz] change (1 / 2 : ℝ) * ∑ z, |px z - py z| ≤ 1 calc _ ≤ (1 / 2 : ℝ) * ∑ z, (px z + py z) := by apply mul_le_mul_of_nonneg_left _ (by norm_num) exact Finset.sum_le_sum fun z _ ↦ hpoint z _ = 1 := by rw [Finset.sum_add_distrib] have hx : ∑ z, px z = 1 := by simpa [px] using (isProbabilityVector_indicator x).2 have hy : ∑ z, py z = 1 := by simpa [py] using (isProbabilityVector_indicator y).2 rw [hx, hy] norm_num -
oscillationBound_markovOperatorlemma — Given a finite stochastic matrix, a nonnegative contraction coefficient, half-ℓ¹ contraction of its forward action, and a function with oscillation at most B, one backward Markov step has oscillation at most alpha * B.hypothesesS :P :S → S → ℝhP :∀ s, IsProbabilityVector (P s)alpha B :ℝhalpha :0 ≤ alphahcontract :∀ p qandthen(1 / 2 : ℝ) * ∑ s, |markovStep p P s - markovStep q P s|≤ alpha * ((1 / 2 : ℝ) * ∑ s, |p s - q s|)f :S → ℝhf :OscillationBound B fconclusionOscillationBound (alpha * B) (markovOperator P f)Proof (Lean source)
lemma oscillationBound_markovOperator {S : Type*} [Fintype S] [Nonempty S] (P : S → S → ℝ) (hP : ∀ s, IsProbabilityVector (P s)) {alpha B : ℝ} (halpha : 0 ≤ alpha) (hcontract : ∀ p q, IsProbabilityVector p → IsProbabilityVector q → (1 / 2 : ℝ) * ∑ s, |markovStep p P s - markovStep q P s| ≤ alpha * ((1 / 2 : ℝ) * ∑ s, |p s - q s|)) {f : S → ℝ} (hf : OscillationBound B f) : OscillationBound (alpha * B) (markovOperator P f) := by classical intro x y let px : S → ℝ := fun z ↦ if z = x then 1 else 0 let py : S → ℝ := fun z ↦ if z = y then 1 else 0 have hpx : IsProbabilityVector px := isProbabilityVector_indicator x have hpy : IsProbabilityVector py := isProbabilityVector_indicator y have happx : markovStep px P = P x := by funext z simp [markovStep, vecMul, dotProduct, px] have happy : markovStep py P = P y := by funext z simp [markovStep, vecMul, dotProduct, py] have htv : (1 / 2 : ℝ) * ∑ s, |P x s - P y s| ≤ alpha := by have hc := hcontract px py hpx hpy rw [happx, happy] at hc exact hc.trans (by simpa [px, py] using mul_le_mul_of_nonneg_left (halfL1_indicator_sub_indicator_le_one x y) halpha) have hdual := abs_sum_sub_mul_le_oscillation_halfL1 (hP x) (hP y) hf unfold markovOperator rw [← Finset.sum_sub_distrib] calc |∑ s, (P x s * f s - P y s * f s)| = |∑ s, (P x s - P y s) * f s| := by congr 1 apply Finset.sum_congr rfl intro s _ ring _ ≤ B * ((1 / 2 : ℝ) * ∑ s, |P x s - P y s|) := hdual _ ≤ B * alpha := mul_le_mul_of_nonneg_left htv (oscillationBound_nonneg hf) _ = alpha * B := mul_comm _ _ -
monolemma — If a function has oscillation at most A and A is at most B, the function has oscillation at most B.hypothesesconclusionOscillationBound B fProof (Lean source)
lemma OscillationBound.mono {S : Type*} {A B : ℝ} {f : S → ℝ} (hf : OscillationBound A f) (hAB : A ≤ B) : OscillationBound B f := fun x y ↦ (hf x y).trans hAB
FinitePartitionConditional 1 core · 1 supporting This module provides the law of total probability over a finite measurable partition, written with Mathlib's conditional measure μ[E | C], and its uniform-bound consequence: a bound on the conditional probability of an e ★ measure_le_of_cond_le_on_finite_partition
Finite-partition aggregation of conditional probabilities
This module provides the law of total probability over a finite measurable partition, written with
Mathlib's conditional measure μ[E | C], and its uniform-bound consequence: a bound on the
conditional probability of an event in every positive-probability cell bounds its unconditional
probability. Zero-probability cells are handled explicitly, so applications only need conditional
estimates on positive-probability cells.
theorem measure_le_of_cond_le_on_finite_partition reviewed
⚑ flagged
Causalean.Mathlib.Probability
Given a probability measure, a finite collection of cells, measurability of every cell, pairwise disjointness of distinct cells, coverage of the whole sample space, an event, measurability of that event, a probability bound, and that bound conditional on each positive-mass cell, the unconditional event probability is at most the same bound.
Formal statement
hypotheses
Ω ι :
μ :
C :
ι → Set Ω
hC :
∀ i, MeasurableSet (C i)
hdisj :
∀ i j
if
i ≠ j
then
Disjoint (C i) (C j)
hcover :
(⋃ i, C i) = univ
E :
Set Ω
hE :
β :
ℝ≥0∞
hcond :
∀ i
if
μ (C i) ≠ 0
then
μ[E | C i] ≤ β
conclusion
μ E ≤ β
Proof (Lean source)
theorem measure_le_of_cond_le_on_finite_partition
{Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι]
(μ : Measure Ω) [IsProbabilityMeasure μ] (C : ι → Set Ω)
(hC : ∀ i, MeasurableSet (C i))
(hdisj : ∀ i j, i ≠ j → Disjoint (C i) (C j))
(hcover : (⋃ i, C i) = univ) (E : Set Ω) (hE : MeasurableSet E)
(β : ℝ≥0∞) (hcond : ∀ i, μ (C i) ≠ 0 → μ[E | C i] ≤ β) :
μ E ≤ β := by
-- Insert the exact finite sum, bound positive cells by `β`, and use that cell masses sum to one.
rw [measure_eq_sum_mul_cond_of_finite_partition μ C hC hdisj hcover E hE]
calc
∑ i, μ (C i) * μ[E | C i] ≤ ∑ i, μ (C i) * β := by
apply Finset.sum_le_sum
intro i _
by_cases hzero : μ (C i) = 0
· simp [hzero]
· simpa [mul_comm] using mul_le_mul_left (hcond i hzero) (μ (C i))
_ = (∑ i, μ (C i)) * β := by rw [Finset.sum_mul]
_ = 1 * β := by
have hmass : ∑ i, μ (C i) = 1 := by
simpa only [hcover, measure_univ, tsum_fintype] using
(measure_iUnion (μ := μ) (fun i j hij ↦ hdisj i j hij) hC).symm
rw [hmass]
_ = β := one_mul β
1 supporting declaration (lemmas, instances)
-
measure_eq_sum_mul_cond_of_finite_partitiontheorem — Given a probability measure, a finite collection of cells, measurability of every cell, pairwise disjointness of distinct cells, coverage of the whole sample space, an event, and measurability of that event, its probability equals the finite sum of cell mass times conditional event probability.hypothesesΩ ι :μ :C :ι → Set ΩhC :∀ i, MeasurableSet (C i)hdisj :∀ i jifi ≠ jthenDisjoint (C i) (C j)hcover :(⋃ i, C i) = univE :Set ΩhE :conclusionμ E = ∑ i, μ (C i) * μ[E | C i]Proof (Lean source)
theorem measure_eq_sum_mul_cond_of_finite_partition {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (C : ι → Set Ω) (hC : ∀ i, MeasurableSet (C i)) (hdisj : ∀ i j, i ≠ j → Disjoint (C i) (C j)) (hcover : (⋃ i, C i) = univ) (E : Set Ω) (hE : MeasurableSet E) : μ E = ∑ i, μ (C i) * μ[E | C i] := by -- Split `E` across the disjoint cover, then expand `cond_apply`; zero cells cancel separately. have hdisj_inter : Pairwise (fun i j ↦ Disjoint (C i ∩ E) (C j ∩ E)) := by intro i j hij exact (hdisj i j hij).mono inter_subset_left inter_subset_left calc μ E = μ ((⋃ i, C i) ∩ E) := by rw [hcover, univ_inter] _ = μ (⋃ i, C i ∩ E) := by rw [iUnion_inter] _ = ∑' i, μ (C i ∩ E) := measure_iUnion hdisj_inter fun i ↦ (hC i).inter hE _ = ∑ i, μ (C i ∩ E) := tsum_fintype (L := .unconditional ι) (fun i ↦ μ (C i ∩ E)) _ = ∑ i, μ (C i) * μ[E | C i] := by apply Finset.sum_congr rfl intro i _ by_cases hzero : μ (C i) = 0 · have hinter : μ (C i ∩ E) = 0 := measure_mono_null inter_subset_left hzero simp [hzero, hinter] · rw [cond_apply (hC i), ← mul_assoc, ENNReal.mul_inv_cancel hzero (measure_ne_top μ (C i)), one_mul]
GaussianMoments 2 core · 6 supporting This file lifts standard-normal tail identities to a real Gaussian law N(m, v) with variance parameter v > 0. ★ gaussianReal_Ioi_eq★ integral_Ioi_id_gaussianReal
General Gaussian survival and truncated first moment
This file lifts standard-normal tail identities to a real Gaussian law N(m, v) with
variance parameter v > 0. The proofs use the affine change of variables
y = m + sqrt v * z from the standard normal and reuse the standard-normal survival and
truncated-moment formulas.
The public results are:
* gaussianReal_Ioi_eq: the right-tail probability
(gaussianReal m v) (Ioi c) is 1 - stdNormalCDF ((c - m) / sqrt v);
* integral_Ioi_id_gaussianReal: the truncated first moment over (c, infinity) is
`m * (1 - stdNormalCDF ((c - m) / sqrt v))
+ sqrt v * stdNormalPDF ((c - m) / sqrt v)`.
lemma gaussianReal_Ioi_eq reviewed
⚑ flagged
Causalean.Mathlib
Gaussian survival. For a normal law with mean m and a nonnegative variance parameter v that is nonzero, the probability mass above a threshold c equals one minus the standard-normal CDF evaluated at the standardized threshold (c − m)/√v.
Formal statement
hypotheses
m :
ℝ
v :
ℝ≥0
hv :
v ≠ 0
c :
ℝ
conclusion
Proof (Lean source)
lemma gaussianReal_Ioi_eq (m : ℝ) (v : ℝ≥0) (hv : v ≠ 0) (c : ℝ) :
((gaussianReal m v) (Ioi c)).toReal
= 1 - stdNormalCDF ((c - m) / sqrt (v : ℝ)) := by
let s : ℝ := sqrt (v : ℝ)
let t : ℝ := (c - m) / s
have hvpos_nn : (0 : ℝ≥0) < v := by
exact bot_lt_iff_ne_bot.mpr hv
have hvpos : 0 < (v : ℝ) := by
exact_mod_cast hvpos_nn
have hspos : 0 < s := by
dsimp [s]
exact Real.sqrt_pos.2 hvpos
have hpre : (fun z : ℝ => s * z + m) ⁻¹' Ioi c = Ioi t := by
simpa [t] using affine_preimage_Ioi (s := s) (c := c) (m := m) hspos
calc
((gaussianReal m v) (Ioi c)).toReal
= (((gaussianReal 0 1).map (fun z : ℝ => s * z + m)) (Ioi c)).toReal := by
rw [gaussianReal_eq_map_std m v]
_ = ((gaussianReal 0 1) (Ioi t)).toReal := by
rw [Measure.map_apply]
· rw [hpre]
· exact (continuous_const.mul continuous_id |>.add continuous_const).measurable
· exact measurableSet_Ioi
_ = ∫ x in Ioi t, stdNormalPDF x := stdNormalMeasure_Ioi_toReal_eq_integral t
_ = 1 - stdNormalCDF t := integral_Ioi_stdNormalPDF t
_ = 1 - stdNormalCDF ((c - m) / sqrt (v : ℝ)) := by rfl
lemma integral_Ioi_id_gaussianReal reviewed
⚑ flagged
Causalean.Mathlib
Gaussian truncated first moment. For a normal law with mean m and a nonnegative variance parameter v that is nonzero, the first moment integrated over the tail above a threshold c equals m·(1 − Φ(t)) + √v·φ(t), where t = (c − m)/√v — the affine image of the standard-normal truncated moment ∫_{t}^∞ z φ(z) dz = φ(t).
Formal statement
hypotheses
m :
ℝ
v :
ℝ≥0
hv :
v ≠ 0
c :
ℝ
conclusion
∫ y in Ioi c, y ∂(gaussianReal m v)
= m * (1 - stdNormalCDF ((c - m) / sqrt (v : ℝ)))
Proof (Lean source)
lemma integral_Ioi_id_gaussianReal (m : ℝ) (v : ℝ≥0) (hv : v ≠ 0) (c : ℝ) :
∫ y in Ioi c, y ∂(gaussianReal m v)
= m * (1 - stdNormalCDF ((c - m) / sqrt (v : ℝ)))
+ sqrt (v : ℝ) * stdNormalPDF ((c - m) / sqrt (v : ℝ)) := by
let s : ℝ := sqrt (v : ℝ)
let t : ℝ := (c - m) / s
have hvpos_nn : (0 : ℝ≥0) < v := by
exact bot_lt_iff_ne_bot.mpr hv
have hvpos : 0 < (v : ℝ) := by
exact_mod_cast hvpos_nn
have hspos : 0 < s := by
dsimp [s]
exact Real.sqrt_pos.2 hvpos
have hpre : (fun z : ℝ => s * z + m) ⁻¹' Ioi c = Ioi t := by
simpa [t] using affine_preimage_Ioi (s := s) (c := c) (m := m) hspos
calc
∫ y in Ioi c, y ∂(gaussianReal m v)
= ∫ y in Ioi c, y ∂Measure.map
(fun z : ℝ => s * z + m) (gaussianReal 0 1) := by
rw [gaussianReal_eq_map_std m v]
_ = ∫ z in (fun z : ℝ => s * z + m) ⁻¹' Ioi c,
(s * z + m) ∂(gaussianReal 0 1) := by
rw [setIntegral_map]
· exact measurableSet_Ioi
· exact continuous_id.aestronglyMeasurable
· exact
(continuous_const.mul continuous_id |>.add continuous_const).measurable.aemeasurable
_ = ∫ z in Ioi t, (s * z + m) ∂(gaussianReal 0 1) := by
rw [hpre]
_ = ∫ z in Ioi t, gaussianPDFReal 0 1 z * (s * z + m) :=
integral_Ioi_affine_gaussianReal_eq_density s m t
_ = s * (∫ z in Ioi t, z * stdNormalPDF z)
+ m * (∫ z in Ioi t, stdNormalPDF z) :=
integral_Ioi_affine_stdNormal s m t
_ = s * stdNormalPDF t + m * (1 - stdNormalCDF t) := by
rw [integral_Ioi_id_mul_stdNormalPDF, integral_Ioi_stdNormalPDF]
_ = m * (1 - stdNormalCDF ((c - m) / sqrt (v : ℝ)))
+ sqrt (v : ℝ) * stdNormalPDF ((c - m) / sqrt (v : ℝ)) := by
dsimp [s, t]
ring
6 supporting declarations (lemmas, instances)
-
gaussianReal_eq_map_stdlemma — A real Gaussian distribution with nonnegative variance is the standard normal distribution after scaling by the standard deviation and shifting by the mean.hypothesesm :ℝv :ℝ≥0conclusionProof (Lean source)
lemma gaussianReal_eq_map_std (m : ℝ) (v : ℝ≥0) : gaussianReal m v = (gaussianReal 0 1).map (fun z => sqrt (v : ℝ) * z + m) := by have hcoe : (⟨(v : ℝ), v.2⟩ : ℝ≥0) = v := by ext simp calc gaussianReal m v = gaussianReal (0 + m) v := by simp _ = (gaussianReal 0 v).map (· + m) := by rw [gaussianReal_map_add_const] _ = ((gaussianReal 0 1).map (sqrt (v : ℝ) * ·)).map (· + m) := by congr 1 rw [gaussianReal_map_const_mul] simp [hcoe] _ = (gaussianReal 0 1).map (fun z => sqrt (v : ℝ) * z + m) := by rw [Measure.map_map] · rfl · exact (continuous_id.add continuous_const).measurable · exact (continuous_const.mul continuous_id).measurable -
affine_preimage_Ioilemma — The inverse image of a right-hand tail under a positive affine transformation is a right-hand tail whose threshold is transformed by the inverse affine formula.hypothesesα :hs :0 < sProof (Lean source)
lemma affine_preimage_Ioi {α : Type*} [Field α] [LinearOrder α] [IsStrictOrderedRing α] {s c m : α} (hs : 0 < s) : (fun z : α => s * z + m) ⁻¹' Ioi c = Ioi ((c - m) / s) := by ext z dsimp [preimage, Ioi] constructor · intro hz have hz' : c - m < z * s := by nlinarith exact (div_lt_iff₀ hs).2 hz' · intro hz have hz' : c - m < z * s := (div_lt_iff₀ hs).1 hz nlinarith [hz'] -
stdNormalMeasure_Ioi_toReal_eq_integrallemma — The standard normal probability of values above t equals the integral of the standard-normal density over that upper-tail region.Proof (Lean source)
lemma stdNormalMeasure_Ioi_toReal_eq_integral (t : ℝ) : ((gaussianReal 0 1) (Ioi t)).toReal = ∫ x in Ioi t, stdNormalPDF x := by have hmeasure := ProbabilityTheory.gaussianReal_apply_eq_integral (μ := 0) (v := 1) (by norm_num) (Ioi t) have hnonneg : 0 ≤ ∫ x in Ioi t, gaussianPDFReal 0 1 x := by exact integral_nonneg fun x => gaussianPDFReal_nonneg 0 1 x rw [hmeasure] rw [ENNReal.toReal_ofReal hnonneg] simp [stdNormalPDF] -
integrable_id_mul_stdNormalPDFlemma — The standard normal density has a finite first absolute moment.conclusionIntegrable (fun x : ℝ => x * stdNormalPDF x)Proof (Lean source)
@[fun_prop] lemma integrable_id_mul_stdNormalPDF : Integrable (fun x : ℝ => x * stdNormalPDF x) := by have hbase : Integrable (fun x : ℝ => x * exp (-(1 / 2 : ℝ) * x ^ 2)) := by simpa using integrable_mul_exp_neg_mul_sq (b := (1 / 2 : ℝ)) (by norm_num) have hpdf : ∀ x : ℝ, gaussianPDFReal 0 1 x = (sqrt (2 * π))⁻¹ * exp (-(1 / 2 : ℝ) * x ^ 2) := by intro x unfold gaussianPDFReal congr 2 · norm_num · norm_num ring convert hbase.const_mul (sqrt (2 * π))⁻¹ using 1 ext x rw [stdNormalPDF, hpdf x] ring -
integral_Ioi_affine_stdNormallemma — Above a threshold, integrating an affine function against the standard-normal density equals its slope times the truncated first moment plus its intercept times the tail mass.Proof (Lean source)
lemma integral_Ioi_affine_stdNormal (s m t : ℝ) : ∫ z in Ioi t, gaussianPDFReal 0 1 z * (s * z + m) = s * (∫ z in Ioi t, z * stdNormalPDF z) + m * (∫ z in Ioi t, stdNormalPDF z) := by have h_int_id : Integrable (fun z : ℝ => z * stdNormalPDF z) (volume.restrict (Ioi t)) := integrable_id_mul_stdNormalPDF.integrableOn have h_int_pdf : Integrable (fun z : ℝ => stdNormalPDF z) (volume.restrict (Ioi t)) := by exact ((integrable_gaussianPDFReal 0 1).integrableOn : Integrable (fun z : ℝ => gaussianPDFReal 0 1 z) (volume.restrict (Ioi t))) calc ∫ z in Ioi t, gaussianPDFReal 0 1 z * (s * z + m) = ∫ z in Ioi t, (s * (z * stdNormalPDF z) + m * stdNormalPDF z) := by congr 1 ext z simp [stdNormalPDF] ring _ = (∫ z in Ioi t, s * (z * stdNormalPDF z)) + ∫ z in Ioi t, m * stdNormalPDF z := by rw [integral_add] · exact h_int_id.const_mul s · exact h_int_pdf.const_mul m _ = s * (∫ z in Ioi t, z * stdNormalPDF z) + m * (∫ z in Ioi t, stdNormalPDF z) := by rw [integral_const_mul, integral_const_mul] -
integral_Ioi_affine_gaussianReal_eq_densitylemma — Above a threshold, the integral of an affine function under the standard-normal law equals the integral of that function against its density.hypothesess m t :ℝconclusion∫ z in Ioi t, (s * z + m) ∂(gaussianReal 0 1)= ∫ z in Ioi t, gaussianPDFReal 0 1 z * (s * z + m)Proof (Lean source)
lemma integral_Ioi_affine_gaussianReal_eq_density (s m t : ℝ) : ∫ z in Ioi t, (s * z + m) ∂(gaussianReal 0 1) = ∫ z in Ioi t, gaussianPDFReal 0 1 z * (s * z + m) := by rw [ProbabilityTheory.gaussianReal_of_var_ne_zero] · rw [setIntegral_withDensity_eq_setIntegral_toReal_smul] · congr 1 ext z simp [ProbabilityTheory.gaussianPDF, ENNReal.toReal_ofReal, gaussianPDFReal_nonneg] · exact ProbabilityTheory.measurable_gaussianPDF 0 1 · exact ae_of_all _ fun _ => ProbabilityTheory.gaussianPDF_lt_top · exact measurableSet_Ioi · norm_num
IidMeanVariance 1 core · 15 supporting This module gives the exact mean and variance of an i.i.d. ★ iid_mean_euclidean_abs_le
Moments and deviation bounds for i.i.d. empirical means
This module gives the exact mean and variance of an i.i.d. empirical average,
as well as scalar and finite-dimensional L² and L¹ deviation bounds under
the corresponding moment assumptions.
The sample index is an arbitrary nonempty finite type; the sample size is then
its cardinality. Each result also has a Fin n specialisation under the
unprimed classical name, so that callers indexing a sample by a Finset
subtype or by a fold of a cross-fitting partition can use the same lemmas.
The file also records the integrability / L²-membership side conditions of the
Euclidean deviation bound as public lemmas, since they are needed whenever the
bound is combined with another integral estimate.
theorem iid_mean_euclidean_abs_le reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a strictly positive sample size n and finitely many square-integrable real-valued statistics indexed by k, each observed on the same n-point independent, identically distributed sample, the expected Euclidean norm of the vector of centered sample averages — one coordinate per statistic — is at most the square root of the sum of the population second moments divided by n.
Formal statement
hypotheses
Proof (Lean source)
theorem iid_mean_euclidean_abs_le {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι]
(μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n)
(ξ : ι → Ω → ℝ) (hξ : ∀ k, MemLp (ξ k) 2 μ) :
∫ s, sqrt (∑ k : ι,
((n : ℝ)⁻¹ * (∑ i : Fin n, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2)
∂(Measure.pi fun _ : Fin n => μ) ≤
sqrt ((∑ k : ι, ∫ ω, (ξ k ω) ^ 2 ∂μ) / (n : ℝ)) := by
haveI : Nonempty (Fin n) := Fin.pos_iff_nonempty.mp hn
simpa using
iid_mean_euclidean_abs_le_fintype (ι := Fin n) (κ := ι) μ ξ hξ
15 supporting declarations (lemmas, instances)
-
sqrt_sum_sq_le_sum_abslemma — The Euclidean length of a finite real-valued vector is no greater than the sum of the absolute values of its components.Proof (Lean source)
lemma sqrt_sum_sq_le_sum_abs {ι : Type*} [Fintype ι] (v : ι → ℝ) : sqrt (∑ i, (v i) ^ 2) ≤ ∑ i, |v i| := by rw [Real.sqrt_le_iff] refine ⟨Finset.sum_nonneg fun _ _ => abs_nonneg _, ?_⟩ simpa [sq_abs] using Finset.sum_sq_le_sq_sum_of_nonneg (s := univ) (f := fun i => |v i|) (fun _ _ => abs_nonneg _) -
integrable_euclidean_of_integrabletheorem — The Euclidean length of a finite family of integrable real functions is itself integrable.hypothesesconclusionIntegrable (fun ω => sqrt (∑ i, (v ω i) ^ 2)) μProof (Lean source)
@[fun_prop] theorem integrable_euclidean_of_integrable {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] {μ : Measure Ω} (v : Ω → ι → ℝ) (hv : ∀ i, Integrable (fun ω => v ω i) μ) : Integrable (fun ω => sqrt (∑ i, (v ω i) ^ 2)) μ := by have hsum : Integrable (fun ω => ∑ i, |v ω i|) μ := by fun_prop have hmeas : AEStronglyMeasurable (fun ω => sqrt (∑ i, (v ω i) ^ 2)) μ := by fun_prop refine hsum.mono' hmeas (ae_of_all _ fun ω => ?_) rw [Real.norm_of_nonneg (Real.sqrt_nonneg _)] exact sqrt_sum_sq_le_sum_abs (v ω) -
memLp_two_sqrt_sum_sqtheorem — The Euclidean length of a finite family of square-integrable real functions is itself square-integrable.hypothesesΩ ι :hY :∀ k, MemLp (Y k) 2 μProof (Lean source)
theorem memLp_two_sqrt_sum_sq {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] {μ : Measure Ω} {Y : ι → Ω → ℝ} (hY : ∀ k, MemLp (Y k) 2 μ) : MemLp (fun ω => sqrt (∑ k, (Y k ω) ^ 2)) 2 μ := by have hsum_int : Integrable (fun ω => ∑ k, (Y k ω) ^ 2) μ := integrable_finset_sum _ fun k _ => (hY k).integrable_sq have hR_ae : AEStronglyMeasurable (fun ω => sqrt (∑ k, (Y k ω) ^ 2)) μ := hsum_int.aemeasurable.sqrt.aestronglyMeasurable apply (memLp_two_iff_integrable_sq hR_ae).2 convert hsum_int using 1 funext ω exact Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _) -
iid_mean_sq_le_fintypetheorem — The mean squared error of a square-integrable scalar sample average from independent, identically distributed observations is at most the population second moment divided by the sample size.hypothesesconclusion∫ s, ((Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i)) - ∫ ω, ξ ω ∂μ) ^ 2 ∂(Measure.pi fun _ : ι => μ)≤ (∫ ω, (ξ ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ)Proof (Lean source)
theorem iid_mean_sq_le_fintype {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (ξ : Ω → ℝ) (hξ : MemLp ξ 2 μ) : ∫ s, ((Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i)) - ∫ ω, ξ ω ∂μ) ^ 2 ∂(Measure.pi fun _ : ι => μ) ≤ (∫ ω, (ξ ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ) := by have hcard : Fintype.card ι ≠ 0 := Fintype.card_ne_zero let P : Measure (ι → Ω) := Measure.pi fun _ : ι => μ let X : (ι → Ω) → ℝ := fun s => ∑ i : ι, ξ (s i) have hXLp : MemLp X 2 P := by simpa [X, P] using memLp_finset_sum univ fun i _ => hξ.comp_measurePreserving (measurePreserving_eval (fun _ : ι => μ) i) have hmean : ∫ s, (Fintype.card ι : ℝ)⁻¹ * X s ∂P = ∫ ω, ξ ω ∂μ := by rw [integral_const_mul] change (Fintype.card ι : ℝ)⁻¹ * ∫ s, ∑ i : ι, ξ (s i) ∂(Measure.pi fun _ : ι => μ) = _ have hsum_integral := integral_finset_sum univ fun i _ => (measurePreserving_eval (fun _ : ι => μ) i).integrable_comp_of_integrable (hξ.integrable (by norm_num)) rw [show (∫ s, ∑ i : ι, ξ (s i) ∂(Measure.pi fun _ : ι => μ)) = ∑ i : ι, ∫ s, ξ (s i) ∂(Measure.pi fun _ : ι => μ) by simpa using hsum_integral] have hcoord (i : ι) : ∫ s, ξ (s i) ∂(Measure.pi fun _ : ι => μ) = ∫ ω, ξ ω ∂μ := integral_comp_eval (μ := fun _ : ι => μ) (i := i) hξ.aestronglyMeasurable simp_rw [hcoord] simp [hcard] calc ∫ s, ((Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i)) - ∫ ω, ξ ω ∂μ) ^ 2 ∂P = variance (fun s => (Fintype.card ι : ℝ)⁻¹ * X s) P := by rw [ProbabilityTheory.variance_eq_integral] · simp only [hmean] rfl · exact hXLp.const_mul (Fintype.card ι : ℝ)⁻¹ |>.aemeasurable _ = ((Fintype.card ι : ℝ)⁻¹) ^ 2 * variance X P := by exact ProbabilityTheory.variance_const_mul _ _ _ _ = ((Fintype.card ι : ℝ)⁻¹) ^ 2 * (∑ _i : ι, variance ξ μ) := by congr 1 change variance (fun s => ∑ i : ι, ξ (s i)) (Measure.pi fun _ : ι => μ) = _ calc variance (fun s => ∑ i : ι, ξ (s i)) (Measure.pi fun _ : ι => μ) = variance (∑ i : ι, fun s => ξ (s i)) (Measure.pi fun _ : ι => μ) := by congr 1 funext s simp _ = _ := ProbabilityTheory.variance_sum_pi (fun _ : ι => hξ) _ ≤ ((Fintype.card ι : ℝ)⁻¹) ^ 2 * (∑ _i : ι, ∫ ω, (ξ ω) ^ 2 ∂μ) := by gcongr exact ProbabilityTheory.variance_le_expectation_sq hξ.aestronglyMeasurable _ = (∫ ω, (ξ ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ) := by simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp -
iid_mean_abs_le_fintypetheorem — The mean absolute error of a square-integrable scalar sample average from independent, identically distributed observations is at most the square root of the population second moment divided by the sample size.hypothesesconclusion∫ s, |(Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i))- ∫ ω, ξ ω ∂μ| ∂(Measure.pi fun _ : ι => μ)≤ sqrt ((∫ ω, (ξ ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ))Proof (Lean source)
theorem iid_mean_abs_le_fintype {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (ξ : Ω → ℝ) (hξ : MemLp ξ 2 μ) : ∫ s, |(Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i)) - ∫ ω, ξ ω ∂μ| ∂(Measure.pi fun _ : ι => μ) ≤ sqrt ((∫ ω, (ξ ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ)) := by let P : Measure (ι → Ω) := Measure.pi fun _ : ι => μ let Y : (ι → Ω) → ℝ := fun s => (Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ (s i)) - ∫ ω, ξ ω ∂μ have hYLp : MemLp Y 2 P := by apply MemLp.sub (MemLp.const_mul (by simpa [P] using memLp_finset_sum univ fun i _ => hξ.comp_measurePreserving (measurePreserving_eval (fun _ : ι => μ) i)) _) exact memLp_const _ exact (ConvergingTogether.integral_abs_le_sqrt_integral_sq P Y hYLp).trans (by simpa [P, Y] using (Real.sqrt_le_sqrt (iid_mean_sq_le_fintype (ι := ι) μ ξ hξ))) -
memLp_two_iid_mean_euclidean_fintypetheorem — The centred coordinatewise sample averages of finitely many square-integrable statistics form a square-integrable Euclidean length on the product sample space.hypothesesProof (Lean source)
theorem memLp_two_iid_mean_euclidean_fintype {Ω ι κ : Type*} [MeasurableSpace Ω] [Fintype ι] [Fintype κ] (μ : Measure Ω) [IsProbabilityMeasure μ] (ξ : κ → Ω → ℝ) (hξ : ∀ k, MemLp (ξ k) 2 μ) : MemLp (fun s => sqrt (∑ k : κ, ((Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2)) 2 (Measure.pi fun _ : ι => μ) := by refine memLp_two_sqrt_sum_sq (fun k => ?_) apply MemLp.sub (MemLp.const_mul (by simpa using memLp_finset_sum univ fun i _ => (hξ k).comp_measurePreserving (measurePreserving_eval (fun _ : ι => μ) i)) _) exact memLp_const _ -
iid_mean_euclidean_abs_le_fintypetheorem — The expected Euclidean error of finitely many square-integrable sample averages from the same independent, identically distributed sample is controlled by their summed population second moments and the sample size.hypothesesProof (Lean source)
theorem iid_mean_euclidean_abs_le_fintype {Ω ι κ : Type*} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] [Fintype κ] (μ : Measure Ω) [IsProbabilityMeasure μ] (ξ : κ → Ω → ℝ) (hξ : ∀ k, MemLp (ξ k) 2 μ) : ∫ s, sqrt (∑ k : κ, ((Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2) ∂(Measure.pi fun _ : ι => μ) ≤ sqrt ((∑ k : κ, ∫ ω, (ξ k ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ)) := by let P : Measure (ι → Ω) := Measure.pi fun _ : ι => μ let Y : κ → (ι → Ω) → ℝ := fun k s => (Fintype.card ι : ℝ)⁻¹ * (∑ i : ι, ξ k (s i)) - ∫ ω, ξ k ω ∂μ let R : (ι → Ω) → ℝ := fun s => sqrt (∑ k : κ, (Y k s) ^ 2) have hYLp (k : κ) : MemLp (Y k) 2 P := by apply MemLp.sub (MemLp.const_mul (by simpa [P] using memLp_finset_sum univ fun i _ => (hξ k).comp_measurePreserving (measurePreserving_eval (fun _ : ι => μ) i)) _) exact memLp_const _ have hRLp : MemLp R 2 P := memLp_two_sqrt_sum_sq hYLp calc ∫ s, sqrt (∑ k : κ, (Y k s) ^ 2) ∂P ≤ sqrt (∫ s, (R s) ^ 2 ∂P) := by simpa [R, abs_of_nonneg (Real.sqrt_nonneg _)] using ConvergingTogether.integral_abs_le_sqrt_integral_sq P R hRLp _ = sqrt (∑ k : κ, ∫ s, (Y k s) ^ 2 ∂P) := by congr 1 rw [show (fun s => (R s) ^ 2) = fun s => ∑ k : κ, (Y k s) ^ 2 by funext s exact Real.sq_sqrt (sum_nonneg fun _ _ => sq_nonneg _)] exact integral_finset_sum _ fun k _ => (hYLp k).integrable_sq _ ≤ sqrt ((∑ k : κ, ∫ ω, (ξ k ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ)) := by apply Real.sqrt_le_sqrt calc (∑ k : κ, ∫ s, (Y k s) ^ 2 ∂P) ≤ ∑ k : κ, (∫ ω, (ξ k ω) ^ 2 ∂μ) / (Fintype.card ι : ℝ) := by exact Finset.sum_le_sum fun k _ => iid_mean_sq_le_fintype μ (ξ k) (hξ k) _ = _ := by rw [Finset.sum_div] -
iid_average_integral_fintypelemma — An average of independent, identically distributed observations has the same expectation as the population statistic being averaged.hypothesesconclusion(∫ sample : ι → Ω, (Fintype.card ι : ℝ)⁻¹ * ∑ i, F (sample i) ∂Measure.pi (fun _ : ι => μ))= ∫ o, F o ∂μProof (Lean source)
lemma iid_average_integral_fintype {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] [Nonempty ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (F : Ω → ℝ) (hF : Integrable F μ) : (∫ sample : ι → Ω, (Fintype.card ι : ℝ)⁻¹ * ∑ i, F (sample i) ∂Measure.pi (fun _ : ι => μ)) = ∫ o, F o ∂μ := by have hcard : Fintype.card ι ≠ 0 := Fintype.card_ne_zero rw [integral_const_mul] rw [integral_finset_sum] · simp_rw [integral_comp_eval (μ := fun _ : ι => μ) hF.aestronglyMeasurable] simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp · intro i _ exact integrable_comp_eval hF -
iid_average_variance_fintypelemma — The variance of an average of independent, identically distributed observations is the population variance divided by the sample size.hypothesesProof (Lean source)
lemma iid_average_variance_fintype {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (F : Ω → ℝ) (hF : MemLp F 2 μ) : variance (fun sample : ι → Ω => (Fintype.card ι : ℝ)⁻¹ * ∑ i, F (sample i)) (Measure.pi (fun _ : ι => μ)) = (Fintype.card ι : ℝ)⁻¹ * variance F μ := by by_cases hι : Nonempty ι · letI := hι have hcard : Fintype.card ι ≠ 0 := Fintype.card_ne_zero rw [ProbabilityTheory.variance_const_mul] have hfun : (fun sample : ι → Ω => ∑ i, F (sample i)) = ∑ i, fun sample : ι → Ω => F (sample i) := by funext sample simp rw [hfun] rw [ProbabilityTheory.variance_sum_pi (fun _ => hF)] simp only [Finset.sum_const, Finset.card_univ, nsmul_eq_mul] field_simp · haveI : IsEmpty ι := not_nonempty_iff.mp hι have hfun : (fun sample : ι → Ω => (Fintype.card ι : ℝ)⁻¹ * ∑ i, F (sample i)) = 0 := by funext sample simp rw [hfun, ProbabilityTheory.variance_zero] simp -
iid_mean_sq_letheorem — The mean squared error of a square-integrable scalar sample average of n independent, identically distributed observations is at most the population second moment divided by n.hypothesesProof (Lean source)
theorem iid_mean_sq_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) (ξ : Ω → ℝ) (hξ : MemLp ξ 2 μ) : ∫ s, ((n : ℝ)⁻¹ * (∑ i : Fin n, ξ (s i)) - ∫ ω, ξ ω ∂μ) ^ 2 ∂(Measure.pi fun _ : Fin n => μ) ≤ (∫ ω, (ξ ω) ^ 2 ∂μ) / (n : ℝ) := by haveI : Nonempty (Fin n) := Fin.pos_iff_nonempty.mp hn simpa using iid_mean_sq_le_fintype (ι := Fin n) μ ξ hξ -
iid_mean_abs_letheorem — The mean absolute error of a square-integrable scalar sample average of n independent, identically distributed observations is at most the square root of the population second moment divided by n.hypothesesProof (Lean source)
theorem iid_mean_abs_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (hn : 0 < n) (ξ : Ω → ℝ) (hξ : MemLp ξ 2 μ) : ∫ s, |(n : ℝ)⁻¹ * (∑ i : Fin n, ξ (s i)) - ∫ ω, ξ ω ∂μ| ∂(Measure.pi fun _ : Fin n => μ) ≤ sqrt ((∫ ω, (ξ ω) ^ 2 ∂μ) / (n : ℝ)) := by haveI : Nonempty (Fin n) := Fin.pos_iff_nonempty.mp hn simpa using iid_mean_abs_le_fintype (ι := Fin n) μ ξ hξ -
memLp_two_iid_mean_euclideantheorem — The centred coordinatewise sample averages of finitely many square-integrable statistics over an n-point independent, identically distributed sample form a square-integrable Euclidean length.hypothesesProof (Lean source)
theorem memLp_two_iid_mean_euclidean {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] (μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (ξ : ι → Ω → ℝ) (hξ : ∀ k, MemLp (ξ k) 2 μ) : MemLp (fun s => sqrt (∑ k : ι, ((n : ℝ)⁻¹ * (∑ i : Fin n, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2)) 2 (Measure.pi fun _ : Fin n => μ) := by simpa using memLp_two_iid_mean_euclidean_fintype (ι := Fin n) (κ := ι) μ ξ hξ -
integrable_iid_mean_euclideantheorem — The centred coordinatewise sample averages of finitely many integrable statistics over an n-point independent, identically distributed sample have integrable Euclidean length.hypothesesconclusionIntegrable (fun s => sqrt (∑ k : ι, ((n : ℝ)⁻¹ * (∑ i : Fin n, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2)) (Measure.pi fun _ : Fin n => μ)Proof (Lean source)
theorem integrable_iid_mean_euclidean {Ω ι : Type*} [MeasurableSpace Ω] [Fintype ι] (μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (ξ : ι → Ω → ℝ) (hξ : ∀ k, Integrable (ξ k) μ) : Integrable (fun s => sqrt (∑ k : ι, ((n : ℝ)⁻¹ * (∑ i : Fin n, ξ k (s i)) - ∫ ω, ξ k ω ∂μ) ^ 2)) (Measure.pi fun _ : Fin n => μ) := by let v : (Fin n → Ω) → ι → ℝ := fun s k => (n : ℝ)⁻¹ * (∑ i : Fin n, ξ k (s i)) - ∫ ω, ξ k ω ∂μ have hv (k : ι) : Integrable (fun s => v s k) (Measure.pi fun _ : Fin n => μ) := by dsimp only [v] apply Integrable.sub · apply Integrable.const_mul exact integrable_finset_sum univ fun i _ => (measurePreserving_eval (fun _ : Fin n => μ) i).integrable_comp_of_integrable (hξ k) · exact integrable_const _ simpa only [v] using integrable_euclidean_of_integrable v hv -
iid_average_integrallemma — An average of n independent, identically distributed observations has the same expectation as the population statistic being averaged.hypothesesProof (Lean source)
lemma iid_average_integral {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (m : ℕ) (hm : 0 < m) (F : Ω → ℝ) (hF : Integrable F μ) : (∫ sample : Fin m → Ω, (m : ℝ)⁻¹ * ∑ i, F (sample i) ∂Measure.pi (fun _ : Fin m => μ)) = ∫ o, F o ∂μ := by haveI : Nonempty (Fin m) := Fin.pos_iff_nonempty.mp hm simpa using iid_average_integral_fintype (ι := Fin m) μ F hF -
iid_average_variancelemma — The variance of an average of independent, identically distributed observations is the population variance divided by the sample size (including the zero-length case).hypothesesProof (Lean source)
lemma iid_average_variance {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (m : ℕ) (F : Ω → ℝ) (hF : MemLp F 2 μ) : variance (fun sample : Fin m → Ω => (m : ℝ)⁻¹ * ∑ i, F (sample i)) (Measure.pi (fun _ : Fin m => μ)) = (m : ℝ)⁻¹ * variance F μ := by cases m with | zero => have hfun : (fun sample : Fin 0 → Ω => ((0 : ℕ) : ℝ)⁻¹ * ∑ i, F (sample i)) = 0 := by funext sample simp rw [hfun, ProbabilityTheory.variance_zero] simp | succ m => simpa using iid_average_variance_fintype (ι := Fin (m + 1)) μ F hF
MeasurableCondQuantile 2 core · 7 supporting This file constructs a measurable conditional quantile from Mathlib's regular conditional CDF condCDF ρ : α → StieltjesFunction ℝ. ★ measurable_condQuantile_and_attains
Measurable conditional quantile selection
This file constructs a measurable conditional quantile from Mathlib's regular conditional
CDF condCDF ρ : α → StieltjesFunction ℝ. Given a measurable target level
τ : α → ℝ with 0 < τ a < 1, the conditional quantile is the generalized inverse
condQuantile ρ τ a = inf {x | τ a ≤ condCDF ρ a x}.
The key measurability identity is
{a | condQuantile ρ τ a ≤ t} = {a | τ a ≤ condCDF ρ a t}, using monotonicity,
right-continuity, and the atBot/atTop limits of condCDF. The theorem
measurable_condQuantile_and_attains proves that condQuantile ρ τ is measurable and,
when every conditional CDF is continuous at its selected quantile, attains the requested level:
condCDF ρ a (condQuantile ρ τ a) = τ a.
def condQuantile reviewed
⚑ flagged
Causalean.Mathlib
For any measurable parameter space, a measure on the product of that space and the real line, a real-valued target-level function on the parameter space, and a parameter value, the conditional quantile is the infimum of the real response values at which the conditional cumulative distribution function reaches the target level at that parameter value.
theorem measurable_condQuantile_and_attains reviewed
⚑ flagged
Causalean.Mathlib
Measurable conditional quantile (selection). For a measure ρ on the product of a parameter space and the reals, and a measurable target level function τ that is everywhere strictly positive and everywhere strictly below one, if the conditional cumulative distribution function of ρ is continuous at the selected conditional quantile, for every parameter value, then the conditional quantile map condQuantile ρ τ is measurable and attains the target level — the conditional CDF at the selected quantile equals τ a for every a.
Formal statement
hypotheses
α :
Type u_1
ρ :
Measure (α × ℝ)
τ :
α → ℝ
hτ :
hτ0 :
∀ a, 0 < τ a
hτ1 :
∀ a, τ a < 1
hcont :
conclusion
conclusion 1
Measurable (condQuantile ρ τ)
Proof (Lean source)
theorem measurable_condQuantile_and_attains (ρ : Measure (α × ℝ))
(τ : α → ℝ) (hτ : Measurable τ) (hτ0 : ∀ a, 0 < τ a) (hτ1 : ∀ a, τ a < 1)
(hcont : ∀ a, ContinuousAt (condCDF ρ a) (condQuantile ρ τ a)) :
Measurable (condQuantile ρ τ) ∧
∀ a, condCDF ρ a (condQuantile ρ τ a) = τ a := by
constructor
· refine measurable_of_Iic (α := ℝ) (fun t => ?_)
have hset : (condQuantile ρ τ) ⁻¹' Iic t = {a | τ a ≤ condCDF ρ a t} := by
ext a
exact condQuantile_le_iff (ρ := ρ) (τ := τ) (a := a) (x := t) (hτ0 a) (hτ1 a)
rw [hset]
exact measurableSet_le hτ (measurable_condCDF ρ t)
· intro a
have hge : τ a ≤ condCDF ρ a (condQuantile ρ τ a) :=
le_condCDF_condQuantile (ρ := ρ) (τ := τ) (a := a) (hτ1 a)
have hle : condCDF ρ a (condQuantile ρ τ a) ≤ τ a := by
by_contra hnot
have hlt : τ a < condCDF ρ a (condQuantile ρ τ a) := lt_of_not_ge hnot
let q := condQuantile ρ τ a
have hnear : ∀ᶠ y in 𝓝 q, τ a < condCDF ρ a y := by
simpa [q] using ((hcont a).tendsto.eventually_const_lt hlt)
obtain ⟨ε, hεpos, hε⟩ := Metric.eventually_nhds_iff.mp hnear
let x := q - ε / 2
have hxlt : x < q := sub_lt_self q (half_pos hεpos)
have hdist : dist x q < ε := by
rw [Real.dist_eq]
have hhalf_pos : 0 < ε / 2 := half_pos hεpos
have hcalc : x - q = -(ε / 2) := by simp [x]
rw [hcalc, abs_neg, abs_of_pos hhalf_pos]
linarith
have hxS : τ a ≤ condCDF ρ a x := (hε hdist).le
have hq_le_x : q ≤ x := by
change condQuantile ρ τ a ≤ x
exact condQuantile_le_of_le_condCDF (ρ := ρ) (τ := τ) (a := a) (hτ0 a) hxS
exact not_lt_of_ge hq_le_x hxlt
exact le_antisymm hle hge
7 supporting declarations (lemmas, instances)
-
condQuantileSet_up_closedlemma — If a response value's conditional cumulative distribution function reaches a target level, then every larger response value also reaches that level. -
bddBelow_condQuantileSetlemma — At a strictly positive conditional-quantile level, the response values whose conditional cumulative distribution function reaches that level are bounded below.hypotheseshτ0 :0 < τ aProof (Lean source)
lemma bddBelow_condQuantileSet {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} (hτ0 : 0 < τ a) : BddBelow {x : ℝ | τ a ≤ condCDF ρ a x} := by obtain ⟨N, hN⟩ := Filter.eventually_atBot.mp ((tendsto_condCDF_atBot ρ a).eventually_lt_const hτ0) refine ⟨N, fun s hs => ?_⟩ by_contra hlt push_neg at hlt exact absurd hs (not_le.mpr (hN s hlt.le)) -
nonempty_condQuantileSetlemma — At a conditional-quantile level strictly below one, some response value has a conditional cumulative distribution function that reaches that level.Proof (Lean source)
lemma nonempty_condQuantileSet {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} (hτ1 : τ a < 1) : ({x : ℝ | τ a ≤ condCDF ρ a x}).Nonempty := by obtain ⟨N, hN⟩ := Filter.eventually_atTop.mp ((tendsto_condCDF_atTop ρ a).eventually_const_lt hτ1) exact ⟨N, (hN N le_rfl).le⟩ -
le_condCDF_condQuantilelemma — At a target level below one, the conditional generalized inverse reaches at least that level in the conditional cumulative distribution function.Proof (Lean source)
lemma le_condCDF_condQuantile {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} (hτ1 : τ a < 1) : τ a ≤ condCDF ρ a (condQuantile ρ τ a) := by set q := condQuantile ρ τ a with hq have hne : ({x : ℝ | τ a ≤ condCDF ρ a x}).Nonempty := nonempty_condQuantileSet hτ1 have hgt : ∀ x, q < x → τ a ≤ condCDF ρ a x := by intro x hx obtain ⟨s, hs, hsx⟩ := exists_lt_of_csInf_lt hne hx exact condQuantileSet_up_closed hs hsx.le have htends : Tendsto (condCDF ρ a) (𝓝[Ioi q] q) (𝓝 (condCDF ρ a q)) := ((condCDF ρ a).right_continuous q).mono_left (nhdsWithin_mono q Set.Ioi_subset_Ici_self) have hev : ∀ᶠ x in 𝓝[Ioi q] q, τ a ≤ condCDF ρ a x := by filter_upwards [self_mem_nhdsWithin] with x hx using hgt x hx exact ge_of_tendsto htends hev -
le_condCDF_of_condQuantile_lelemma — A conditional quantile below a value makes the conditional CDF reach any level below one.hypothesesconclusionτ a ≤ condCDF ρ a xProof (Lean source)
lemma le_condCDF_of_condQuantile_le {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} {x : ℝ} (hτ1 : τ a < 1) (hx : condQuantile ρ τ a ≤ x) : τ a ≤ condCDF ρ a x := le_trans (le_condCDF_condQuantile (ρ := ρ) (τ := τ) (a := a) hτ1) ((condCDF ρ a).mono hx) -
condQuantile_le_of_le_condCDFlemma — When the conditional cumulative distribution function has reached a positive target level at a point, the conditional generalized inverse is no larger than that point.hypothesesconclusioncondQuantile ρ τ a ≤ xProof (Lean source)
lemma condQuantile_le_of_le_condCDF {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} {x : ℝ} (hτ0 : 0 < τ a) (hx : τ a ≤ condCDF ρ a x) : condQuantile ρ τ a ≤ x := csInf_le (bddBelow_condQuantileSet (ρ := ρ) (τ := τ) (a := a) hτ0) hx -
condQuantile_le_ifflemma — At an interior target level, a point is above the conditional generalized inverse exactly when its conditional cumulative distribution function has reached that level.hypothesesconclusioncondQuantile ρ τ a ≤ x ↔ τ a ≤ condCDF ρ a xProof (Lean source)
lemma condQuantile_le_iff {ρ : Measure (α × ℝ)} {τ : α → ℝ} {a : α} {x : ℝ} (hτ0 : 0 < τ a) (hτ1 : τ a < 1) : condQuantile ρ τ a ≤ x ↔ τ a ≤ condCDF ρ a x := ⟨le_condCDF_of_condQuantile_le (ρ := ρ) (τ := τ) (a := a) hτ1, condQuantile_le_of_le_condCDF (ρ := ρ) (τ := τ) (a := a) hτ0⟩
SignedTwoPoint 2 core · 8 supporting The symmetric two-point outcome law twoPointMean B u supported on {−B, B} with mean u: Q_u(B) = (1 + u/B)/2, Q_u(−B) = (1 − u/B)/2. ★ bernoulli_mean_channel_kl
Symmetric signed two-point mean channel
The symmetric two-point outcome law twoPointMean B u supported on {−B, B} with mean u:
Q_u(B) = (1 + u/B)/2, Q_u(−B) = (1 − u/B)/2. It is the affine image of the {0,1} Bernoulli
law bernoulliLaw under x ↦ 2Bx − B, which lets its Kullback–Leibler divergence inherit the
quadratic band of the Bernoulli KL.
This file provides:
* twoPointMean — the signed two-point channel, with measurable_twoPointMean,
twoPointMean_isProbabilityMeasure, twoPointMean_integral, twoPointMean_mean,
twoPointMean_bad_support_zero;
* klDiv_map_measurableEquiv — KL-divergence invariance under a measurable equivalence;
* twoPointMean_eq_map_bernoulli — the affine-image representation;
* bernoulli_mean_channel_kl — the KL band KL(Q_u, Q_v) ≤ (u − v)²/B² for |u|,|v| ≤ B/2.
It is the reusable least-favorable outcome channel for two-point / Le Cam minimax lower bounds in a mean-estimation setting.
def twoPointMean reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a real scale and a real target mean, the symmetric two-point mean measure is the sum of a point mass at weighted by and a point mass at weighted by .
lemma bernoulli_mean_channel_kl reviewed
⚑ flagged
Causalean.Mathlib.Probability
KL band for the signed two-point mean channel. For a strictly positive spread parameter B and two channel means u and v each confined to the interval [-B/2, B/2], the Kullback–Leibler divergence between the two-point channels with means u and v is bounded by the quadratic (u − v)²/B². This is the affine transport of the {0,1} Bernoulli KL band onto the {−B, B} mean parametrization.
Formal statement
hypotheses
B u v :
ℝ
hB :
0 < B
hu :
|u| ≤ B / 2
hv :
|v| ≤ B / 2
conclusion
≤ ofReal ((u - v) ^ 2 / B ^ 2)
Proof (Lean source)
lemma bernoulli_mean_channel_kl (B u v : ℝ) (hB : 0 < B)
(hu : |u| ≤ B / 2) (hv : |v| ≤ B / 2) :
klDiv (twoPointMean B u) (twoPointMean B v)
≤ ofReal ((u - v) ^ 2 / B ^ 2) := by
let p : ℝ := (1 + u / B) / 2
let q : ℝ := (1 + v / B) / 2
have hB_ne : B ≠ 0 := ne_of_gt hB
have hu_bounds := abs_le.mp hu
have hv_bounds := abs_le.mp hv
have hp_lo : 1 / 4 ≤ p := by
dsimp [p]
field_simp [hB_ne]
nlinarith [hu_bounds.1, hB]
have hp_hi : p ≤ 3 / 4 := by
dsimp [p]
field_simp [hB_ne]
nlinarith [hu_bounds.2, hB]
have hq_lo : 1 / 4 ≤ q := by
dsimp [q]
field_simp [hB_ne]
nlinarith [hv_bounds.1, hB]
have hq_hi : q ≤ 3 / 4 := by
dsimp [q]
field_simp [hB_ne]
nlinarith [hv_bounds.2, hB]
haveI : IsFiniteMeasure (bernoulliLaw p) := by
rw [bernoulliLaw]
refine ⟨?_⟩
rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply]
simp only [Measure.dirac_apply, Set.mem_univ, Set.indicator_of_mem, Pi.one_apply,
smul_eq_mul, mul_one]
exact ENNReal.add_lt_top.2 ⟨ENNReal.ofReal_lt_top, ENNReal.ofReal_lt_top⟩
haveI : IsFiniteMeasure (bernoulliLaw q) := by
rw [bernoulliLaw]
refine ⟨?_⟩
rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply]
simp only [Measure.dirac_apply, Set.mem_univ, Set.indicator_of_mem, Pi.one_apply,
smul_eq_mul, mul_one]
exact ENNReal.add_lt_top.2 ⟨ENNReal.ofReal_lt_top, ENNReal.ofReal_lt_top⟩
rw [twoPointMean_eq_map_bernoulli B u hB.ne', twoPointMean_eq_map_bernoulli B v hB.ne',
klDiv_map_measurableEquiv]
have hbern :
klDiv (bernoulliLaw p) (bernoulliLaw q) ≤
ofReal (4 * (p - q) ^ 2) :=
bernoulliLaw_klDiv_le_four_sq_sub hp_lo hp_hi hq_lo hq_hi
calc
klDiv (bernoulliLaw p) (bernoulliLaw q)
≤ ofReal (4 * (p - q) ^ 2) := hbern
_ = ofReal ((u - v) ^ 2 / B ^ 2) := by
congr 1
subst p
subst q
field_simp [hB_ne]
ring
8 supporting declarations (lemmas, instances)
-
measurable_twoPointMeanlemma — For a fixed scale B, the signed two-point mean channel is measurable as a function of the target mean u.Proof (Lean source)
@[fun_prop] lemma measurable_twoPointMean (B : ℝ) : Measurable (fun u : ℝ => twoPointMean B u) := by unfold twoPointMean fun_prop -
twoPointMean_coef_nonneglemma — When the scale is positive and the target mean lies within that scale, both weights in the signed two-point distribution are nonnegative.hypothesesB u :ℝhB :0 < Bhu :|u| ≤ Bconclusionconclusion 10 ≤ (1 + u / B) / 2conclusion 20 ≤ (1 - u / B) / 2Proof (Lean source)
lemma twoPointMean_coef_nonneg {B u : ℝ} (hB : 0 < B) (hu : |u| ≤ B) : 0 ≤ (1 + u / B) / 2 ∧ 0 ≤ (1 - u / B) / 2 := by have hbounds := abs_le.mp hu constructor <;> field_simp [ne_of_gt hB] <;> nlinarith [hbounds.1, hbounds.2, hB] -
twoPointMean_isProbabilityMeasurelemma — The signed two-point channel is a probability measure. For 0 < B and |u| ≤ B the total mass of twoPointMean B u is 1.Proof (Lean source)
lemma twoPointMean_isProbabilityMeasure {B u : ℝ} (hB : 0 < B) (hu : |u| ≤ B) : IsProbabilityMeasure (twoPointMean B u) := by rw [isProbabilityMeasure_iff] unfold twoPointMean rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] simp only [Measure.dirac_apply, Set.indicator_of_mem, Set.mem_univ, Pi.one_apply, smul_eq_mul, mul_one] rcases twoPointMean_coef_nonneg hB hu with ⟨hplus, hminus⟩ rw [← ENNReal.ofReal_add hplus hminus] rw [show (1 + u / B) / 2 + (1 - u / B) / 2 = (1 : ℝ) by ring] simp -
twoPointMean_integrallemma — Two-point integral. For 0 < B and |u| ≤ B, integrating f against twoPointMean B u returns the two-point weighted average ((1 + u/B)/2)·f(B) + ((1 − u/B)/2)·f(−B).hypothesesB u :ℝhB :0 < Bhu :|u| ≤ Bf :ℝ → ℝconclusion∫ y, f y ∂twoPointMean B u = ((1 + u / B) / 2) * f B + ((1 - u / B) / 2) * f (-B)Proof (Lean source)
lemma twoPointMean_integral {B u : ℝ} (hB : 0 < B) (hu : |u| ≤ B) (f : ℝ → ℝ) : ∫ y, f y ∂twoPointMean B u = ((1 + u / B) / 2) * f B + ((1 - u / B) / 2) * f (-B) := by unfold twoPointMean rw [integral_add_measure] · rw [integral_smul_measure, integral_smul_measure] rcases twoPointMean_coef_nonneg hB hu with ⟨hplus, hminus⟩ simp [hplus, hminus, smul_eq_mul] · exact Integrable.smul_measure (μ := Measure.dirac B) (c := ofReal ((1 + u / B) / 2)) (integrable_dirac (f := f) (a := B) (by simp [enorm])) (by simp) · exact Integrable.smul_measure (μ := Measure.dirac (-B)) (c := ofReal ((1 - u / B) / 2)) (integrable_dirac (f := f) (a := -B) (by simp [enorm])) (by simp) -
twoPointMean_meanlemma — The mean is u. For 0 < B and |u| ≤ B, the expectation of the identity under twoPointMean B u is exactly u.hypothesesB u :ℝhB :0 < Bhu :|u| ≤ Bconclusion∫ y, y ∂twoPointMean B u = uProof (Lean source)
lemma twoPointMean_mean {B u : ℝ} (hB : 0 < B) (hu : |u| ≤ B) : ∫ y, y ∂twoPointMean B u = u := by rw [twoPointMean_integral hB hu] field_simp [ne_of_gt hB] ring -
twoPointMean_bad_support_zerolemma — The channel is supported in [−M, M] whenever |B| ≤ M. The mass that any nonnegative mixture of point masses at B and −B places outside the interval [−M, M] is 0.hypothesesB M :ℝwplus wminus :ℝ≥0∞hBM :|B| ≤ Mconclusion(wplus • Measure.dirac B + wminus • Measure.dirac (-B)) {y | y ∉ Icc (-M) M} = 0Proof (Lean source)
lemma twoPointMean_bad_support_zero {B M : ℝ} (wplus wminus : ℝ≥0∞) (hBM : |B| ≤ M) : (wplus • Measure.dirac B + wminus • Measure.dirac (-B)) {y | y ∉ Icc (-M) M} = 0 := by let S : Set ℝ := {y | y ∉ Icc (-M) M} have hS : MeasurableSet S := measurableSet_Icc.compl change (wplus • Measure.dirac B + wminus • Measure.dirac (-B)) S = 0 rw [Measure.add_apply, Measure.smul_apply, Measure.smul_apply] have hBmem : B ∈ Icc (-M) M := by exact abs_le.mp hBM have hnegBmem : -B ∈ Icc (-M) M := by rw [Set.mem_Icc] constructor <;> linarith [abs_le.mp hBM |>.1, abs_le.mp hBM |>.2] have hBbad : B ∉ S := by simpa [S] using hBmem have hnegBbad : -B ∉ S := by simpa [S] using hnegBmem have hdiracB : Measure.dirac B S = 0 := by rw [Measure.dirac_apply' B hS] simp [hBbad] have hdiracNeg : Measure.dirac (-B) S = 0 := by rw [Measure.dirac_apply' (-B) hS] simp [hnegBbad] rw [hdiracB, hdiracNeg] simp -
klDiv_map_measurableEquivlemma — KL-divergence is invariant under a measurable equivalence. Pushing both finite measures μ, ν forward through a measurable equivalence e leaves their Kullback–Leibler divergence unchanged: KL(e_* μ, e_* ν) = KL(μ, ν).hypothesesα β :e :α ≃ᵐ βμ ν :Proof (Lean source)
lemma klDiv_map_measurableEquiv {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] (e : α ≃ᵐ β) (μ ν : Measure α) [IsFiniteMeasure μ] [IsFiniteMeasure ν] : klDiv (Measure.map e μ) (Measure.map e ν) = klDiv μ ν := by by_cases hμν : μ ≪ ν · have hmap : Measure.map e μ ≪ Measure.map e ν := hμν.map e.measurable rw [InformationTheory.klDiv_eq_lintegral_klFun, InformationTheory.klDiv_eq_lintegral_klFun, if_pos hmap, if_pos hμν] rw [e.measurableEmbedding.lintegral_map] refine lintegral_congr_ae ?_ exact (e.measurableEmbedding.rnDeriv_map μ ν).mono fun _ hx => by simpa using congrArg (fun y : ℝ≥0∞ => ofReal (klFun y.toReal)) hx · have hmap_not : ¬ Measure.map e μ ≪ Measure.map e ν := by intro hmap apply hμν have hback : Measure.map e.symm (Measure.map e μ) ≪ Measure.map e.symm (Measure.map e ν) := hmap.map e.symm.measurable simpa [Measure.map_map, Function.comp_def] using hback rw [InformationTheory.klDiv_eq_lintegral_klFun, InformationTheory.klDiv_eq_lintegral_klFun, if_neg hmap_not, if_neg hμν] -
twoPointMean_eq_map_bernoullilemma — Affine-image representation. The {−B, B} mean channel is the pushforward of the {0,1} Bernoulli law bernoulliLaw ((1 + u/B)/2) under the affine map x ↦ 2Bx − B (for B ≠ 0).hypothesesB u :ℝhB :B ≠ 0conclusiontwoPointMean B u= Measure.map (affineHomeomorph (2 * B) (-B) (mul_ne_zero (by norm_num) hB)).toMeasurableEquiv (bernoulliLaw ((1 + u / B) / 2))Proof (Lean source)
lemma twoPointMean_eq_map_bernoulli (B u : ℝ) (hB : B ≠ 0) : twoPointMean B u = Measure.map (affineHomeomorph (2 * B) (-B) (mul_ne_zero (by norm_num) hB)).toMeasurableEquiv (bernoulliLaw ((1 + u / B) / 2)) := by let e : ℝ ≃ᵐ ℝ := (affineHomeomorph (2 * B) (-B) (mul_ne_zero (by norm_num) hB)).toMeasurableEquiv change twoPointMean B u = Measure.map e (bernoulliLaw ((1 + u / B) / 2)) rw [twoPointMean, bernoulliLaw] rw [Measure.map_add _ _ e.measurable] rw [Measure.map_smul, Measure.map_smul] rw [Measure.map_dirac, Measure.map_dirac] simp only [Homeomorph.toMeasurableEquiv_coe, affineHomeomorph_apply, mul_one, mul_zero, zero_add, e] rw [show 2 * B + -B = B by ring] rw [show 1 - (1 + u / B) / 2 = (1 - u / B) / 2 by ring]
StdNormalMoments 1 core · 1 supporting This file proves two one-dimensional identities for the named standard-normal density stdNormalPDF and CDF stdNormalCDF: * integral_Ioi_stdNormalPDF: the survival integral ∫_{c}^∞ φ(t) dt = 1 - Φ(c); * integral_Ioi_id_mu ★ integral_Ioi_id_mul_stdNormalPDF
Standard normal survival integral and truncated first moment
This file proves two one-dimensional identities for the named standard-normal
density stdNormalPDF and CDF stdNormalCDF:
* integral_Ioi_stdNormalPDF: the survival integral
∫_{c}^∞ φ(t) dt = 1 - Φ(c);
* integral_Ioi_id_mul_stdNormalPDF: the truncated first moment
∫_{c}^∞ t * φ(t) dt = φ(c).
The moment identity follows from d/dt[-φ(t)] = t * φ(t) and supplies the
closed-form Gaussian tail moment used by sensitivity calculations.
lemma integral_Ioi_id_mul_stdNormalPDF reviewed
⚑ flagged
Causalean.Mathlib
The standard-normal truncated first moment. For any real cutoff c, the tail integral of t times the standard normal density over (c, ∞) equals the density value at c.
Formal statement
Proof (Lean source)
lemma integral_Ioi_id_mul_stdNormalPDF (c : ℝ) :
∫ t in Ioi c, t * stdNormalPDF t = stdNormalPDF c := by
let phi : ℝ → ℝ := fun x => exp (-x ^ 2 / 2)
have phi_pos : ∀ x : ℝ, 0 < phi x := fun x => Real.exp_pos _
have phi_continuous : Continuous phi := by
dsimp [phi]
fun_prop
have gaussianPDFReal_eq : ∀ x : ℝ,
gaussianPDFReal 0 1 x = (sqrt (2 * π))⁻¹ * phi x := by
intro x
unfold gaussianPDFReal
dsimp [phi]
congr 2
· norm_num
· ring
have neg_phi_hasDerivAt :
∀ x : ℝ, HasDerivAt (fun y => -phi y) (x * phi x) x := by
intro x
dsimp [phi]
have hpow : HasDerivAt (fun y : ℝ => -y ^ 2 / 2) (-x) x := by
have := ((hasDerivAt_pow 2 x).div_const 2).fun_neg
simpa [neg_div, pow_one] using this.congr_deriv (by ring)
have hcomp : HasDerivAt (fun y => exp (-y ^ 2 / 2))
(exp (-x ^ 2 / 2) * (-x)) x := (Real.hasDerivAt_exp _).comp x hpow
exact hcomp.fun_neg.congr_deriv (by ring)
have abs_le_exp_sq_div_four : ∀ x : ℝ, |x| ≤ exp (x ^ 2 / 4) := by
intro x
have h1 : |x| ≤ 1 + x ^ 2 / 4 := by
nlinarith [sq_nonneg (|x| / 2 - 1), sq_abs x, abs_nonneg x]
exact h1.trans (by have := Real.add_one_le_exp (x ^ 2 / 4); linarith)
have x_mul_phi_integrable : Integrable (fun x : ℝ => x * phi x) := by
have hdom : Integrable (fun x : ℝ => exp (-(1/4 : ℝ) * x ^ 2)) :=
integrable_exp_neg_mul_sq (by norm_num)
refine hdom.mono' ((continuous_id.mul phi_continuous).aestronglyMeasurable) ?_
filter_upwards with x
have hexp : phi x = exp (-(1/2 : ℝ) * x ^ 2) := by
dsimp [phi]
ring_nf
rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg (phi_pos x).le, hexp]
calc |x| * exp (-(1/2 : ℝ) * x ^ 2)
≤ exp (x ^ 2 / 4) * exp (-(1/2 : ℝ) * x ^ 2) := by
gcongr
exact abs_le_exp_sq_div_four x
_ = exp (-(1/4 : ℝ) * x ^ 2) := by
rw [← Real.exp_add]
congr 1
ring
have mul_phi_integrableOn_Ioi : IntegrableOn (fun x => x * phi x) (Ioi c) := by
exact x_mul_phi_integrable.integrableOn
have neg_phi_tendsto_atTop :
Tendsto (fun x => -phi x) atTop (nhds 0) := by
have : Tendsto phi atTop (nhds 0) := by
dsimp [phi]
have hsq : Tendsto (fun x : ℝ => x ^ 2) atTop atTop := by
exact Filter.tendsto_pow_atTop (α := ℝ) (n := 2) (by norm_num)
have h2 :
Tendsto (fun x : ℝ => -x ^ 2 / 2) atTop atBot := by
apply Filter.Tendsto.atBot_div_const (by norm_num)
exact Filter.tendsto_neg_atBot_iff.mpr hsq
exact Real.tendsto_exp_atBot.comp h2
simpa using this.neg
have integral_Ioi_mul_phi : ∫ x in Ioi c, x * phi x = phi c := by
have := integral_Ioi_of_hasDerivAt_of_tendsto'
(f := fun y => -phi y) (f' := fun x => x * phi x) (a := c) (m := 0)
(fun x _ => neg_phi_hasDerivAt x) mul_phi_integrableOn_Ioi neg_phi_tendsto_atTop
simpa using this
calc
∫ t in Ioi c, t * stdNormalPDF t
= ∫ t in Ioi c, (sqrt (2 * π))⁻¹ * (t * phi t) := by
congr 1
ext t
rw [stdNormalPDF, gaussianPDFReal_eq]
ring
_ = (sqrt (2 * π))⁻¹ * ∫ t in Ioi c, t * phi t := by
rw [integral_const_mul]
_ = (sqrt (2 * π))⁻¹ * phi c := by
rw [integral_Ioi_mul_phi]
_ = stdNormalPDF c := by
rw [stdNormalPDF, gaussianPDFReal_eq]
1 supporting declaration (lemmas, instances)
-
integral_Ioi_stdNormalPDFlemma — The standard-normal survival integral: ∫_{c}^∞ φ(t) dt = 1 − Φ(c).Proof (Lean source)
lemma integral_Ioi_stdNormalPDF (c : ℝ) : ∫ t in Ioi c, stdNormalPDF t = 1 - stdNormalCDF c := by have hmeasure := ProbabilityTheory.gaussianReal_apply_eq_integral (μ := 0) (v := 1) (by norm_num) (Ioi c) have hnonneg_g : 0 ≤ ∫ t in Ioi c, gaussianPDFReal 0 1 t := by exact integral_nonneg fun t => gaussianPDFReal_nonneg 0 1 t have hset_g : ∫ t in Ioi c, gaussianPDFReal 0 1 t = (gaussianReal 0 1).real (Ioi c) := by rw [MeasureTheory.measureReal_def] rw [hmeasure] exact (ENNReal.toReal_ofReal hnonneg_g).symm have hset : ∫ t in Ioi c, stdNormalPDF t = (gaussianReal 0 1).real (Ioi c) := by simpa [stdNormalPDF] using hset_g have hcompl : (gaussianReal 0 1).real (Ioi c) = 1 - (gaussianReal 0 1).real (Iic c) := by have h := MeasureTheory.measureReal_compl (μ := gaussianReal 0 1) (s := Iic c) measurableSet_Iic simpa [Set.compl_Iic, MeasureTheory.probReal_univ] using h have hcdf : (gaussianReal 0 1).real (Iic c) = stdNormalCDF c := by rw [stdNormalCDF, ProbabilityTheory.cdf_eq_real] rw [hset, hcompl, hcdf]
VarianceProd 1 core · 0 supporting This file provides the law of total variance in an explicit form for a statistic of two independent coordinates, using its within-slice variances and slice means. ★ variance_prod_eq_integral_variance_add
Variance decomposition on a product probability space
This file provides the law of total variance in an explicit form for a statistic of two independent coordinates, using its within-slice variances and slice means.
lemma variance_prod_eq_integral_variance_add reviewed
⚑ flagged
Causalean.Mathlib.Probability
For independent coordinates with laws μ and ν, and a real-valued statistic F on the product that is square-integrable under the product law, suppose that almost every slice of F along the first coordinate, at a fixed value of the second coordinate, is square-integrable, that the map m of slice means is square-integrable under ν, and that m records the correct slice means: the integral of F over the first coordinate at almost every value of the second coordinate equals m there. Then the variance of F under the product measure equals the ν-average of the within-slice variances of F plus the variance, across the second coordinate, of the slice-mean map m.
Formal statement
Proof (Lean source)
lemma variance_prod_eq_integral_variance_add
{Ω T : Type*} [MeasurableSpace Ω] [MeasurableSpace T]
(μ : Measure Ω) (ν : Measure T)
[IsProbabilityMeasure μ] [IsProbabilityMeasure ν]
(F : Ω × T → ℝ) (m : T → ℝ)
(hF : MemLp F 2 (μ.prod ν))
(hsection : ∀ᵐ t ∂ν, MemLp (fun s => F (s, t)) 2 μ)
(hm : MemLp m 2 ν)
(hmean : ∀ᵐ t ∂ν, (∫ s, F (s, t) ∂μ) = m t) :
variance F (μ.prod ν) =
(∫ t, variance (fun s => F (s, t)) μ ∂ν) +
variance m ν := by
have hFsq : Integrable (fun z => F z ^ 2) (μ.prod ν) :=
hF.integrable_sq
have hinnerSq :
Integrable (fun t => ∫ s, F (s, t) ^ 2 ∂μ) ν := by
simpa only [Function.uncurry_apply_pair] using hFsq.integral_prod_right
have hvariance :
(fun t => variance (fun s => F (s, t)) μ) =ᵐ[ν]
fun t => (∫ s, F (s, t) ^ 2 ∂μ) - (m t) ^ 2 := by
filter_upwards [hsection, hmean] with t htsection htmean
rw [variance_eq_sub htsection, htmean]
simp only [Pi.pow_apply]
rw [variance_eq_sub hF, variance_eq_sub hm]
rw [integral_congr_ae hvariance]
simp only [Pi.pow_apply]
rw [integral_sub hinnerSq hm.integrable_sq]
rw [integral_prod_symm _ hFsq]
have hFint : Integrable F (μ.prod ν) := hF.integrable (by norm_num)
rw [integral_prod_symm _ hFint]
rw [integral_congr_ae hmean]
ring
WeightedProduct 3 core · 2 supporting This module states the finite-product second-moment and expected-absolute-value bounds for marked observations centered by their design-conditional mean. ★ product_weighted_centered_l1_le
Weighted conditional-mean-zero sums under a finite product law
This module states the finite-product second-moment and expected-absolute-value bounds for marked observations centered by their design-conditional mean. The weights may depend measurably on the complete vector of observed designs.
def designVector reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a map assigning each observation a design value and a finite sample of observations, the design vector assigns to every sample coordinate the design value of the observation at that coordinate.
def weightedCenteredSum reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a map assigning each observation a design value, a real-valued outcome function, a real-valued function of design values, weights that may depend on the complete design vector, and a finite sample of observations, the weighted centered sum is the sum over sample coordinates of each weight times the outcome minus the given function evaluated at that coordinate's design value.
theorem product_weighted_centered_l1_le reviewed
⚑ flagged
Causalean.Mathlib.Probability
For a one-observation probability law, a measurable design map, a measurable outcome confined to the unit interval, a measurable design regression that is its conditional expectation, a measurable array of weights depending on the full design vector, and the two natural square-integrability conditions, the expected absolute weighted centered sum is at most one half the square root of the expected sum of squared weights.
Formal statement
hypotheses
N :
Omega D :
P :
Measure Omega
design :
Omega -> D
hdesign :
Measurable design
Y :
Omega -> Real
hY :
hY_nonneg :
forall omega, 0 <= Y omega
hY_le_one :
forall omega, Y omega <= 1
mD :
D -> Real
hmD :
Measurable mD
hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design
hw :
hweight_sq :
Integrable (fun z : Fin N -> Omega => ∑ i, (w (designVector design z) i) ^ 2) (Measure.pi (fun _ : Fin N => P))
hsum_sq :
Integrable (fun z : Fin N -> Omega => (weightedCenteredSum design Y mD w z) ^ 2) (Measure.pi (fun _ : Fin N => P))
conclusion
(∫ z : Fin N -> Omega, abs (weightedCenteredSum design Y mD w z) ∂(Measure.pi (fun _ : Fin N => P))) <
= (1 / 2 : Real) * sqrt (∫ z : Fin N -> Omega, ∑ i, (w (designVector design z) i) ^ 2 ∂(Measure.pi (fun _ : Fin N => P)))
Proof (Lean source)
theorem product_weighted_centered_l1_le
{N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D]
(P : Measure Omega) [IsProbabilityMeasure P]
(design : Omega -> D) (hdesign : Measurable design)
(Y : Omega -> Real) (hY : Measurable Y)
(hY_nonneg : forall omega, 0 <= Y omega)
(hY_le_one : forall omega, Y omega <= 1)
(mD : D -> Real) (hmD : Measurable mD)
(hcond :
P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design)
(w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w)
(hweight_sq : Integrable
(fun z : Fin N -> Omega => ∑ i, (w (designVector design z) i) ^ 2)
(Measure.pi (fun _ : Fin N => P)))
(hsum_sq : Integrable
(fun z : Fin N -> Omega =>
(weightedCenteredSum design Y mD w z) ^ 2)
(Measure.pi (fun _ : Fin N => P))) :
(∫ z : Fin N -> Omega,
abs (weightedCenteredSum design Y mD w z)
∂(Measure.pi (fun _ : Fin N => P))) <=
(1 / 2 : Real) * sqrt
(∫ z : Fin N -> Omega,
∑ i, (w (designVector design z) i) ^ 2
∂(Measure.pi (fun _ : Fin N => P))) := by
let μN : Measure (Fin N -> Omega) := Measure.pi fun _ : Fin N => P
let S : (Fin N -> Omega) -> Real := weightedCenteredSum design Y mD w
let A : Real := ∫ z : Fin N -> Omega,
∑ i, (w (designVector design z) i) ^ 2 ∂μN
have hdesignN : Measurable (designVector (N := N) design) :=
measurable_designVector design hdesign
have hSmeas : Measurable S := by
apply measurable_sum
intro i hi
exact ((measurable_pi_apply i).comp (hw.comp hdesignN)).mul
((hY.comp (measurable_pi_apply i)).sub
(hmD.comp (hdesign.comp (measurable_pi_apply i))))
have hSLp : MemLp S 2 μN := by
apply (memLp_two_iff_integrable_sq hSmeas.aestronglyMeasurable).2
simpa [S, μN] using hsum_sq
have hCS : (∫ z, abs (S z) ∂μN) ≤
sqrt (∫ z, (S z) ^ 2 ∂μN) := by
simpa [Real.norm_eq_abs] using
Causalean.Mathlib.Probability.ConvergingTogether.integral_abs_le_sqrt_integral_sq
μN S hSLp
have hL2 : (∫ z, (S z) ^ 2 ∂μN) ≤ (1 / 4 : Real) * A := by
simpa [S, A, μN] using
product_weighted_centered_sq_integral_le P design hdesign Y hY hY_nonneg
hY_le_one mD hmD hcond w hw hweight_sq hsum_sq
have hA0 : 0 ≤ A := by
apply integral_nonneg_of_ae
filter_upwards with z
exact sum_nonneg fun i _ => sq_nonneg _
have hsqrt : sqrt ((1 / 4 : Real) * A) =
(1 / 2 : Real) * sqrt A := by
calc
sqrt ((1 / 4 : Real) * A) =
sqrt (((1 / 2 : Real) * sqrt A) ^ 2) := by
congr 1
rw [pow_two]
calc
(1 / 4 : Real) * A =
(1 / 4 : Real) * (sqrt A * sqrt A) := by
rw [Real.mul_self_sqrt hA0]
_ = (1 / 2 : Real) * sqrt A *
((1 / 2 : Real) * sqrt A) := by ring
_ = (1 / 2 : Real) * sqrt A :=
Real.sqrt_sq (mul_nonneg (by norm_num) (Real.sqrt_nonneg A))
change (∫ z, abs (S z) ∂μN) ≤ (1 / 2 : Real) * sqrt A
calc
(∫ z, abs (S z) ∂μN) ≤ sqrt (∫ z, (S z) ^ 2 ∂μN) := hCS
_ ≤ sqrt ((1 / 4 : Real) * A) := Real.sqrt_le_sqrt hL2
_ = (1 / 2 : Real) * sqrt A := hsqrt
2 supporting declarations (lemmas, instances)
-
measurable_designVectortheorem — For a design map that is measurable, the corresponding finite-sample vector of design values is measurable.hypothesesconclusionMeasurable (designVector (N := N) design)Proof (Lean source)
@[fun_prop] theorem measurable_designVector {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] (design : Omega -> D) (hdesign : Measurable design) : Measurable (designVector (N := N) design) := by rw [measurable_pi_iff] intro i exact hdesign.comp (measurable_pi_apply i) -
product_weighted_centered_sq_integral_letheorem — For a one-observation probability law, a measurable design map, a measurable outcome confined to the unit interval, a measurable design regression that is its conditional expectation, a measurable array of weights depending on the full design vector, and the two natural square-integrability conditions, the second moment of the weighted centered sum is at most one quarter of the expected sum of squared weights.hypothesesN :Omega D :P :Measure Omegadesign :Omega -> Dhdesign :Measurable designY :Omega -> RealhY :hY_nonneg :forall omega, 0 <= Y omegahY_le_one :forall omega, Y omega <= 1mD :D -> RealhmD :Measurable mDhcond :P[Y | comap design inferInstance] =ᵐ[P] mD ∘ designhw :hweight_sq :Integrable (fun z : Fin N -> Omega => ∑ i, (w (designVector design z) i) ^ 2) (Measure.pi (fun _ : Fin N => P))hsum_sq :Integrable (fun z : Fin N -> Omega => (weightedCenteredSum design Y mD w z) ^ 2) (Measure.pi (fun _ : Fin N => P))conclusion(∫ z : Fin N -> Omega, (weightedCenteredSum design Y mD w z) ^ 2 ∂(Measure.pi (fun _ : Fin N => P))) <= (1 / 4 : Real) * (∫ z : Fin N -> Omega, ∑ i, (w (designVector design z) i) ^ 2 ∂(Measure.pi (fun _ : Fin N => P)))Proof (Lean source)
theorem product_weighted_centered_sq_integral_le {N : Nat} {Omega D : Type*} [MeasurableSpace Omega] [MeasurableSpace D] (P : Measure Omega) [IsProbabilityMeasure P] (design : Omega -> D) (hdesign : Measurable design) (Y : Omega -> Real) (hY : Measurable Y) (hY_nonneg : forall omega, 0 <= Y omega) (hY_le_one : forall omega, Y omega <= 1) (mD : D -> Real) (hmD : Measurable mD) (hcond : P[Y | comap design inferInstance] =ᵐ[P] mD ∘ design) (w : (Fin N -> D) -> Fin N -> Real) (hw : Measurable w) (hweight_sq : Integrable (fun z : Fin N -> Omega => ∑ i, (w (designVector design z) i) ^ 2) (Measure.pi (fun _ : Fin N => P))) (hsum_sq : Integrable (fun z : Fin N -> Omega => (weightedCenteredSum design Y mD w z) ^ 2) (Measure.pi (fun _ : Fin N => P))) : (∫ z : Fin N -> Omega, (weightedCenteredSum design Y mD w z) ^ 2 ∂(Measure.pi (fun _ : Fin N => P))) <= (1 / 4 : Real) * (∫ z : Fin N -> Omega, ∑ i, (w (designVector design z) i) ^ 2 ∂(Measure.pi (fun _ : Fin N => P))) := by cases N with | zero => simp [weightedCenteredSum] | succ n => let μN : Measure (Fin (n + 1) -> Omega) := Measure.pi fun _ : Fin (n + 1) => P let W : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => w (designVector design z) i let R : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => Y (z i) - mD (design (z i)) let X : Fin (n + 1) -> (Fin (n + 1) -> Omega) -> Real := fun i z => W i z * R i z have hdesignN : Measurable (designVector (N := n + 1) design) := measurable_designVector design hdesign have hWmeas (i : Fin (n + 1)) : Measurable (W i) := by exact (measurable_pi_apply i).comp (hw.comp hdesignN) have hRmeas (i : Fin (n + 1)) : Measurable (R i) := by exact (hY.comp (measurable_pi_apply i)).sub (hmD.comp (hdesign.comp (measurable_pi_apply i))) have hXmeas (i : Fin (n + 1)) : Measurable (X i) := (hWmeas i).mul (hRmeas i) have henergyMeas : Measurable (fun z : Fin (n + 1) -> Omega => ∑ i, (W i z) ^ 2) := measurable_sum _ fun i _ => (hWmeas i).pow_const 2 obtain ⟨hYInt, hmInt, hm_nonneg, hm_le_one, hcenter⟩ := residual_facts P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond have hRbound (i : Fin (n + 1)) : ∀ᵐ z ∂μN, ‖R i z‖ ≤ (2 : Real) := by have hmp := measurePreserving_eval (fun _ : Fin (n + 1) => P) i have hm0 := hmp.quasiMeasurePreserving.tendsto_ae.eventually hm_nonneg have hm1 := hmp.quasiMeasurePreserving.tendsto_ae.eventually hm_le_one filter_upwards [hm0, hm1] with z hz0 hz1 change 0 ≤ mD (design (z i)) at hz0 change mD (design (z i)) ≤ 1 at hz1 rw [Real.norm_eq_abs] apply abs_le.2 constructor <;> linarith [hY_nonneg (z i), hY_le_one (z i)] have hWiSq (i : Fin (n + 1)) : Integrable (fun z => (W i z) ^ 2) μN := by apply Integrable.mono hweight_sq ((hWmeas i).pow_const 2).aestronglyMeasurable filter_upwards with z rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _), Real.norm_eq_abs, abs_of_nonneg (sum_nonneg fun _ _ => sq_nonneg _)] exact Finset.single_le_sum (s := univ) (f := fun k : Fin (n + 1) => (W k z) ^ 2) (fun k _ => sq_nonneg (W k z)) (Finset.mem_univ i) have hXiSq (i : Fin (n + 1)) : Integrable (fun z => (X i z) ^ 2) μN := by apply (hWiSq i).const_mul 4 |>.mono' · exact (hXmeas i).pow_const 2 |>.aestronglyMeasurable · filter_upwards [hRbound i] with z hr change ‖(X i z) ^ 2‖ ≤ (4 : Real) * (W i z) ^ 2 rw [Real.norm_eq_abs, abs_of_nonneg (sq_nonneg _)] change (W i z * R i z) ^ 2 ≤ 4 * W i z ^ 2 rw [Real.norm_eq_abs] at hr have hrsq : (R i z) ^ 2 ≤ 4 := by rw [← sq_abs] have hs := (sq_le_sq₀ (abs_nonneg (R i z)) (by norm_num)).2 hr norm_num at hs ⊢ exact hs rw [mul_pow] calc W i z ^ 2 * R i z ^ 2 ≤ W i z ^ 2 * 4 := mul_le_mul_of_nonneg_left hrsq (sq_nonneg _) _ = 4 * W i z ^ 2 := by ring have hcrossInt (i j : Fin (n + 1)) : Integrable (fun z => X i z * X j z) μN := by apply (hXiSq i).add (hXiSq j) |>.mono' · exact (hXmeas i).mul (hXmeas j) |>.aestronglyMeasurable · filter_upwards with z rw [Real.norm_eq_abs] have ha : 0 ≤ |X i z| := abs_nonneg _ have hb : 0 ≤ |X j z| := abs_nonneg _ have hab : |X i z * X j z| = |X i z| * |X j z| := abs_mul _ _ rw [hab] have hsq := sq_nonneg (|X i z| - |X j z|) have hi : (X i z) ^ 2 = |X i z| ^ 2 := (sq_abs _).symm have hj : (X j z) ^ 2 = |X j z| ^ 2 := (sq_abs _).symm change |X i z| * |X j z| ≤ (X i z) ^ 2 + (X j z) ^ 2 rw [hi, hj] nlinarith [sq_nonneg |X i z|, sq_nonneg |X j z|] have hdiag (i : Fin (n + 1)) : (∫ z, (X i z) ^ 2 ∂μN) ≤ (1 / 4 : Real) * ∫ z, (W i z) ^ 2 ∂μN := by simpa [μN, X, W, R] using product_diag_integral_le P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond w hw i (hXiSq i) (hWiSq i) have hcross (i j : Fin (n + 1)) (hij : i ≠ j) : (∫ z, X i z * X j z ∂μN) = 0 := by simpa [μN, X, W, R] using product_cross_integral_eq_zero P design hdesign Y hY hY_nonneg hY_le_one mD hmD hcond w hw i j hij (hcrossInt i j) have hsquare (z : Fin (n + 1) -> Omega) : (weightedCenteredSum design Y mD w z) ^ 2 = ∑ i, ∑ j, X i z * X j z := by rw [pow_two] simp only [weightedCenteredSum, X, W, R] rw [Finset.sum_mul_sum] have hsumIntegral : (∫ z, (weightedCenteredSum design Y mD w z) ^ 2 ∂μN) = ∑ i, ∑ j, ∫ z, X i z * X j z ∂μN := by rw [integral_congr_ae (Filter.Eventually.of_forall hsquare)] rw [integral_finsetSum univ] · apply Finset.sum_congr rfl intro i hi rw [integral_finsetSum univ] intro j hj exact hcrossInt i j · intro i hi exact integrable_finsetSum univ fun j _ => hcrossInt i j have hcollapse (i : Fin (n + 1)) : (∑ j, ∫ z, X i z * X j z ∂μN) = ∫ z, (X i z) ^ 2 ∂μN := by rw [Finset.sum_eq_single i] · apply integral_congr_ae filter_upwards with z rw [pow_two] · intro j hj hji exact hcross i j (Ne.symm hji) · simp have henergyIntegral : (∫ z, ∑ i, (W i z) ^ 2 ∂μN) = ∑ i, ∫ z, (W i z) ^ 2 ∂μN := by exact integral_finsetSum univ fun i _ => hWiSq i change (∫ z, (weightedCenteredSum design Y mD w z) ^ 2 ∂μN) ≤ (1 / 4 : Real) * ∫ z, ∑ i, (W i z) ^ 2 ∂μN rw [hsumIntegral] simp_rw [hcollapse] rw [henergyIntegral, Finset.mul_sum] exact Finset.sum_le_sum fun i _ => hdiag i