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.
ConvergingTogether 4 core · 4 supporting · 2 submodules This namespace collects the reusable pieces for the converging-together theorem. FiniteMarkedPoissonPartition 36 to review
36 core · 52 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 6 core · 3 supporting · 3 submodules Kernel-measure probability helpers: graph-map product identities and composition-product assembly lemmas for conditional-law arguments. SteinMethod 13 core · 25 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
The standard-normal density φ(x) = exp(-x²/2)/√(2π) (= gaussianPDFReal 0 1).
Definition (Lean source)
noncomputable def stdNormalPDF (x : ℝ) : ℝ := gaussianPDFReal 0 1 x
def stdNormalCDF reviewed
⚑ flagged
Causalean.Mathlib
The standard-normal CDF Φ(x) = P(N(0,1) ≤ x), packaged from Mathlib's cdf.
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)
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
The probit Φ⁻¹(p): the standard-normal quantile, the generalized inverse of Φ.
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)
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 1 to review 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
The Bernoulli law on ℝ with success probability p. Concentrates ENNReal.ofReal p on 1 and ENNReal.ofReal (1 − p) on 0.
Definition (Lean source)
noncomputable def bernoulliLaw (p : ℝ) : Measure ℝ :=
ofReal p • Measure.dirac (1 : ℝ)
+ ofReal (1 - p) • Measure.dirac (0 : ℝ)
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
The Boolean Bernoulli distribution assigns success probability to truth and failure probability to falsehood. It is the same two-point law as the existing real-valued Bernoulli distribution on zero and one, but its Boolean values make it usable as a Markov kernel into a Boolean coordinate of a potential-outcome tuple.
def binomialWeight unreviewed
⚑ flagged
Causalean.Mathlib.Probability
The real binomial weight of count j among m trials with success parameter p.
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)
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)
-
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, .
Formal statement
hypotheses
conclusion
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.hypothesesconclusionProof (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
hypotheses
conclusion
IsGaussian (P.map X) ∧ IsGaussian (P.map Y)
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.hypothesesProof (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) := mX.add mY have mSub : Measurable (X - Y) := mX.sub mY 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.Proof (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
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)
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)
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|) μ := integrable_finset_sum _ fun i _ => (hv i).abs 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
The conditional quantile at level τ: the generalized inverse of the conditional CDF, q(a) = inf { x : ℝ | τ(a) ≤ condCDF ρ a x }.
Definition (Lean source)
noncomputable def condQuantile (ρ : Measure (α × ℝ)) (τ : α → ℝ) (a : α) : ℝ :=
sInf {x : ℝ | τ a ≤ condCDF ρ a x}
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
conclusion
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.hypothesesconclusionx' ∈ {y : ℝ | τ a ≤ condCDF ρ a y} -
bddBelow_condQuantileSetlemma — At a strictly positive conditional-quantile level, the response values whose conditional cumulative distribution function reaches that level are bounded below.hypothesesProof (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.hypothesesconclusion({x : ℝ | τ a ≤ condCDF ρ a x}).NonemptyProof (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.hypothesesconclusionτ a ≤ condCDF ρ a (condQuantile ρ τ a)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
Symmetric two-point mean channel. For a scale B and a target mean u, the law twoPointMean B u on {−B, B} puts mass (1 + u/B)/2 on B and (1 − u/B)/2 on −B; its mean is u.
Definition (Lean source)
noncomputable def twoPointMean (B u : ℝ) : Measure ℝ :=
ofReal ((1 + u / B) / 2) • Measure.dirac B
+ ofReal ((1 - u / B) / 2) • Measure.dirac (-B)
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| ≤ Bconclusion0 ≤ (1 + u / B) / 2 ∧ 0 ≤ (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