PhD: Conditional variance (#20)

Define the conditional variance of a real-valued random variable

Co-authored-by: Kexing Ying <[email protected]>

LeanCamCombi.lean

@@ -51,19 +51,27 @@ import LeanCamCombi.Mathlib.Data.Set.Image
 import LeanCamCombi.Mathlib.Data.Set.Pointwise.SMul
 import LeanCamCombi.Mathlib.GroupTheory.OrderOfElement
 import LeanCamCombi.Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
+import LeanCamCombi.Mathlib.MeasureTheory.Function.L1Space
+import LeanCamCombi.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
 import LeanCamCombi.Mathlib.MeasureTheory.Measure.Haar.NormedSpace
+import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
 import LeanCamCombi.Mathlib.Order.BooleanSubalgebra
 import LeanCamCombi.Mathlib.Order.Flag
 import LeanCamCombi.Mathlib.Order.Partition.Finpartition
 import LeanCamCombi.Mathlib.Order.RelIso.Group
 import LeanCamCombi.Mathlib.Probability.ProbabilityMassFunction.Constructions
+import LeanCamCombi.Mathlib.Probability.Variance
 import LeanCamCombi.Mathlib.RingTheory.FinitePresentation
 import LeanCamCombi.Mathlib.RingTheory.Spectrum.Prime.Topology
 import LeanCamCombi.Mathlib.Topology.MetricSpace.MetricSeparated
 import LeanCamCombi.MetricBetween
 import LeanCamCombi.MinkowskiCaratheodory
 import LeanCamCombi.Multipartite
 import LeanCamCombi.PhD.VCDim.AddVCDim
+import LeanCamCombi.PhD.VCDim.CondVar
 import LeanCamCombi.PhD.VCDim.HausslerPacking
 import LeanCamCombi.PhD.VCDim.HypercubeEdges
 import LeanCamCombi.PlainCombi.LittlewoodOfford

LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean

@@ -0,0 +1,13 @@
+import Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
+
+open Filter
+
+namespace MeasureTheory
+variable {α β γ : Type*}
+  {m₀ m : MeasurableSpace α} {μ : Measure α} [TopologicalSpace β] [TopologicalSpace γ]
+
+/-- The composition of a continuous function and an ae strongly measurable function is ae strongly
+measurable. -/
+lemma _root_.Continuous.comp_aestronglyMeasurable' {g : β → γ} {f : α → β} (hg : Continuous g)
+    (hf : AEStronglyMeasurable' m₀ f μ) : AEStronglyMeasurable' m₀ (fun x => g (f x)) μ :=
+  ⟨_, hg.comp_stronglyMeasurable hf.stronglyMeasurable_mk, EventuallyEq.fun_comp hf.ae_eq_mk g⟩

LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Basic.lean

@@ -0,0 +1,65 @@
+import Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
+import LeanCamCombi.Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+
+/-!
+# TODO
+
+* Rename `condexp` to `condExp`
+* Golf `condexp_const`, no `@`
+* Remove useless `haveI`/`letI`
+* Make `m` explicit in `condexp_add`, `condexp_sub`, etc...
+* See https://leanprover.zulipchat.com/#narrow/channel/217875-Is-there-code-for-X.3F/topic/Conditional.20expectation.20of.20product
+  for how to prove that we can pull `m`-measurable continuous linear maps out of the `m`-conditional
+  expectation.
+-/
+
+open scoped ENNReal
+
+namespace MeasureTheory
+variable {Ω R E : Type*} {f : Ω → E}
+  {m m₀ : MeasurableSpace Ω} {μ : Measure Ω} {s : Set Ω}
+  [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E]
+
+attribute [simp] condexp_const
+
+alias condexp_of_not_integrable := condexp_undef
+
+section NormedRing
+variable [NormedRing R] [NormedSpace ℝ R] [CompleteSpace R] {f g : Ω → R}
+
+lemma condexp_ofNat (n : ℕ) [n.AtLeastTwo] (f : Ω → R) :
+    μ[OfNat.ofNat n * f|m] =ᵐ[μ] OfNat.ofNat n * μ[f|m] := by
+  simpa [Nat.cast_smul_eq_nsmul] using condexp_smul (μ := μ) (m := m) (n : ℝ) f
+
+end NormedRing
+
+variable [IsFiniteMeasure μ] [InnerProductSpace ℝ E]
+
+lemma Memℒp.condexpL2_ae_eq_condexp (hm : m ≤ m₀) (hf : Memℒp f 2 μ) :
+    condexpL2 E ℝ hm hf.toLp =ᵐ[μ] μ[f | m] := by
+  refine ae_eq_condexp_of_forall_setIntegral_eq hm
+    (memℒp_one_iff_integrable.1 <| hf.mono_exponent one_le_two)
+    (fun s hs htop ↦ integrableOn_condexpL2_of_measure_ne_top hm htop.ne _) (fun s hs htop ↦ ?_)
+    (aeStronglyMeasurable'_condexpL2 hm _)
+  rw [integral_condexpL2_eq hm (hf.toLp _) hs htop.ne]
+  refine setIntegral_congr_ae (hm _ hs) ?_
+  filter_upwards [hf.coeFn_toLp] with ω hω _ using hω
+
+lemma eLpNorm_condexp_le : eLpNorm (μ[f | m]) 2 μ ≤ eLpNorm f 2 μ := by
+  by_cases hm : m ≤ m₀; swap
+  · simp [condexp_of_not_le hm]
+  by_cases hfm : AEStronglyMeasurable f μ; swap
+  · rw [condexp_undef (by simp [Integrable, not_and_of_not_left _ hfm])]
+    simp
+  obtain hf | hf := eq_or_ne (eLpNorm f 2 μ) ∞
+  · simp [hf]
+  replace hf : Memℒp f 2 μ := ⟨hfm, Ne.lt_top' fun a ↦ hf (id (Eq.symm a))⟩
+  rw [← eLpNorm_congr_ae (hf.condexpL2_ae_eq_condexp hm)]
+  refine le_trans (eLpNorm_condexpL2_le hm _) ?_
+  rw [eLpNorm_congr_ae hf.coeFn_toLp]
+
+protected lemma Memℒp.condexp (hf : Memℒp f 2 μ) : Memℒp (μ[f | m]) 2 μ := by
+  by_cases hm : m ≤ m₀
+  · exact ⟨(stronglyMeasurable_condexp.mono hm).aestronglyMeasurable,
+      eLpNorm_condexp_le.trans_lt hf.eLpNorm_lt_top⟩
+  · simp [condexp_of_not_le hm]

LeanCamCombi/Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean

@@ -0,0 +1,9 @@
+import Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
+
+namespace MeasureTheory
+variable {α : Type*} {m m₀ : MeasurableSpace α} {μ : Measure[m₀] α}
+
+/-- Pull-out property of the conditional expectation. -/
+lemma condexp_mul_stronglyMeasurable {f g : α → ℝ} (hg : StronglyMeasurable[m] g)
+    (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : μ[f * g | m] =ᵐ[μ] μ[f | m] * g := by
+  simpa [mul_comm] using condexp_stronglyMeasurable_mul hg (mul_comm f g ▸ hfg) hf

LeanCamCombi/Mathlib/MeasureTheory/Function/L1Space.lean

@@ -0,0 +1,11 @@
+import Mathlib.MeasureTheory.Function.L1Space
+import LeanCamCombi.Mathlib.MeasureTheory.Measure.Typeclasses
+
+namespace MeasureTheory
+variable {α β : Type*} {m : MeasurableSpace α} {μ : Measure α} [NormedAddCommGroup β] {c : β}
+
+lemma integrable_const_iff_isFiniteMeasure (hc : c ≠ 0) :
+    Integrable (fun _ ↦ c) μ ↔ IsFiniteMeasure μ := by
+  simp [integrable_const_iff, hc, isFiniteMeasure_iff]
+
+end MeasureTheory

LeanCamCombi/Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean

@@ -0,0 +1,7 @@
+import Mathlib.MeasureTheory.Function.LpSeminorm.Basic
+
+namespace MeasureTheory
+
+-- TODO: Replace
+@[simp] alias Memℒp.zero := zero_memℒp
+@[simp] alias Memℒp.zero' := zero_mem_ℒp'

LeanCamCombi/Mathlib/MeasureTheory/Measure/Typeclasses.lean

@@ -0,0 +1,5 @@
+import Mathlib.MeasureTheory.Measure.Typeclasses
+
+namespace MeasureTheory
+
+attribute [mk_iff] IsFiniteMeasure

LeanCamCombi/Mathlib/Probability/Variance.lean

@@ -0,0 +1,13 @@
+import Mathlib.Probability.Variance
+
+open MeasureTheory
+open scoped ENNReal
+
+namespace ProbabilityTheory
+variable {Ω : Type*} {m : MeasurableSpace Ω} {X Y : Ω → ℝ} {μ : Measure Ω} {s : Set Ω}
+
+scoped notation "Var[" X " ; " μ "]" => ProbabilityTheory.variance X μ
+
+lemma variance_eq_integral (hX : AEMeasurable (fun ω ↦ (‖X ω - ∫ ω', X ω' ∂μ‖₊ : ℝ≥0∞) ^ 2) μ) :
+    Var[X ; μ] = ∫ ω, (X ω - μ[X]) ^ 2 ∂μ := by
+  simp [variance, evariance, ← integral_toReal hX (by simp [← ENNReal.coe_pow])]

LeanCamCombi/PhD/VCDim/CondVar.lean

@@ -0,0 +1,194 @@
+/-
+Copyright (c) 2025 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import Mathlib.MeasureTheory.Integral.Average
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
+import LeanCamCombi.Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
+import LeanCamCombi.Mathlib.MeasureTheory.Function.L1Space
+import LeanCamCombi.Mathlib.Probability.Variance
+
+/-!
+# Conditional variance
+
+This file defines the variance of a real-valued random variable conditional to a sigma-algebra.
+
+## TODO
+
+Define the Lebesgue conditional variance (see GibbsMeasure for a definition of the Lebesgue
+conditional expectation).
+-/
+
+open MeasureTheory Filter
+open scoped ENNReal
+
+namespace ProbabilityTheory
+variable {Ω : Type*} {m₀ m : MeasurableSpace Ω} {hm : m ≤ m₀} {X Y : Ω → ℝ} {μ : Measure[m₀] Ω}
+  {s : Set Ω}
+
+variable (m X μ) in
+/-- Conditional variance of a real-valued random variable. It is defined as 0 if any one of the
+following conditions is true:
+- `m` is not a sub-σ-algebra of `m₀`,
+- `μ` is not σ-finite with respect to `m`,
+- `X` is not square-integrable. -/
+noncomputable def condVar : Ω → ℝ := μ[(X - μ[X | m]) ^ 2 | m]
+
+@[inherit_doc] scoped notation "Var[" X " ; " μ " | " m "]" => condVar m X μ
+
+lemma condVar_of_not_le (hm : ¬m ≤ m₀) : Var[X ; μ | m] = 0 := by rw [condVar, condexp_of_not_le hm]
+
+lemma condVar_of_not_sigmaFinite (hμm : ¬SigmaFinite (μ.trim hm)) :
+    Var[X ; μ | m] = 0 := by rw [condVar, condexp_of_not_sigmaFinite hm hμm]
+
+open scoped Classical in
+lemma condVar_of_sigmaFinite [SigmaFinite (μ.trim hm)] :
+    Var[X ; μ | m] =
+      if Integrable (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) μ then
+        if StronglyMeasurable[m] (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) then
+          fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2
+        else aestronglyMeasurable'_condexpL1.mk (condexpL1 hm μ fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2)
+      else 0 := condexp_of_sigmaFinite _
+
+lemma condVar_of_stronglyMeasurable [SigmaFinite (μ.trim hm)]
+    (hX : StronglyMeasurable[m] X) (hXint : Integrable ((X - μ[X | m]) ^ 2) μ) :
+    Var[X ; μ | m] = fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2 :=
+  condexp_of_stronglyMeasurable _ ((hX.sub stronglyMeasurable_condexp).pow _) hXint
+
+lemma condVar_of_not_integrable (hXint : ¬ Integrable (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) μ) :
+    Var[X ; μ | m] = 0 := condexp_of_not_integrable hXint
+
+@[simp]
+lemma condVar_zero : Var[0 ; μ | m] = 0 := by
+  by_cases hm : m ≤ m₀
+  swap; · rw [condVar_of_not_le hm]
+  by_cases hμm : SigmaFinite (μ.trim hm)
+  swap; · rw [condVar_of_not_sigmaFinite hμm]
+  rw [condVar_of_stronglyMeasurable stronglyMeasurable_zero]
+  · simp [← Pi.zero_def]
+  · simpa [-integrable_zero] using integrable_zero ..
+
+@[simp]
+lemma condVar_const (hm : m ≤ m₀) (c : ℝ) : Var[fun _ ↦ c ; μ | m] = 0 := by
+  obtain rfl | hc := eq_or_ne c 0
+  · simp [← Pi.zero_def]
+  by_cases hμm : IsFiniteMeasure μ
+  · simp [condVar, hm, Pi.pow_def]
+  · simp [condVar, condexp_of_not_integrable, integrable_const_iff_isFiniteMeasure hc,
+      integrable_const_iff_isFiniteMeasure <| pow_ne_zero _ hc, hμm, Pi.pow_def]
+
+lemma condVar_ae_eq_condexpL1 [hμm : SigmaFinite (μ.trim hm)] (X : Ω → ℝ) :
+    Var[X ; μ | m] =ᵐ[μ] condexpL1 hm μ (fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2) :=
+  condexp_ae_eq_condexpL1 ..
+
+lemma condVar_ae_eq_condexpL1CLM [SigmaFinite (μ.trim hm)]
+    (hX : Integrable (fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) μ) :
+    Var[X ; μ | m] =ᵐ[μ] condexpL1CLM _ hm μ (hX.toL1 fun ω ↦ (X ω - (μ[X | m]) ω) ^ 2) :=
+  condexp_ae_eq_condexpL1CLM ..
+
+lemma stronglyMeasurable_condVar : StronglyMeasurable[m] (Var[X ; μ | m]) :=
+  stronglyMeasurable_condexp
+
+lemma condVar_congr_ae (h : X =ᵐ[μ] Y) : Var[X ; μ | m] =ᵐ[μ] Var[Y ; μ | m] :=
+  condexp_congr_ae <| by filter_upwards [h, condexp_congr_ae h] with ω hω hω'; dsimp; rw [hω, hω']
+
+lemma condVar_of_aestronglyMeasurable' [hμm : SigmaFinite (μ.trim hm)]
+    (hX : AEStronglyMeasurable' m X μ) (hXint : Integrable (fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2) μ) :
+    Var[X ; μ | m] =ᵐ[μ] fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2 :=
+  condexp_of_aestronglyMeasurable' _ ((continuous_pow _).comp_aestronglyMeasurable'
+    (hX.sub stronglyMeasurable_condexp.aeStronglyMeasurable')) hXint
+
+lemma integrable_condVar : Integrable Var[X ; μ | m] μ := by
+  by_cases hm : m ≤ m₀
+  swap; · rw [condVar_of_not_le hm]; exact integrable_zero _ _ _
+  by_cases hμm : SigmaFinite (μ.trim hm)
+  swap; · rw [condVar_of_not_sigmaFinite hμm]; exact integrable_zero _ _ _
+  haveI : SigmaFinite (μ.trim hm) := hμm
+  exact (integrable_condexpL1 _).congr (condVar_ae_eq_condexpL1 X).symm
+
+/-- The integral of the conditional expectation `μ[X | m]` over an `m`-measurable set is equal to
+the integral of `X` on that set. -/
+lemma setIntegral_condVar [SigmaFinite (μ.trim hm)]
+    (hX : Integrable (fun ω ↦ (X ω - (μ[X|m]) ω) ^ 2) μ) (hs : MeasurableSet[m] s) :
+    ∫ ω in s, (Var[X ; μ | m]) ω ∂μ = ∫ ω in s, (X ω - (μ[X|m]) ω) ^ 2 ∂μ :=
+  setIntegral_condexp _ hX hs
+
+lemma condVar_ae_eq_condexp_sq_sub_condexp_sq (hm : m ≤ m₀) [IsFiniteMeasure μ]
+    (hX : Memℒp X 2 μ) :
+    Var[X ; μ | m] =ᵐ[μ] μ[X ^ 2 | m] - μ[X | m] ^ 2 := by
+  calc
+    Var[X ; μ | m]
+    _ = μ[X ^ 2 - 2 * X * μ[X|m] + μ[X|m] ^ 2 | m] := by rw [condVar, sub_sq]
+    _ =ᵐ[μ] μ[X ^ 2 | m] - 2 * μ[X | m] ^ 2 + μ[X | m] ^ 2 := by
+      have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
+      have aux₁ : Integrable (2 * X * μ[X|m]) μ := by
+        rw [(_ : 2 * X * μ[X|m] = fun ω ↦ 2 * (X ω * (μ[X|m]) ω))]
+        swap; ext ω; simp [mul_assoc]
+        have aux₁' : Memℒp (X * μ[X | m]) 1 μ := by
+          refine @Memℒp.mul Ω m₀ _ _ _ 1 2 2 _ _ hX.condexp hX ?_
+          simp [ENNReal.inv_two_add_inv_two]
+        exact Integrable.const_mul (memℒp_one_iff_integrable.1 aux₁') (2 : ℝ)
+      have aux₂ : Integrable (μ[X|m] ^ 2) μ := hX.condexp.integrable_sq
+      filter_upwards [condexp_add (m := m) (aux₀.sub aux₁) aux₂, condexp_sub (m := m) aux₀ aux₁,
+        condexp_mul_stronglyMeasurable stronglyMeasurable_condexp aux₁
+          ((hX.integrable one_le_two).const_mul _), condexp_ofNat (m := m) 2 X]
+        with ω hω₀ hω₁ hω₂ hω₃
+      simp [hω₀, hω₁, hω₂, hω₃, condexp_const,
+        condexp_of_stronglyMeasurable hm (stronglyMeasurable_condexp.pow _) aux₂]
+      simp [mul_assoc, sq]
+    _ = μ[X ^ 2 | m] - μ[X | m] ^ 2 := by ring
+
+lemma condVar_ae_le_condexp_sq (hm : m ≤ m₀) [IsFiniteMeasure μ] (hX : Memℒp X 2 μ) :
+    Var[X ; μ | m] ≤ᵐ[μ] μ[X ^ 2 | m] := by
+  filter_upwards [condVar_ae_eq_condexp_sq_sub_condexp_sq hm hX] with ω hω
+  dsimp at hω
+  nlinarith
+
+/-- **Law of total variance** -/
+lemma integral_condVar_add_variance_condexp (hm : m ≤ m₀) [IsProbabilityMeasure μ]
+    (hX : Memℒp X 2 μ) : μ[Var[X ; μ | m]] + Var[μ[X | m] ; μ] = Var[X ; μ] := by
+  calc
+    μ[Var[X ; μ | m]] + Var[μ[X | m] ; μ]
+    _ = μ[(μ[X ^ 2 | m] - μ[X | m] ^ 2 : Ω → ℝ)] + (μ[μ[X | m] ^ 2] - μ[μ[X | m]] ^ 2) := by
+      congr 1
+      · exact integral_congr_ae <| condVar_ae_eq_condexp_sq_sub_condexp_sq hm hX
+      · exact variance_def' hX.condexp
+    _ = μ[X ^ 2] - μ[μ[X | m] ^ 2] + (μ[μ[X | m] ^ 2] - μ[X] ^ 2) := by
+      rw [integral_sub' integrable_condexp, integral_condexp hm, integral_condexp hm]
+      exact hX.condexp.integrable_sq
+    _ = Var[X ; μ] := by rw [variance_def' hX]; ring
+
+lemma condVar_bot' [NeZero μ] (X : Ω → ℝ) :
+    Var[X ; μ | ⊥] = fun _ => ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
+  ext ω; simp [condVar, condexp_bot', average]
+
+lemma condVar_bot_ae_eq (X : Ω → ℝ) :
+    Var[X ; μ | ⊥] =ᵐ[μ] fun _ ↦ ⨍ ω, (X ω - ⨍ ω', X ω' ∂μ) ^ 2 ∂μ := by
+  obtain rfl | hμ := eq_zero_or_neZero μ
+  · rw [ae_zero]
+    exact eventually_bot
+  · exact .of_forall <| congr_fun (condVar_bot' X)
+
+lemma condVar_bot [IsProbabilityMeasure μ] (hX : Memℒp X 2 μ) :
+    Var[X ; μ | ⊥] = fun _ω ↦ Var[X ; μ] := by
+  simp [condVar_bot', average_eq_integral, hX.variance_eq]
+
+lemma condVar_smul (c : ℝ) (X : Ω → ℝ) : Var[c • X ; μ | m] =ᵐ[μ] c ^ 2 • Var[X ; μ | m] := by
+  calc
+    Var[c • X ; μ | m]
+    _ =ᵐ[μ] μ[c ^ 2 • (X - μ[X | m]) ^ 2 | m] := by
+      rw [condVar]
+      refine condexp_congr_ae ?_
+      filter_upwards [condexp_smul (m := m) c X] with ω hω
+      simp [hω, ← mul_sub, mul_pow]
+    _ =ᵐ[μ] c ^ 2 • Var[X ; μ | m] := condexp_smul ..
+
+@[simp] lemma condVar_neg (X : Ω → ℝ) : Var[-X ; μ | m] =ᵐ[μ] Var[X ; μ | m] := by
+  refine condexp_congr_ae ?_
+  filter_upwards [condexp_neg (m := m) X] with ω hω
+  simp [condVar, hω]
+  ring
+
+end ProbabilityTheory