Mathlib.Probability.Independence.Conditional
Tools for working with conditional independence of random variables and σ-algebras.
DensityIntersection 32 core · 30 supporting · 8 submodules Positive-density graphoid intersection for conditional independence. ThreeBlockShiftedProduct 3 core · 2 supporting · 1 submodule Held-out scores are shifted by measurable training-block functions. Transport 2 core · 6 supporting · 1 submodule Transport of conditional-independence statements along measurable maps and almost-everywhere retractions.
AELift 1 core · 3 supporting This file proves generic almost-everywhere equality lifting lemmas under an overlap-style null-set hypothesis. ★ ae_eq_of_ae_eq_restrict_arm
Almost-Everywhere Lifts Under Overlap
This file proves generic almost-everywhere equality lifting lemmas under an overlap-style null-set hypothesis.
The exported support lemmas convert between restricted a.e. equality and
indicator equality (indicator_aeEq_of_aeEq_restrict,
aeEq_restrict_of_indicator_aeEq) and propagate vanishing through conditional
expectation (condExp_indicator_aeEq_zero). The main public theorem is
ae_eq_of_ae_eq_restrict_arm.
theorem ae_eq_of_ae_eq_restrict_arm reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Restricted-set a.e.-equality lift for σ-measurable functions. For a sub-σ-algebra m such that m is coarser than the ambient σ-algebra, if f and g agree on an m-measurable set, they agree almost everywhere on the restriction of the measure to a set E, and every m-measurable set whose intersection with E is null is itself null, then f and g agree almost everywhere on the whole space.
Formal statement
hypotheses
Ω :
Type*
m :
hm :
m ≤ mΩ
μ :
@Measure Ω mΩ
E :
Set Ω
β :
Type*
Ω → β
h_eq_meas :
MeasurableSet[m] {ω | f ω = g ω}
_h :
f =ᵐ[μ.restrict E] g
_h_overlap :
∀ s : Set Ω
conclusion
f =ᵐ[μ] g
Proof (Lean source)
theorem ae_eq_of_ae_eq_restrict_arm
{Ω : Type*} {mΩ : MeasurableSpace Ω}
(m : MeasurableSpace Ω) (hm : m ≤ mΩ)
{μ : @Measure Ω mΩ}
{E : Set Ω}
{β : Type*} {f g : Ω → β}
(h_eq_meas : MeasurableSet[m] {ω | f ω = g ω})
(_h : f =ᵐ[μ.restrict E] g)
(_h_overlap : ∀ s : Set Ω, MeasurableSet[m] s →
μ (s ∩ E) = 0 → μ s = 0) :
f =ᵐ[μ] g := by
let s : Set Ω := {ω | f ω ≠ g ω}
have hs : MeasurableSet[m] s := by
simpa [s, Set.compl_setOf] using h_eq_meas.compl
have hs_ambient : @MeasurableSet Ω mΩ s := hm _ hs
have hs_arm_zero : μ (s ∩ E) = 0 := by
have hbad : (μ.restrict E) s = 0 := by
exact MeasureTheory.ae_iff.mp _h
rwa [MeasureTheory.Measure.restrict_apply hs_ambient] at hbad
have hs_zero : μ s = 0 := _h_overlap s hs hs_arm_zero
exact MeasureTheory.ae_iff.mpr hs_zero
3 supporting declarations (lemmas, instances)
-
indicator_aeEq_of_aeEq_restrictlemma — Push an a.e.-equality under μ.restrict s to a global equality of s-indicators.hypothesesΩ :hs :β :h :f =ᵐ[μ.restrict s] gconclusions.indicator f =ᵐ[μ] s.indicator gProof (Lean source)
lemma indicator_aeEq_of_aeEq_restrict {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {s : Set Ω} (hs : MeasurableSet s) {β : Type*} [Zero β] {f g : Ω → β} (h : f =ᵐ[μ.restrict s] g) : s.indicator f =ᵐ[μ] s.indicator g := by have h_on : ∀ᵐ ω ∂(μ.restrict s), s.indicator f ω = s.indicator g ω := by filter_upwards [h, ae_restrict_mem hs] with ω hω hωs rw [Set.indicator_of_mem hωs, Set.indicator_of_mem hωs, hω] have h_off : ∀ᵐ ω ∂(μ.restrict sᶜ), s.indicator f ω = s.indicator g ω := by rw [ae_restrict_iff' hs.compl] filter_upwards with ω hωs rw [Set.indicator_of_notMem hωs, Set.indicator_of_notMem hωs] exact MeasureTheory.ae_of_ae_restrict_of_ae_restrict_compl s h_on h_off -
aeEq_restrict_of_indicator_aeEqlemma — Recover a μ.restrict s a.e.-equality from a global equality of s-indicators.hypothesesΩ :hs :β :h :s.indicator f =ᵐ[μ] s.indicator gconclusionf =ᵐ[μ.restrict s] gProof (Lean source)
lemma aeEq_restrict_of_indicator_aeEq {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {s : Set Ω} (hs : MeasurableSet s) {β : Type*} [Zero β] {f g : Ω → β} (h : s.indicator f =ᵐ[μ] s.indicator g) : f =ᵐ[μ.restrict s] g := by rw [EventuallyEq, ae_restrict_iff' hs] filter_upwards [h] with ω hω hωs have hf : s.indicator f ω = f ω := Set.indicator_of_mem hωs f have hg : s.indicator g ω = g ω := Set.indicator_of_mem hωs g simpa [hf, hg] using hω -
condExp_indicator_aeEq_zerolemma — If an integrable function vanishes after restriction by an m-measurable indicator, so does its conditional expectation.hypothesesconclusions.indicator (μ[f | m]) =ᵐ[μ] 0Proof (Lean source)
lemma condExp_indicator_aeEq_zero {Ω : Type*} {mΩ : MeasurableSpace Ω} {μ : Measure Ω} {m : MeasurableSpace Ω} {s : Set Ω} (hs : MeasurableSet[m] s) {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [CompleteSpace E] {f : Ω → E} (hf : Integrable f μ) (h : s.indicator f =ᵐ[μ] 0) : s.indicator (μ[f | m]) =ᵐ[μ] 0 := by have hCE_ind := MeasureTheory.condExp_indicator (m := m) hf hs have hLHS_zero : μ[s.indicator f | m] =ᵐ[μ] 0 := by refine (MeasureTheory.condExp_congr_ae (m := m) h).trans ?_ rw [MeasureTheory.condExp_zero (m := m) (μ := μ) (E := E)] exact hCE_ind.symm.trans hLHS_zero
CondExp_Part1 1 core · 3 supporting This first half proves drop-of-conditioning and product-factorization identities implied by conditional independence. ★ condExp_mul_of_condIndep
Conditional Expectations Under Conditional Independence
This first half proves drop-of-conditioning and product-factorization identities implied by conditional independence. These identities express how irrelevant conditioning information can be removed and how conditionally independent factors separate inside conditional expectations.
The central exported lemmas are condExp_sup_comap_eq_of_condIndep_comap and
condExp_sup_comap_eq_of_condIndep for removing irrelevant conditioning
variables, condExp_mul_of_condIndep for factoring a product's conditional
expectation. CondExp_Part2.lean imports this module and adds weak union,
measurable-coordinate extension, and semigraphoid contraction.
theorem condExp_mul_of_condIndep reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Conditional-independence factorization of a product's conditional expectation. For a sub-σ-algebra m coarser than the ambient σ-algebra, measurable maps f and g that are conditionally independent given m, and measurable real-valued functions u and v such that u ∘ f, v ∘ g, and their pointwise product are all integrable, then the conditional expectation, given m, of the product (u ∘ f)·(v ∘ g) equals the product of the separate conditional expectations of u ∘ f and v ∘ g given m.
Formal statement
hypotheses
Ω α β :
Type*
hm :
m ≤ mΩ
μ :
f :
Ω → α
g :
Ω → β
hf :
hg :
hCI :
CondIndepFun m hm f g μ
u :
α → ℝ
v :
β → ℝ
hu :
hv :
huf :
Integrable (fun ω => u (f ω)) μ
hvg :
Integrable (fun ω => v (g ω)) μ
huv :
Integrable (fun ω => u (f ω) * v (g ω)) μ
conclusion
μ[fun ω => u (f ω) * v (g ω) | m]
=ᵐ[μ] (μ[fun ω => u (f ω) | m]) * (μ[fun ω => v (g ω) | m])
Proof (Lean source)
theorem condExp_mul_of_condIndep
{Ω α β : Type*}
{m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ)
[MeasurableSpace α] [MeasurableSpace β]
[StandardBorelSpace Ω]
{μ : Measure Ω} [IsFiniteMeasure μ]
{f : Ω → α} {g : Ω → β}
(hf : Measurable f) (hg : Measurable g)
(hCI : CondIndepFun m hm f g μ)
{u : α → ℝ} {v : β → ℝ} (hu : Measurable u) (hv : Measurable v)
(huf : Integrable (fun ω => u (f ω)) μ)
(hvg : Integrable (fun ω => v (g ω)) μ)
(huv : Integrable (fun ω => u (f ω) * v (g ω)) μ) :
μ[fun ω => u (f ω) * v (g ω) | m]
=ᵐ[μ] (μ[fun ω => u (f ω) | m]) * (μ[fun ω => v (g ω) | m]) := by
let mg : MeasurableSpace Ω := m ⊔ MeasurableSpace.comap g inferInstance
have hm_g : mg ≤ mΩ := by
dsimp [mg]
exact sup_le hm hg.comap_le
haveI : IsFiniteMeasure (μ.trim hm_g) :=
MeasureTheory.isFiniteMeasure_trim hm_g
haveI : SigmaFinite (μ.trim hm_g) := inferInstance
have hg_mg : @Measurable Ω β mg _ g := by
exact Measurable.of_comap_le le_sup_right
have hvg_mg :
@StronglyMeasurable Ω ℝ _ mg (fun ω => v (g ω)) := by
exact (hv.comp hg_mg).stronglyMeasurable
have huv' :
Integrable ((fun ω => u (f ω)) * (fun ω => v (g ω))) μ := huv
have htower :
μ[fun ω => u (f ω) * v (g ω) | m]
=ᵐ[μ] μ[μ[fun ω => u (f ω) * v (g ω) | mg] | m] := by
exact (MeasureTheory.condExp_condExp_of_le
(f := fun ω => u (f ω) * v (g ω)) (m₁ := m) (m₂ := mg) (m₀ := mΩ)
le_sup_left hm_g).symm
have hinner :
μ[fun ω => u (f ω) * v (g ω) | mg]
=ᵐ[μ] μ[fun ω => u (f ω) | mg] * (fun ω => v (g ω)) := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_right (m := mg)
(f := fun ω => u (f ω)) (g := fun ω => v (g ω)) hvg_mg huv' huf
have hdrop :
μ[fun ω => u (f ω) | mg] =ᵐ[μ] μ[fun ω => u (f ω) | m] := by
dsimp [mg]
exact condExp_sup_comap_eq_of_condIndep hm hg hf hCI hu huf
have hinner_outer :
μ[μ[fun ω => u (f ω) * v (g ω) | mg] | m]
=ᵐ[μ] μ[μ[fun ω => u (f ω) | mg] * (fun ω => v (g ω)) | m] := by
exact MeasureTheory.condExp_congr_ae hinner
have hdrop_mul :
μ[fun ω => u (f ω) | mg] * (fun ω => v (g ω))
=ᵐ[μ] μ[fun ω => u (f ω) | m] * (fun ω => v (g ω)) := by
exact hdrop.mul (Filter.EventuallyEq.refl (ae μ) (fun ω => v (g ω)))
have hdrop_outer :
μ[μ[fun ω => u (f ω) | mg] * (fun ω => v (g ω)) | m]
=ᵐ[μ] μ[μ[fun ω => u (f ω) | m] * (fun ω => v (g ω)) | m] := by
exact MeasureTheory.condExp_congr_ae hdrop_mul
have hprod_ae :
μ[fun ω => u (f ω) * v (g ω) | mg]
=ᵐ[μ] μ[fun ω => u (f ω) | m] * (fun ω => v (g ω)) :=
hinner.trans hdrop_mul
have hprod_int :
Integrable (μ[fun ω => u (f ω) | m] * (fun ω => v (g ω))) μ := by
exact (MeasureTheory.integrable_condExp (m := mg)
(f := fun ω => u (f ω) * v (g ω)) (μ := μ)).congr hprod_ae
have hce_sm :
@StronglyMeasurable Ω ℝ _ m (μ[fun ω => u (f ω) | m]) := by
exact MeasureTheory.stronglyMeasurable_condExp
have hpull :
μ[μ[fun ω => u (f ω) | m] * (fun ω => v (g ω)) | m]
=ᵐ[μ] μ[fun ω => u (f ω) | m] * μ[fun ω => v (g ω) | m] := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := m)
(f := μ[fun ω => u (f ω) | m]) (g := fun ω => v (g ω))
hce_sm hprod_int hvg
exact htower.trans (hinner_outer.trans (hdrop_outer.trans hpull))
3 supporting declarations (lemmas, instances)
-
setIntegral_condExp_indep_indicatortheorem — Under conditional independence of two variables given a σ-algebra, integrating the conditional expectation of a constant times an event indicator over the intersection of a conditioning event and an event determined by one variable equals integrating that indicator directly.hypothesesΩ α β :Type*hm :m ≤ mΩμ :f :Ω → αg :Ω → βhf :hg :hCI :CondIndepFun m hm g f μS A F :Set ΩhS :hA :MeasurableSet[m] AhF :c :ℝconclusion∫ x in A ∩ F, (μ[S.indicator (fun _ : Ω => c) | m]) x ∂μ= ∫ x in A ∩ F, S.indicator (fun _ : Ω => c) x ∂μProof (Lean source)
theorem setIntegral_condExp_indep_indicator {Ω α β : Type*} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → α} {g : Ω → β} (hf : Measurable f) (hg : Measurable g) (hCI : CondIndepFun m hm g f μ) {S A F : Set Ω} (hS : MeasurableSet[comap g inferInstance] S) (hA : MeasurableSet[m] A) (hF : MeasurableSet[comap f inferInstance] F) (c : ℝ) : ∫ x in A ∩ F, (μ[S.indicator (fun _ : Ω => c) | m]) x ∂μ = ∫ x in A ∩ F, S.indicator (fun _ : Ω => c) x ∂μ := by let oneS : Ω → ℝ := S.indicator (fun _ => (1 : ℝ)) have hsmul_fun : (fun ω => c • oneS ω) = S.indicator (fun _ : Ω => c) := by ext ω by_cases hω : ω ∈ S <;> simp [oneS, hω] have hsmul_ae : (fun ω => c • oneS ω) =ᵐ[μ] S.indicator (fun _ : Ω => c) := by exact MeasureTheory.ae_of_all μ fun ω => congrFun hsmul_fun ω have hce : μ[S.indicator (fun _ : Ω => c) | m] =ᵐ[μ] fun ω => c * (μ⟦S | m⟧) ω := by have h1 : μ[S.indicator (fun _ : Ω => c) | m] =ᵐ[μ] μ[fun ω => c • oneS ω | m] := by exact (MeasureTheory.condExp_congr_ae hsmul_ae).symm have h2 := MeasureTheory.condExp_smul (μ := μ) (c := c) (f := oneS) (m := m) refine h1.trans ?_ filter_upwards [h2] with ω hω exact hω calc ∫ x in A ∩ F, (μ[S.indicator (fun _ : Ω => c) | m]) x ∂μ = ∫ x in A ∩ F, (fun ω => c * (μ⟦S | m⟧) ω) x ∂μ := by refine MeasureTheory.setIntegral_congr_ae ((hm _ hA).inter (hf.comap_le _ hF)) ?_ exact hce.mono fun x hx _ => hx _ = c * ∫ x in A ∩ F, (μ⟦S | m⟧) x ∂μ := by rw [MeasureTheory.integral_const_mul] _ = c * ∫ x in A ∩ F, oneS x ∂μ := by rw [setIntegral_condExp_indep_indicator_one hm hf hg hCI hS hA hF] _ = ∫ x in A ∩ F, (fun ω => c * oneS ω) x ∂μ := by rw [MeasureTheory.integral_const_mul] _ = ∫ x in A ∩ F, S.indicator (fun _ : Ω => c) x ∂μ := by refine MeasureTheory.setIntegral_congr_fun ((hm _ hA).inter (hf.comap_le _ hF)) ?_ intro x _hx simpa [Pi.smul_apply, smul_eq_mul] using congrFun hsmul_fun x -
condExp_sup_comap_eq_of_condIndep_comaptheorem — If g is conditionally independent of f given m, conditioning a σ(g)-measurable integrable real function on m ⊔ σ(f) is the same as conditioning it on m, up to μ-a.e. equality.hypothesesΩ α β :Type*hm :m ≤ mΩμ :f :Ω → αg :Ω → βhf :hg :hCI :CondIndepFun m hm g f μY :Ω → ℝhY_meas :hY_int :Integrable Y μconclusionμ[Y | m ⊔ comap f inferInstance] =ᵐ[μ] μ[Y | m]Proof (Lean source)
theorem condExp_sup_comap_eq_of_condIndep_comap {Ω α β : Type*} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → α} {g : Ω → β} (hf : Measurable f) (hg : Measurable g) (hCI : CondIndepFun m hm g f μ) {Y : Ω → ℝ} (hY_meas : @Measurable Ω ℝ (MeasurableSpace.comap g inferInstance) _ Y) (hY_int : Integrable Y μ) : μ[Y | m ⊔ MeasurableSpace.comap f inferInstance] =ᵐ[μ] μ[Y | m] := by let mf : MeasurableSpace Ω := MeasurableSpace.comap f inferInstance let mg : MeasurableSpace Ω := MeasurableSpace.comap g inferInstance let M : MeasurableSpace Ω := m ⊔ mf have hmM : M ≤ mΩ := by dsimp [M, mf] exact sup_le hm hf.comap_le have hmg : mg ≤ mΩ := by dsimp [mg] exact hg.comap_le haveI : SigmaFinite (μ.trim hm) := by infer_instance haveI : SigmaFinite (μ.trim hmM) := by infer_instance haveI : SigmaFinite (μ.trim hmg) := by infer_instance let T_M : (Ω →₁[μ] ℝ) →L[ℝ] Ω →₁[μ] ℝ := MeasureTheory.condExpL1CLM ℝ hmM μ let T_m : (Ω →₁[μ] ℝ) →L[ℝ] Ω →₁[μ] ℝ := MeasureTheory.condExpL1CLM ℝ hm μ have hL1 : T_M (hY_int.toL1 Y) = T_m (hY_int.toL1 Y) := by have hP_ind : ∀ (c : ℝ) {s : Set Ω} (hs : MeasurableSet[mg] s) (hμs : μ s < ⊤), T_M (@MeasureTheory.Lp.simpleFunc.indicatorConst Ω ℝ mΩ _ (1 : ENNReal) μ s (hmg s hs) hμs.ne c) = T_m (@MeasureTheory.Lp.simpleFunc.indicatorConst Ω ℝ mΩ _ (1 : ENNReal) μ s (hmg s hs) hμs.ne c) := by intro c s hs hμs have hsΩ : @MeasurableSet Ω mΩ s := hmg s hs have hs_int : Integrable (s.indicator (fun _ : Ω => c)) μ := by refine (MeasureTheory.integrable_indicator_iff (μ := μ) hsΩ).2 ?_ exact MeasureTheory.integrableOn_const have hind_eq : @MeasureTheory.Lp.simpleFunc.indicatorConst Ω ℝ mΩ _ (1 : ENNReal) μ s (hmg s hs) hμs.ne c = hs_int.toL1 (s.indicator (fun _ : Ω => c)) := by apply MeasureTheory.Lp.ext refine (@MeasureTheory.indicatorConstLp_coeFn Ω ℝ mΩ (1 : ENNReal) μ _ s (hmg s hs) hμs.ne c).trans ?_ exact hs_int.coeFn_toL1.symm rw [hind_eq] apply MeasureTheory.Lp.ext have hM := MeasureTheory.condExp_ae_eq_condExpL1CLM hmM hs_int have hm' := MeasureTheory.condExp_ae_eq_condExpL1CLM hm hs_int have hdrop : μ[s.indicator (fun _ : Ω => c) | M] =ᵐ[μ] μ[s.indicator (fun _ : Ω => c) | m] := by dsimp [M, mf] exact condExp_indicator_sup_comap_eq_of_condIndep hm hf hg hCI hs c exact hM.symm.trans (hdrop.trans hm') have hP_add : ∀ ⦃u v : Ω → ℝ⦄, ∀ hu : MemLp u 1 μ, ∀ hv : MemLp v 1 μ, @StronglyMeasurable Ω ℝ _ mg u → @StronglyMeasurable Ω ℝ _ mg v → Disjoint (support u) (support v) → T_M (hu.toLp u) = T_m (hu.toLp u) → T_M (hv.toLp v) = T_m (hv.toLp v) → T_M (hu.toLp u + hv.toLp v) = T_m (hu.toLp u + hv.toLp v) := by intro u v hu hv _hu_meas _hv_meas _hdisj hu_eq hv_eq simp [T_M, T_m, map_add, hu_eq, hv_eq] have hP_closed : IsClosed {u : @MeasureTheory.lpMeas Ω ℝ ℝ _ _ _ mg mΩ (1 : ENNReal) μ | T_M (u : @Lp Ω ℝ mΩ _ (1 : ENNReal) μ) = T_m (u : @Lp Ω ℝ mΩ _ (1 : ENNReal) μ)} := by exact isClosed_eq (T_M.continuous.comp continuous_subtype_val) (T_m.continuous.comp continuous_subtype_val) exact MeasureTheory.Lp.induction_stronglyMeasurable hmg (by norm_num) (fun u : Ω →₁[μ] ℝ => T_M u = T_m u) hP_ind hP_add hP_closed (hY_int.toL1 Y) (hY_meas.stronglyMeasurable.aestronglyMeasurable.congr hY_int.coeFn_toL1.symm) have hM := MeasureTheory.condExp_ae_eq_condExpL1CLM hmM hY_int have hm' := MeasureTheory.condExp_ae_eq_condExpL1CLM hm hY_int have hL1_ae : (T_M (hY_int.toL1 Y) : Ω → ℝ) =ᵐ[μ] (T_m (hY_int.toL1 Y) : Ω → ℝ) := by rw [hL1] exact hM.trans (hL1_ae.trans hm'.symm) -
condExp_sup_comap_eq_of_condIndeptheorem — If a conditioning σ-algebra is coarser than the ambient one, random elements f and g are measurable, g is conditionally independent of f given that σ-algebra, and a real-valued transform h is measurable with h(g) integrable, then adding the information generated by f does not change the conditional expectation of h(g), almost everywhere.hypothesesΩ α β :Type*hm :m ≤ mΩμ :f :Ω → αg :Ω → βhf :hg :hCI :CondIndepFun m hm g f μh :β → ℝhh :hhg :Integrable (fun ω => h (g ω)) μconclusionμ[fun ω => h (g ω) | m ⊔ comap f inferInstance]=ᵐ[μ] μ[fun ω => h (g ω) | m]Proof (Lean source)
theorem condExp_sup_comap_eq_of_condIndep {Ω α β : Type*} {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) [MeasurableSpace α] [MeasurableSpace β] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {f : Ω → α} {g : Ω → β} (hf : Measurable f) (hg : Measurable g) (hCI : CondIndepFun m hm g f μ) {h : β → ℝ} (hh : Measurable h) (hhg : Integrable (fun ω => h (g ω)) μ) : μ[fun ω => h (g ω) | m ⊔ comap f inferInstance] =ᵐ[μ] μ[fun ω => h (g ω) | m] := by have hg_comap : @Measurable Ω β (comap g inferInstance) _ g := by exact Measurable.of_comap_le le_rfl have hY_meas : @Measurable Ω ℝ (comap g inferInstance) _ (fun ω => h (g ω)) := by exact hh.comp hg_comap exact condExp_sup_comap_eq_of_condIndep_comap hm hf hg hCI hY_meas hhg
CondExp_Part2 3 core · 1 supporting This file proves conditional-expectation identities implied by conditional independence, including drop-of-conditioning, product factorization, weak union, and contraction. ★ condIndepFun_weak_union_of_prodMk★ condIndepFun_contraction_of_prodMk★ condIndep_valuesProjection_contraction
Conditional Expectations Under Conditional Independence
This file proves conditional-expectation identities implied by conditional independence, including drop-of-conditioning, product factorization, weak union, and contraction. These measure-theoretic facts give a reusable algebra for conditional independence under enlarged conditioning σ-algebras and paired coordinates.
The central exported lemmas are condExp_sup_comap_eq_of_condIndep_comap and
condExp_sup_comap_eq_of_condIndep for removing irrelevant conditioning
variables, condExp_mul_of_condIndep for factoring a product's conditional
expectation, condIndepFun_weak_union_of_prodMk for weak union,
condIndepFun_prodMk_of_measurable_left for adjoining an m-measurable
coordinate, and condIndepFun_contraction_of_prodMk for semigraphoid
contraction.
theorem condIndepFun_weak_union_of_prodMk reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Weak union for conditional independence. For a sub-σ-algebra m coarser than the ambient σ-algebra and measurable maps W, V, and A, if W is conditionally independent of the pair (V, A) given m, then W is conditionally independent of V given the enlarged σ-algebra m joined with the σ-algebra generated by A.
Formal statement
hypotheses
Ω α β γ :
hm :
m ≤ mΩ
μ :
W :
Ω → α
V :
Ω → β
A :
Ω → γ
hW :
hV :
hA :
hCI :
CondIndepFun m hm W (fun ω => (V ω, A ω)) μ
conclusion
Proof (Lean source)
theorem condIndepFun_weak_union_of_prodMk
{Ω α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
{m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ)
[StandardBorelSpace Ω]
{μ : Measure Ω} [IsFiniteMeasure μ]
{W : Ω → α} {V : Ω → β} {A : Ω → γ}
(hW : Measurable W) (hV : Measurable V) (hA : Measurable A)
(hCI : CondIndepFun m hm W (fun ω => (V ω, A ω)) μ) :
CondIndepFun (m ⊔ MeasurableSpace.comap A inferInstance)
(sup_le hm hA.comap_le) W V μ := by
let mA : MeasurableSpace Ω := m ⊔ MeasurableSpace.comap A inferInstance
let pair : Ω → β × γ := fun ω => (V ω, A ω)
let mVA : MeasurableSpace Ω := m ⊔ MeasurableSpace.comap pair inferInstance
have hpair : @Measurable Ω (β × γ) mΩ _ pair := hV.prod hA
have hmVA : mVA ≤ mΩ := by
dsimp [mVA]
exact sup_le hm hpair.comap_le
have hpair_mVA : @Measurable Ω (β × γ) mVA _ pair := by
exact Measurable.of_comap_le le_sup_right
have hV_mVA : @Measurable Ω β mVA _ V := by
exact measurable_fst.comp hpair_mVA
have hA_pair :
@Measurable Ω γ (MeasurableSpace.comap pair inferInstance) _ A := by
exact measurable_snd.comp (Measurable.of_comap_le le_rfl)
have hmA_le_mVA : mA ≤ mVA := by
dsimp [mA, mVA]
exact sup_le le_sup_left (le_trans hA_pair.comap_le le_sup_right)
have hCI_A : CondIndepFun m hm W A μ := by
simpa [Function.comp_def] using
(hCI.comp measurable_id measurable_snd)
rw [ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul hW hV]
intro s t hs ht
let S : Set Ω := W ⁻¹' s
let T : Set Ω := V ⁻¹' t
let oneS : Ω → ℝ := S.indicator (fun _ => (1 : ℝ))
let oneT : Ω → ℝ := T.indicator (fun _ => (1 : ℝ))
have hS_meas : @MeasurableSet Ω mΩ S := hW hs
have hT_meas : @MeasurableSet Ω mΩ T := hV ht
have hS_int : Integrable oneS μ := by
refine (MeasureTheory.integrable_indicator_iff hS_meas).2 ?_
exact MeasureTheory.integrableOn_const
have hT_int : Integrable oneT μ := by
refine (MeasureTheory.integrable_indicator_iff hT_meas).2 ?_
exact MeasureTheory.integrableOn_const
have hST_int : Integrable (oneS * oneT) μ := by
have hST_set_int :
Integrable ((S ∩ T).indicator (fun _ : Ω => (1 : ℝ))) μ := by
refine (MeasureTheory.integrable_indicator_iff (hS_meas.inter hT_meas)).2 ?_
exact MeasureTheory.integrableOn_const
exact hST_set_int.congr (MeasureTheory.ae_of_all μ fun ω => by
by_cases hωS : ω ∈ S <;> by_cases hωT : ω ∈ T <;> simp [oneS, oneT, hωS, hωT])
have hT_mVA :
@StronglyMeasurable Ω ℝ _ mVA oneT := by
exact MeasureTheory.stronglyMeasurable_const.indicator (hV_mVA ht)
have hdrop_mVA :
μ[oneS | mVA] =ᵐ[μ] μ[oneS | m] := by
have hs_ind_meas :
Measurable (s.indicator (fun _ : α => (1 : ℝ))) := by fun_prop
have hone : oneS = fun ω => s.indicator (fun _ : α => (1 : ℝ)) (W ω) := by
funext ω
by_cases hω : W ω ∈ s <;> simp [oneS, S, hω]
rw [hone]
simpa [mVA, pair] using
(condExp_sup_comap_eq_of_condIndep hm hpair hW hCI
(h := s.indicator (fun _ : α => (1 : ℝ))) hs_ind_meas hS_int)
have hdrop_mA :
μ[oneS | mA] =ᵐ[μ] μ[oneS | m] := by
have hs_ind_meas :
Measurable (s.indicator (fun _ : α => (1 : ℝ))) := by fun_prop
have hone : oneS = fun ω => s.indicator (fun _ : α => (1 : ℝ)) (W ω) := by
funext ω
by_cases hω : W ω ∈ s <;> simp [oneS, S, hω]
rw [hone]
simpa [mA] using
(condExp_sup_comap_eq_of_condIndep hm hA hW hCI_A
(h := s.indicator (fun _ : α => (1 : ℝ))) hs_ind_meas hS_int)
have htower :
μ[oneS * oneT | mA] =ᵐ[μ] μ[μ[oneS * oneT | mVA] | mA] := by
exact (MeasureTheory.condExp_condExp_of_le
(f := oneS * oneT) (m₁ := mA) (m₂ := mVA) (m₀ := mΩ)
hmA_le_mVA hmVA).symm
have hinner :
μ[oneS * oneT | mVA] =ᵐ[μ] μ[oneS | mVA] * oneT := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_right (m := mVA)
(f := oneS) (g := oneT) hT_mVA hST_int hS_int
have hinner_drop :
μ[oneS * oneT | mVA] =ᵐ[μ] μ[oneS | m] * oneT :=
hinner.trans (hdrop_mVA.mul (Filter.EventuallyEq.rfl))
have hinner_outer :
μ[μ[oneS * oneT | mVA] | mA]
=ᵐ[μ] μ[μ[oneS | m] * oneT | mA] :=
MeasureTheory.condExp_congr_ae hinner_drop
have hprod_int :
Integrable (μ[oneS | m] * oneT) μ := by
exact (MeasureTheory.integrable_condExp (m := mVA)
(f := oneS * oneT) (μ := μ)).congr hinner_drop
have hceS_mA :
@StronglyMeasurable Ω ℝ _ mA (μ[oneS | m]) := by
exact MeasureTheory.stronglyMeasurable_condExp.mono le_sup_left
have hpull :
μ[μ[oneS | m] * oneT | mA]
=ᵐ[μ] μ[oneS | m] * μ[oneT | mA] := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := mA)
(f := μ[oneS | m]) (g := oneT) hceS_mA hprod_int hT_int
have hsets :
μ⟦W ⁻¹' s ∩ V ⁻¹' t | mA⟧
=ᵐ[μ] μ[oneS * oneT | mA] := by
rw [show W ⁻¹' s ∩ V ⁻¹' t = S ∩ T by rfl]
rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
rfl
calc
μ⟦W ⁻¹' s ∩ V ⁻¹' t | mA⟧
=ᵐ[μ] μ[oneS * oneT | mA] := hsets
_ =ᵐ[μ] μ[μ[oneS * oneT | mVA] | mA] := htower
_ =ᵐ[μ] μ[μ[oneS | m] * oneT | mA] := hinner_outer
_ =ᵐ[μ] μ[oneS | m] * μ[oneT | mA] := hpull
_ =ᵐ[μ] μ[oneS | mA] * μ[oneT | mA] := by
exact hdrop_mA.symm.mul (Filter.EventuallyEq.rfl)
_ =ᵐ[μ] μ⟦W ⁻¹' s | mA⟧ * μ⟦V ⁻¹' t | mA⟧ := by
rfl
theorem condIndepFun_contraction_of_prodMk reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Contraction for conditional independence via a product right side. For a sub-σ-algebra m coarser than the ambient σ-algebra and measurable maps X, Y, and W, if X is conditionally independent of Y given the enlarged σ-algebra m joined with the σ-algebra generated by W and X is conditionally independent of W given m, then X is conditionally independent of the pair (Y, W) given m.
Formal statement
hypotheses
Ω α β γ :
hm :
m ≤ mΩ
μ :
X :
Ω → α
Y :
Ω → β
W :
Ω → γ
hX :
hY :
hW :
h1 :
h2 :
CondIndepFun m hm X W μ
conclusion
CondIndepFun m hm X (fun ω => (Y ω, W ω)) μ
Proof (Lean source)
theorem condIndepFun_contraction_of_prodMk
{Ω α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ]
{m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ)
[StandardBorelSpace Ω]
{μ : Measure Ω} [IsFiniteMeasure μ]
{X : Ω → α} {Y : Ω → β} {W : Ω → γ}
(hX : Measurable X) (hY : Measurable Y) (hW : Measurable W)
(h1 : CondIndepFun
(m ⊔ MeasurableSpace.comap W inferInstance)
(sup_le hm hW.comap_le) X Y μ)
(h2 : CondIndepFun m hm X W μ) :
CondIndepFun m hm X (fun ω => (Y ω, W ω)) μ := by
let pair : Ω → β × γ := fun ω => (Y ω, W ω)
let xsets : Set (Set Ω) := {q | ∃ s : Set α, MeasurableSet s ∧ X ⁻¹' s = q}
let pairsets : Set (Set Ω) :=
{q | ∃ t : Set β, MeasurableSet t ∧
∃ u : Set γ, MeasurableSet u ∧ pair ⁻¹' (t ×ˢ u) = q}
have hpair_meas : Measurable pair := by fun_prop
have hpX_pi : IsPiSystem xsets := by
simpa [xsets] using (MeasurableSpace.isPiSystem_measurableSet (α := α)).comap X
have hpPair_pi : IsPiSystem pairsets := by
simpa [pairsets] using (isPiSystem_prod (α := β) (β := γ)).comap pair
have hpX_meas : ∀ s ∈ xsets, MeasurableSet s := by
rintro _ ⟨s, hs, rfl⟩
exact hX hs
have hpPair_meas : ∀ s ∈ pairsets, MeasurableSet s := by
rintro _ ⟨t, ht, u, hu, rfl⟩
exact hpair_meas (ht.prod hu)
have hrect : ProbabilityTheory.CondIndepSets m hm xsets pairsets μ := by
rw [ProbabilityTheory.condIndepSets_iff m hm xsets pairsets hpX_meas hpPair_meas μ]
intro t1 t2 ht1 ht2
rcases ht1 with ⟨s, hs_meas, rfl⟩
rcases ht2 with ⟨t, ht_meas, u, hu_meas, rfl⟩
let A : Set Ω := X ⁻¹' s
let B : Set Ω := Y ⁻¹' t
let C : Set Ω := W ⁻¹' u
let oneA : Ω → ℝ := A.indicator (fun _ => (1 : ℝ))
let oneB : Ω → ℝ := B.indicator (fun _ => (1 : ℝ))
let oneC : Ω → ℝ := C.indicator (fun _ => (1 : ℝ))
let mW : MeasurableSpace Ω := m ⊔ MeasurableSpace.comap W inferInstance
have hA_meas : @MeasurableSet Ω mΩ A := hX hs_meas
have hB_meas : @MeasurableSet Ω mΩ B := hY ht_meas
have hC_meas : @MeasurableSet Ω mΩ C := hW hu_meas
have hmW : mW ≤ mΩ := by
dsimp [mW]
exact sup_le hm hW.comap_le
have hm_le_mW : m ≤ mW := by
dsimp [mW]
exact le_sup_left
have hC_mW : @MeasurableSet Ω mW C := by
dsimp [mW, C]
exact Measurable.of_comap_le le_sup_right hu_meas
have hC_sm : @StronglyMeasurable Ω ℝ _ mW oneC :=
MeasureTheory.stronglyMeasurable_const.indicator hC_mW
have hceA_m : @StronglyMeasurable Ω ℝ _ m (μ[oneA | m]) :=
MeasureTheory.stronglyMeasurable_condExp
have hceA_m_mW : @StronglyMeasurable Ω ℝ _ mW (μ[oneA | m]) :=
hceA_m.mono hm_le_mW
have hA_int : Integrable oneA μ := by
refine (MeasureTheory.integrable_indicator_iff hA_meas).2 ?_
exact MeasureTheory.integrableOn_const
have hB_int : Integrable oneB μ := by
refine (MeasureTheory.integrable_indicator_iff hB_meas).2 ?_
exact MeasureTheory.integrableOn_const
have hC_int : Integrable oneC μ := by
refine (MeasureTheory.integrable_indicator_iff hC_meas).2 ?_
exact MeasureTheory.integrableOn_const
have hAB_int : Integrable (oneA * oneB) μ := by
refine ((MeasureTheory.integrable_indicator_iff (hA_meas.inter hB_meas)).2
(MeasureTheory.integrableOn_const (μ := μ) (s := A ∩ B) (C := (1 : ℝ)))).congr ?_
exact MeasureTheory.ae_of_all μ fun ω => by
by_cases hωA : ω ∈ A <;> by_cases hωB : ω ∈ B <;> simp [oneA, oneB, hωA, hωB]
have hBC_int : Integrable (oneB * oneC) μ := by
refine ((MeasureTheory.integrable_indicator_iff (hB_meas.inter hC_meas)).2
(MeasureTheory.integrableOn_const (μ := μ) (s := B ∩ C) (C := (1 : ℝ)))).congr ?_
exact MeasureTheory.ae_of_all μ fun ω => by
by_cases hωB : ω ∈ B <;> by_cases hωC : ω ∈ C <;> simp [oneB, oneC, hωB, hωC]
have hABC_int : Integrable ((oneA * oneB) * oneC) μ := by
refine ((MeasureTheory.integrable_indicator_iff ((hA_meas.inter hB_meas).inter hC_meas)).2
(MeasureTheory.integrableOn_const (μ := μ) (s := (A ∩ B) ∩ C) (C := (1 : ℝ)))).congr ?_
exact MeasureTheory.ae_of_all μ fun ω => by
by_cases hωA : ω ∈ A <;> by_cases hωB : ω ∈ B <;> by_cases hωC : ω ∈ C <;>
simp [oneA, oneB, oneC, hωA, hωB, hωC]
have hCI1 :=
(ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul hX hY).mp
h1 s t hs_meas ht_meas
have hCI2 :=
(ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul hX hW).mp
h2 s u hs_meas hu_meas
have hdropA :
μ[oneA | mW] =ᵐ[μ] μ[oneA | m] := by
have hs_ind_meas : Measurable (s.indicator (fun _ : α => (1 : ℝ))) := by fun_prop
have hone : oneA = fun ω => s.indicator (fun _ : α => (1 : ℝ)) (X ω) := by
funext ω
by_cases hω : X ω ∈ s <;> simp [oneA, A, hω]
rw [hone]
simpa [mW] using
(condExp_sup_comap_eq_of_condIndep hm hW hX h2
(h := s.indicator (fun _ : α => (1 : ℝ))) hs_ind_meas hA_int)
have hpullC_AB :
μ[(oneA * oneB) * oneC | mW] =ᵐ[μ] μ[oneA * oneB | mW] * oneC := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_right (m := mW)
(f := oneA * oneB) (g := oneC) hC_sm hABC_int hAB_int
have hpullC_B :
μ[oneB * oneC | mW] =ᵐ[μ] μ[oneB | mW] * oneC := by
exact MeasureTheory.condExp_mul_of_stronglyMeasurable_right (m := mW)
(f := oneB) (g := oneC) hC_sm hBC_int hB_int
have hAB_mW :
μ[oneA * oneB | mW] =ᵐ[μ] μ[oneA | mW] * μ[oneB | mW] := by
have hsets :
μ⟦X ⁻¹' s ∩ Y ⁻¹' t | mW⟧ =ᵐ[μ] μ[oneA * oneB | mW] := by
rw [show X ⁻¹' s ∩ Y ⁻¹' t = A ∩ B by rfl]
rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
rfl
exact hsets.symm.trans hCI1
have hAB_mW_drop :
μ[oneA * oneB | mW] =ᵐ[μ] μ[oneA | m] * μ[oneB | mW] :=
hAB_mW.trans (hdropA.mul (Filter.EventuallyEq.rfl))
have hABC_tower :
μ[(oneA * oneB) * oneC | m] =ᵐ[μ]
μ[μ[(oneA * oneB) * oneC | mW] | m] := by
exact (MeasureTheory.condExp_condExp_of_le
(f := (oneA * oneB) * oneC) (m₁ := m) (m₂ := mW) (m₀ := mΩ)
hm_le_mW hmW).symm
have hinner_ABC :
μ[μ[(oneA * oneB) * oneC | mW] | m] =ᵐ[μ]
μ[(μ[oneA | m] * μ[oneB | mW]) * oneC | m] := by
exact MeasureTheory.condExp_congr_ae (hpullC_AB.trans
(hAB_mW_drop.mul (Filter.EventuallyEq.rfl)))
have hpullA :
μ[(μ[oneA | m] * μ[oneB | mW]) * oneC | m] =ᵐ[μ]
μ[oneA | m] * μ[μ[oneB | mW] * oneC | m] := by
have hint :
Integrable ((μ[oneA | m] * μ[oneB | mW]) * oneC) μ := by
exact (MeasureTheory.integrable_condExp (m := mW)
(f := (oneA * oneB) * oneC) (μ := μ)).congr
(hpullC_AB.trans (hAB_mW_drop.mul (Filter.EventuallyEq.rfl)))
have hint_assoc :
Integrable (μ[oneA | m] * (μ[oneB | mW] * oneC)) μ :=
hint.congr (MeasureTheory.ae_of_all μ fun ω => by ring_nf)
have hB_mW_C_int :
Integrable (μ[oneB | mW] * oneC) μ :=
(MeasureTheory.integrable_condExp (m := mW) (f := oneB * oneC) (μ := μ)).congr
hpullC_B
calc
μ[(μ[oneA | m] * μ[oneB | mW]) * oneC | m]
=ᵐ[μ] μ[μ[oneA | m] * (μ[oneB | mW] * oneC) | m] := by
refine MeasureTheory.condExp_congr_ae ?_
exact MeasureTheory.ae_of_all μ fun ω => by ring_nf
_ =ᵐ[μ] μ[oneA | m] * μ[μ[oneB | mW] * oneC | m] :=
MeasureTheory.condExp_mul_of_stronglyMeasurable_left (m := m)
(f := μ[oneA | m]) (g := μ[oneB | mW] * oneC) hceA_m hint_assoc
hB_mW_C_int
have hBC_tower :
μ[oneB * oneC | m] =ᵐ[μ] μ[μ[oneB * oneC | mW] | m] := by
exact (MeasureTheory.condExp_condExp_of_le
(f := oneB * oneC) (m₁ := m) (m₂ := mW) (m₀ := mΩ)
hm_le_mW hmW).symm
have hBC_inner :
μ[μ[oneB * oneC | mW] | m] =ᵐ[μ] μ[μ[oneB | mW] * oneC | m] :=
MeasureTheory.condExp_congr_ae hpullC_B
have hleft_sets :
μ⟦X ⁻¹' s ∩ pair ⁻¹' (t ×ˢ u) | m⟧
=ᵐ[μ] μ[(oneA * oneB) * oneC | m] := by
rw [show X ⁻¹' s ∩ pair ⁻¹' (t ×ˢ u) = (A ∩ B) ∩ C by
ext ω
simp [A, B, C, pair, and_assoc]]
rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
refine MeasureTheory.condExp_congr_ae ?_
exact MeasureTheory.ae_of_all μ fun ω => by
by_cases hωA : ω ∈ A <;> by_cases hωB : ω ∈ B <;> by_cases hωC : ω ∈ C <;>
simp [oneA, oneB, oneC, hωA, hωB, hωC]
have hpair_sets :
μ⟦pair ⁻¹' (t ×ˢ u) | m⟧ =ᵐ[μ] μ[oneB * oneC | m] := by
rw [show pair ⁻¹' (t ×ˢ u) = B ∩ C by
ext ω
simp [B, C, pair]]
rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one]
rfl
calc
μ⟦X ⁻¹' s ∩ pair ⁻¹' (t ×ˢ u) | m⟧
=ᵐ[μ] μ[(oneA * oneB) * oneC | m] := hleft_sets
_ =ᵐ[μ] μ[μ[(oneA * oneB) * oneC | mW] | m] := hABC_tower
_ =ᵐ[μ] μ[(μ[oneA | m] * μ[oneB | mW]) * oneC | m] := hinner_ABC
_ =ᵐ[μ] μ[oneA | m] * μ[μ[oneB | mW] * oneC | m] := hpullA
_ =ᵐ[μ] μ[oneA | m] * μ[μ[oneB * oneC | mW] | m] := by
exact (Filter.EventuallyEq.rfl).mul (MeasureTheory.condExp_congr_ae hpullC_B.symm)
_ =ᵐ[μ] μ[oneA | m] * μ[oneB * oneC | m] := by
exact (Filter.EventuallyEq.rfl).mul hBC_tower.symm
_ =ᵐ[μ] μ⟦X ⁻¹' s | m⟧ * μ⟦pair ⁻¹' (t ×ˢ u) | m⟧ := by
exact (Filter.EventuallyEq.rfl).mul hpair_sets.symm
rw [ProbabilityTheory.condIndepFun_iff_condIndep]
have hpX_eq : xsets = (fun r : Set α => X ⁻¹' r) '' {s : Set α | MeasurableSet s} := by
ext q
constructor
· rintro ⟨s, hs, hq⟩
exact ⟨s, hs, hq⟩
· rintro ⟨s, hs, hq⟩
exact ⟨s, hs, hq⟩
have hpPair_eq :
pairsets = (fun r : Set (β × γ) => pair ⁻¹' r) ''
Set.image2 (· ×ˢ ·) {t : Set β | MeasurableSet t} {u : Set γ | MeasurableSet u} := by
ext q
constructor
· rintro ⟨t, ht, u, hu, hq⟩
exact ⟨t ×ˢ u, ⟨t, ht, u, hu, rfl⟩, hq⟩
· rintro ⟨r, ⟨t, ht, u, hu, rfl⟩, hq⟩
exact ⟨t, ht, u, hu, hq⟩
have hgenX : (inferInstance : MeasurableSpace α).comap X =
MeasurableSpace.generateFrom xsets := by
rw [show (inferInstance : MeasurableSpace α) =
MeasurableSpace.generateFrom {s : Set α | MeasurableSet s} by
exact (MeasurableSpace.generateFrom_measurableSet (α := α)).symm]
rw [MeasurableSpace.comap_generateFrom]
rfl
have hgenPair : (inferInstance : MeasurableSpace (β × γ)).comap pair =
MeasurableSpace.generateFrom pairsets := by
rw [hpPair_eq, ← generateFrom_prod, MeasurableSpace.comap_generateFrom]
rw [hgenX, hgenPair]
exact ProbabilityTheory.CondIndepSets.condIndep' hpX_meas hpPair_meas hpX_pi hpPair_pi hrect
theorem condIndep_valuesProjection_contraction reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
For coordinate sets X, Y, W, Z, and I, a decidable index type, measurable value spaces, inclusions of the four blocks in I, a finite measure μ, the first conditional independence, and the second one, contraction holds for the coordinate projections.
Formal statement
hypotheses
M :
∀ n, MeasurableSpace (Ω n)
StandardBorelSpace (ValuesOn I Ω)
hX :
X ⊆ I
hY :
Y ⊆ I
hW :
W ⊆ I
hZ :
Z ⊆ I
μ :
h1 :
CondIndepFun (comap (valuesProjection (Ω := Ω) (union_subset hZ hW)) inferInstance) (comap_valuesProjection_le (Ω' := Ω) (union_subset hZ hW)) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hY) μ
h2 :
CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) hW) μ
conclusion
CondIndepFun (comap (valuesProjection (Ω := Ω) hZ) inferInstance) (comap_valuesProjection_le (Ω' := Ω) hZ) (valuesProjection (Ω := Ω) hX) (valuesProjection (Ω := Ω) (union_subset hY hW)) μ
Proof (Lean source)
theorem condIndep_valuesProjection_contraction
{M : Type*} [DecidableEq M]
{I X Y W Z : Finset M}
{Ω : M → Type*} [∀ n, MeasurableSpace (Ω n)]
[StandardBorelSpace (ValuesOn I Ω)]
(hX : X ⊆ I) (hY : Y ⊆ I) (hW : W ⊆ I)
(hZ : Z ⊆ I)
{μ : Measure (ValuesOn I Ω)} [IsFiniteMeasure μ]
(h1 :
CondIndepFun
(comap
(valuesProjection (Ω := Ω) (Finset.union_subset hZ hW)) inferInstance)
(comap_valuesProjection_le (Ω' := Ω) (Finset.union_subset hZ hW))
(valuesProjection (Ω := Ω) hX)
(valuesProjection (Ω := Ω) hY)
μ)
(h2 :
CondIndepFun
(comap (valuesProjection (Ω := Ω) hZ) inferInstance)
(comap_valuesProjection_le (Ω' := Ω) hZ)
(valuesProjection (Ω := Ω) hX)
(valuesProjection (Ω := Ω) hW)
μ) :
CondIndepFun
(comap (valuesProjection (Ω := Ω) hZ) inferInstance)
(comap_valuesProjection_le (Ω' := Ω) hZ)
(valuesProjection (Ω := Ω) hX)
(valuesProjection (Ω := Ω) (Finset.union_subset hY hW))
μ := by
let hYW : (Y ∪ W) ⊆ I := Finset.union_subset hY hW
let hZW : (Z ∪ W) ⊆ I := Finset.union_subset hZ hW
have hσ :
comap (valuesProjection (Ω := Ω) hZW) inferInstance =
comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔
comap (valuesProjection (Ω := Ω) hW) inferInstance :=
comap_valuesProjection_union_eq_sup (Ω' := Ω) hZ hW
have h1' :
CondIndepFun
(comap (valuesProjection (Ω := Ω) hZ) inferInstance ⊔
comap (valuesProjection (Ω := Ω) hW) inferInstance)
(sup_le (comap_valuesProjection_le (Ω' := Ω) hZ)
(comap_valuesProjection_le (Ω' := Ω) hW))
(valuesProjection (Ω := Ω) hX)
(valuesProjection (Ω := Ω) hY)
μ := by
simpa [hσ] using h1
have hpair :
CondIndepFun
(comap (valuesProjection (Ω := Ω) hZ) inferInstance)
(comap_valuesProjection_le (Ω' := Ω) hZ)
(valuesProjection (Ω := Ω) hX)
(fun ξ : ValuesOn I Ω =>
(valuesProjection (Ω := Ω) hY ξ, valuesProjection (Ω := Ω) hW ξ))
μ :=
condIndepFun_contraction_of_prodMk
(m := comap (valuesProjection (Ω := Ω) hZ) inferInstance)
(mΩ := inferInstance)
(μ := μ)
(comap_valuesProjection_le (Ω' := Ω) hZ)
(measurable_valuesProjection (Ω' := Ω) hX)
(measurable_valuesProjection (Ω' := Ω) hY)
(measurable_valuesProjection (Ω' := Ω) hW)
h1' h2
have hassembled :
CondIndepFun
(comap (valuesProjection (Ω := Ω) hZ) inferInstance)
(comap_valuesProjection_le (Ω' := Ω) hZ)
(valuesProjection (Ω := Ω) hX)
(fun ξ : ValuesOn I Ω =>
valuesUnionMk (Ω := Ω) (valuesProjection (Ω := Ω) hY ξ)
(valuesProjection (Ω := Ω) hW ξ))
μ :=
hpair.comp measurable_id (measurable_valuesUnionMk (Ω := Ω))
simpa [Function.comp_def, valuesUnionMk_projection_comp (Ω' := Ω) hY hW]
using hassembled
1 supporting declaration (lemmas, instances)
-
condIndepFun_prodMk_of_measurable_lefttheorem — Extension of CondIndepFun by an m-measurable function.hypothesesΩ α β γ :hm :m ≤ mΩμ :W :Ω → αX :Ω → βZ :Ω → γ_hW :_hZ :_hX_m :Measurable[m] X_hCI :CondIndepFun m hm W Z μconclusionCondIndepFun m hm (fun ω => (W ω, X ω)) Z μProof (Lean source)
theorem condIndepFun_prodMk_of_measurable_left {Ω α β γ : Type*} [MeasurableSpace α] [MeasurableSpace β] [MeasurableSpace γ] {m mΩ : MeasurableSpace Ω} (hm : m ≤ mΩ) [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {W : Ω → α} {X : Ω → β} {Z : Ω → γ} (_hW : Measurable W) (_hZ : Measurable Z) (_hX_m : Measurable[m] X) (_hCI : CondIndepFun m hm W Z μ) : CondIndepFun m hm (fun ω => (W ω, X ω)) Z μ := by let pair : Ω → α × β := fun ω => (W ω, X ω) let rects : Set (Set (α × β)) := Set.image2 (· ×ˢ ·) {s : Set α | MeasurableSet s} {t : Set β | MeasurableSet t} let zsets : Set (Set γ) := {t : Set γ | MeasurableSet t} let pPair : Set (Set Ω) := {q | ∃ s : Set α, MeasurableSet s ∧ ∃ u : Set β, MeasurableSet u ∧ pair ⁻¹' (s ×ˢ u) = q} let pZ : Set (Set Ω) := {q | ∃ r : Set γ, r ∈ zsets ∧ Z ⁻¹' r = q} have hpair_meas : Measurable pair := _hW.prod (_hX_m.mono hm le_rfl) have hpPair_pi : IsPiSystem pPair := by simpa [pPair] using (isPiSystem_prod (α := α) (β := β)).comap pair have hpZ_pi : IsPiSystem pZ := by simpa [pZ, zsets] using (MeasurableSpace.isPiSystem_measurableSet (α := γ)).comap Z have hpPair_meas : ∀ s ∈ pPair, MeasurableSet s := by rintro _ ⟨s, hs, u, hu, rfl⟩ exact hpair_meas (hs.prod hu) have hpZ_meas : ∀ s ∈ pZ, MeasurableSet s := by rintro _ ⟨r, hr, rfl⟩ exact _hZ (by simpa [zsets] using hr) have hrect : ProbabilityTheory.CondIndepSets m hm pPair pZ μ := by rw [ProbabilityTheory.condIndepSets_iff m hm pPair pZ hpPair_meas hpZ_meas μ] intro t1 t2 ht1 ht2 rcases ht1 with ⟨s, hs_meas, u, hu_meas, rfl⟩ rcases ht2 with ⟨v, hv, rfl⟩ have hv_meas : MeasurableSet v := by simpa [zsets] using hv let A : Set Ω := W ⁻¹' s let B : Set Ω := X ⁻¹' u let C : Set Ω := Z ⁻¹' v have hB_m : MeasurableSet[m] B := _hX_m hu_meas have hB_sm : StronglyMeasurable[m] (B.indicator (fun _ : Ω => (1 : ℝ))) := MeasureTheory.stronglyMeasurable_const.indicator hB_m have hB_bound : ∀ᵐ ω ∂μ, ‖B.indicator (fun _ : Ω => (1 : ℝ)) ω‖ ≤ (1 : ℝ) := by exact MeasureTheory.ae_of_all μ fun ω => by rw [indicator] split_ifs <;> simp have hAC_int : Integrable ((A ∩ C).indicator (fun _ : Ω => (1 : ℝ))) μ := by refine (MeasureTheory.integrable_indicator_iff ?_).2 MeasureTheory.integrableOn_const exact (_hW hs_meas).inter (_hZ hv_meas) have hA_int : Integrable (A.indicator (fun _ : Ω => (1 : ℝ))) μ := by refine (MeasureTheory.integrable_indicator_iff ?_).2 MeasureTheory.integrableOn_const exact _hW hs_meas have hpull_AC : μ[B.indicator (fun _ : Ω => (1 : ℝ)) * (A ∩ C).indicator (fun _ : Ω => (1 : ℝ)) | m] =ᵐ[μ] B.indicator (fun _ : Ω => (1 : ℝ)) * μ[(A ∩ C).indicator (fun _ : Ω => (1 : ℝ)) | m] := MeasureTheory.condExp_stronglyMeasurable_mul_of_bound hm hB_sm hAC_int 1 hB_bound have hpull_A : μ[B.indicator (fun _ : Ω => (1 : ℝ)) * A.indicator (fun _ : Ω => (1 : ℝ)) | m] =ᵐ[μ] B.indicator (fun _ : Ω => (1 : ℝ)) * μ[A.indicator (fun _ : Ω => (1 : ℝ)) | m] := MeasureTheory.condExp_stronglyMeasurable_mul_of_bound hm hB_sm hA_int 1 hB_bound have hCIeq := (ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul _hW _hZ).mp _hCI s v hs_meas hv_meas have hleft : μ⟦((A ∩ B) ∩ C) | m⟧ =ᵐ[μ] μ[B.indicator (fun _ : Ω => (1 : ℝ)) * (A ∩ C).indicator (fun _ : Ω => (1 : ℝ)) | m] := by rw [show ((A ∩ B) ∩ C) = B ∩ (A ∩ C) by ext ω simp [and_left_comm, and_assoc]] rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one] have hpair : μ⟦(A ∩ B) | m⟧ =ᵐ[μ] μ[B.indicator (fun _ : Ω => (1 : ℝ)) * A.indicator (fun _ : Ω => (1 : ℝ)) | m] := by rw [show (A ∩ B) = B ∩ A by ext ω simp [and_comm]] rw [show (fun _ : Ω => (1 : ℝ)) = 1 from rfl, Set.inter_indicator_one] calc μ⟦pair ⁻¹' (s ×ˢ u) ∩ Z ⁻¹' v | m⟧ =ᵐ[μ] μ⟦((A ∩ B) ∩ C) | m⟧ := by rfl _ =ᵐ[μ] μ[B.indicator (fun _ : Ω => (1 : ℝ)) * (A ∩ C).indicator (fun _ : Ω => (1 : ℝ)) | m] := hleft _ =ᵐ[μ] B.indicator (fun _ : Ω => (1 : ℝ)) * μ[(A ∩ C).indicator (fun _ : Ω => (1 : ℝ)) | m] := hpull_AC _ =ᵐ[μ] B.indicator (fun _ : Ω => (1 : ℝ)) * (μ⟦A | m⟧ * μ⟦C | m⟧) := by exact hCIeq.mono fun ω hω => by simp [A, C, hω] _ =ᵐ[μ] (B.indicator (fun _ : Ω => (1 : ℝ)) * μ⟦A | m⟧) * μ⟦C | m⟧ := by exact MeasureTheory.ae_of_all μ fun ω => by simp only [Pi.mul_apply] ring _ =ᵐ[μ] μ[B.indicator (fun _ : Ω => (1 : ℝ)) * A.indicator (fun _ : Ω => (1 : ℝ)) | m] * μ⟦C | m⟧ := by exact hpull_A.symm.mul (Filter.EventuallyEq.rfl) _ =ᵐ[μ] μ⟦A ∩ B | m⟧ * μ⟦C | m⟧ := by exact hpair.symm.mul (Filter.EventuallyEq.rfl) _ =ᵐ[μ] μ⟦pair ⁻¹' (s ×ˢ u) | m⟧ * μ⟦Z ⁻¹' v | m⟧ := by rfl rw [ProbabilityTheory.condIndepFun_iff_condIndep] have hpPair_eq : pPair = (fun r : Set (α × β) => pair ⁻¹' r) '' rects := by ext q constructor · rintro ⟨s, hs, u, hu, hq⟩ exact ⟨s ×ˢ u, ⟨s, hs, u, hu, rfl⟩, hq⟩ · rintro ⟨r, ⟨s, hs, u, hu, rfl⟩, hq⟩ exact ⟨s, hs, u, hu, hq⟩ have hgenPair : (inferInstance : MeasurableSpace (α × β)).comap pair = MeasurableSpace.generateFrom pPair := by rw [hpPair_eq, ← generateFrom_prod, MeasurableSpace.comap_generateFrom] have hgenZ : (inferInstance : MeasurableSpace γ).comap Z = MeasurableSpace.generateFrom pZ := by rw [show (inferInstance : MeasurableSpace γ) = MeasurableSpace.generateFrom zsets by exact (MeasurableSpace.generateFrom_measurableSet (α := γ)).symm] rw [MeasurableSpace.comap_generateFrom] rfl rw [hgenPair, hgenZ] exact ProbabilityTheory.CondIndepSets.condIndep' hpPair_meas hpZ_meas hpPair_pi hpZ_pi hrect
FiniteProductResidual 5 core · 13 supporting This module packages the product law of an independent side variable and a finite iid record array. ★ condExp_residual_eq_zero_of_leaveOne
Leave-one residual centering under finite product laws
This module packages the product law of an independent side variable and a finite iid record array. It proves that a one-record residual conditionally centered on its covariate remains centered after adjoining the side variable and every other record, and derives integrable leave-one pullout and distinct-coordinate orthogonality identities.
def productLaw reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.FiniteProductResidual
The side law and record law determine the joint law of an independent side variable and a finite iid record array, given by their product with the finite record product law.
def otherInfo reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.FiniteProductResidual
For a selected coordinate and a side-variable-and-record-array realization, the remaining-information map retains the side variable and every record other than the selected one, by projecting that realization.
Definition (Lean source)
parameters
ι :
Type u_1
A :
Type u_2
Z :
Type u_3
i :
ι
az :
A × (ι → Z)
def
otherInfo i az :
A × ({j : ι // j ≠ i} → Z)
given by
(az.1, fun j => az.2 j.1)
def leaveOneInfo reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.FiniteProductResidual
A covariate map, selected coordinate, and a side-variable-and-record-array realization determine the leave-one information map, which retains the side variable, the selected covariate, and all other complete records, by projecting that realization.
Definition (Lean source)
parameters
ι :
Type u_1
A :
Type u_2
Z :
Type u_3
C :
Type u_4
X :
Z → C
i :
ι
az :
A × (ι → Z)
def
leaveOneInfo X i az :
A × C × ({j : ι // j ≠ i} → Z)
given by
(az.1, X (az.2 i), fun j => az.2 j.1)
def covariateInfo reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.FiniteProductResidual
A covariate map and a side-variable-and-record-array realization determine the full covariate-information map, which retains the side variable and every record's covariate, by applying the covariate map coordinatewise.
Definition (Lean source)
parameters
ι :
Type u_1
A :
Type u_2
Z :
Type u_3
C :
Type u_4
X :
Z → C
az :
A × (ι → Z)
def
covariateInfo X az :
A × (ι → C)
given by
(az.1, fun k => X (az.2 k))
theorem condExp_residual_eq_zero_of_leaveOne reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional.FiniteProductResidual
A measurable covariate map and residual, integrability of the residual under the record law, zero conditional mean of the residual given the covariate under the record law, probability side and record laws on standard Borel spaces, and a selected coordinate imply that, under the joint law of an independent side variable and a finite iid record array, the selected record's residual has zero conditional mean given the selected covariate, the side variable, and all other records.
Formal statement
hypotheses
ι :
Type u_1
A :
Type u_2
Z :
Type u_3
C :
Type u_4
X :
Z → C
r :
Z → ℝ
hX :
hr :
hir :
Integrable r μ
hzero :
μ[r | comap X inferInstance] =ᵐ[μ] 0
i :
ι
conclusion
=ᵐ[productLaw ρ μ] 0
Proof (Lean source)
theorem condExp_residual_eq_zero_of_leaveOne
(hX : Measurable X) (hr : Measurable r) (hir : Integrable r μ)
(hzero : μ[r | comap X inferInstance] =ᵐ[μ] 0) (i : ι) :
(productLaw ρ μ)[fun az => r (az.2 i) |
comap (leaveOneInfo X i) inferInstance] =ᵐ[productLaw ρ μ] 0 := by
classical
have hp := measurePreserving_selectedRecord ρ μ i
have hi : Integrable (fun az : A × (ι → Z) => r (az.2 i)) (productLaw ρ μ) :=
hp.integrable_comp_of_integrable hir
have hd := condExp_adjoin_independent_eq hp.measurable (measurable_otherInfo i)
(indepFun_selectedRecord_otherInfo ρ μ i) hX hr hi
have ht := condExp_comp_of_map_eq (fun az : A × (ι → Z) => az.2 i) hp.measurable
hp.map_eq (comap X inferInstance) hX.comap_le hir
have hz : (fun az : A × (ι → Z) =>
(μ[r | comap X inferInstance]) (az.2 i))
=ᵐ[productLaw ρ μ] 0 := by
filter_upwards [hp.quasiMeasurePreserving.ae_eq hzero] with az hza
exact hza
rw [comap_leaveOneInfo]
apply hd.trans
have ht' : (productLaw ρ μ)[fun az => r (az.2 i) |
comap (X ∘ fun az : A × (ι → Z) => az.2 i) inferInstance]
=ᵐ[productLaw ρ μ] fun az => (μ[r | comap X inferInstance]) (az.2 i) := by
simpa only [MeasurableSpace.comap_comp, Function.comp_def] using ht
exact ht'.trans hz
13 supporting declarations (lemmas, instances)
-
instIsProbabilityMeasureProductLawinstance — Probability side and record laws make their joint product law a probability law, by the probability-measure instances for products and finite product measures. -
measurable_otherInfotheorem — For a selected coordinate, the remaining-information map is measurable.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3i :ιconclusionMeasurable (otherInfo (A := A) (Z := Z) i)Proof (Lean source)
@[fun_prop] theorem measurable_otherInfo (i : ι) : Measurable (otherInfo (A := A) (Z := Z) i) := by exact measurable_fst.prodMk (measurable_pi_lambda _ fun (j : {j : ι // j ≠ i}) => (measurable_pi_apply j.1).comp measurable_snd) -
measurable_leaveOneInfotheorem — A measurable covariate map makes the leave-one information at the selected coordinate measurable.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4Z → ChX :i :ιconclusionMeasurable (leaveOneInfo (A := A) X i)Proof (Lean source)
@[fun_prop] theorem measurable_leaveOneInfo {X : Z → C} (hX : Measurable X) (i : ι) : Measurable (leaveOneInfo (A := A) X i) := by exact measurable_fst.prodMk ((hX.comp ((measurable_pi_apply i).comp measurable_snd)).prodMk (measurable_pi_lambda _ fun (j : {j : ι // j ≠ i}) => (measurable_pi_apply j.1).comp measurable_snd)) -
measurable_covariateInfotheorem — A measurable covariate map makes the full covariate-information map measurable.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4Z → ChX :conclusionMeasurable (covariateInfo (ι := ι) (A := A) X)Proof (Lean source)
@[fun_prop] theorem measurable_covariateInfo {X : Z → C} (hX : Measurable X) : Measurable (covariateInfo (ι := ι) (A := A) X) := by exact measurable_fst.prodMk (measurable_pi_lambda _ fun (k : ι) => hX.comp ((measurable_pi_apply k).comp measurable_snd)) -
comap_leaveOneInfotheorem — For a covariate map and selected coordinate, the σ-algebra generated by leave-one information is the join of the selected covariate σ-algebra and the remaining-information σ-algebra.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4X :Z → Ci :ιconclusion= comap (fun az : A × (ι → Z) => X (az.2 i)) inferInstance ⊔ comap (otherInfo (A := A) (Z := Z) i) inferInstanceProof (Lean source)
theorem comap_leaveOneInfo (X : Z → C) (i : ι) : comap (leaveOneInfo (A := A) X i) inferInstance = comap (fun az : A × (ι → Z) => X (az.2 i)) inferInstance ⊔ comap (otherInfo (A := A) (Z := Z) i) inferInstance := by unfold leaveOneInfo otherInfo simp only [inferInstance, instMeasurableSpace, MeasurableSpace.comap_prodMk] exact sup_left_comm _ _ _ -
measurable_otherRecord_comap_leaveOnetheorem — A covariate map, a selected coordinate, and a distinct off-coordinate record make that record measurable from the selected leave-one information.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4X :Z → Ci j :ιhji :j ≠ iconclusion@Measurable (A × (ι → Z)) Z (comap (leaveOneInfo X i) inferInstance) inferInstance (fun az => az.2 j)Proof (Lean source)
@[fun_prop] theorem measurable_otherRecord_comap_leaveOne (X : Z → C) (i j : ι) (hji : j ≠ i) : @Measurable (A × (ι → Z)) Z (comap (leaveOneInfo X i) inferInstance) inferInstance (fun az => az.2 j) := by have h : @Measurable (A × (ι → Z)) (A × C × ({j : ι // j ≠ i} → Z)) (comap (leaveOneInfo X i) inferInstance) inferInstance (leaveOneInfo X i) := Measurable.of_comap_le le_rfl exact (measurable_pi_apply (⟨j, hji⟩ : {j : ι // j ≠ i})).comp (measurable_snd.comp (measurable_snd.comp h)) -
measurable_covariateInfo_comap_leaveOnetheorem — A measurable covariate map and a selected coordinate make the full covariate-information map measurable from leave-one information.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4Z → ChX :i :ιconclusion@Measurable (A × (ι → Z)) (A × (ι → C)) (comap (leaveOneInfo X i) inferInstance) inferInstance (covariateInfo X)Proof (Lean source)
@[fun_prop] theorem measurable_covariateInfo_comap_leaveOne {X : Z → C} (hX : Measurable X) (i : ι) : @Measurable (A × (ι → Z)) (A × (ι → C)) (comap (leaveOneInfo X i) inferInstance) inferInstance (covariateInfo X) := by have h : @Measurable (A × (ι → Z)) (A × C × ({j : ι // j ≠ i} → Z)) (comap (leaveOneInfo X i) inferInstance) inferInstance (leaveOneInfo X i) := Measurable.of_comap_le le_rfl classical let : MeasurableSpace (A × (ι → Z)) := comap (leaveOneInfo X i) inferInstance unfold covariateInfo refine (measurable_fst.comp h).prodMk (measurable_pi_lambda _ fun (k : ι) => ?_) by_cases hki : k = i · subst k exact measurable_fst.comp (measurable_snd.comp h) · exact hX.comp (measurable_otherRecord_comap_leaveOne X i k hki) -
measurePreserving_selectedRecordtheorem — Probability side and record laws make projection to a selected record preserve the one-record law.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3Fintype ιρ :Measure Aμ :Measure Zi :ιconclusionMeasurePreserving (fun az : A × (ι → Z) => az.2 i) (productLaw ρ μ) μProof (Lean source)
theorem measurePreserving_selectedRecord [Fintype ι] (ρ : Measure A) (μ : Measure Z) [IsProbabilityMeasure ρ] [IsProbabilityMeasure μ] (i : ι) : MeasurePreserving (fun az : A × (ι → Z) => az.2 i) (productLaw ρ μ) μ := by exact (measurePreserving_eval (fun _ : ι => μ) i).comp measurePreserving_snd -
indepFun_selectedRecord_otherInfotheorem — Probability side and record laws make the selected record independent of the side variable together with every other record.Proof (Lean source)
theorem indepFun_selectedRecord_otherInfo {ι A Z : Type*} [Fintype ι] [MeasurableSpace A] [MeasurableSpace Z] (ρ : Measure A) (μ : Measure Z) [IsProbabilityMeasure ρ] [IsProbabilityMeasure μ] (i : ι) : IndepFun (fun az : A × (ι → Z) => az.2 i) (otherInfo i) (productLaw ρ μ) := by classical let P : Measure (ι → Z) := Measure.pi (fun _ : ι => μ) let rest : (ι → Z) → ({j : ι // j ≠ i} → Z) := fun x j => x j.1 have hrest : Measurable rest := measurable_pi_lambda _ fun j => measurable_pi_apply j.1 have hcoords : iIndepFun (fun j (x : ι → Z) => x j) P := iIndepFun_pi (X := fun _ (z : Z) => z) (fun _ => aemeasurable_id) have hblocks : IndepFun (fun x : ι → Z => x i) rest P := by have h := hcoords.indepFun_finset {i} (Finset.univ.erase i) (by simp) (fun j => measurable_pi_apply j) exact h.comp (measurable_pi_apply (⟨i, by simp⟩ : {j : ι // j ∈ ({i} : Finset ι)})) (measurable_pi_lambda _ fun (j : {j : ι // j ≠ i}) => measurable_pi_apply (⟨j.1, by simp [j.2]⟩ : {j : ι // j ∈ Finset.univ.erase i})) let ν := P.map rest have : IsProbabilityMeasure ν := Measure.isProbabilityMeasure_map hrest.aemeasurable have hpair : MeasurePreserving (fun x : ι → Z => (x i, rest x)) P (μ.prod ν) := by refine ⟨(measurable_pi_apply i).prodMk hrest, ?_⟩ rw [hblocks.map_prod_eq_prod_map_map (measurable_pi_apply i).aemeasurable hrest.aemeasurable, (measurePreserving_eval (fun _ : ι => μ) i).map_eq] have hside := (MeasurePreserving.id ρ).prod hpair have hunassoc := (measurePreserving_prodAssoc ρ μ ν).symm MeasurableEquiv.prodAssoc have hswap := (Measure.measurePreserving_swap (μ := ρ) (ν := μ)).prod (MeasurePreserving.id ν) have hassoc := measurePreserving_prodAssoc μ ρ ν have hjoint : MeasurePreserving (fun az : A × (ι → Z) => (az.2 i, otherInfo i az)) (productLaw ρ μ) (μ.prod (ρ.prod ν)) := hassoc.comp (hswap.comp (hunassoc.comp hside)) have hselected : MeasurePreserving (fun az : A × (ι → Z) => az.2 i) (productLaw ρ μ) μ := measurePreserving_fst.comp hjoint have hother : MeasurePreserving (otherInfo i) (productLaw ρ μ) (ρ.prod ν) := measurePreserving_snd.comp hjoint apply (indepFun_iff_map_prod_eq_prod_map_map ((measurable_pi_apply i).comp measurable_snd).aemeasurable (measurable_otherInfo i).aemeasurable).2 exact hjoint.map_eq.trans (congrArg₂ Measure.prod hselected.map_eq.symm hother.map_eq.symm) -
condExp_adjoin_independent_eqtheorem — Measurable record and additional-information maps that are independent, together with a measurable covariate map, a measurable residual, and integrability of the pulled-back residual, imply that adjoining the additional information leaves the residual's covariate conditional mean unchanged.hypothesesΩ Z C B :Y :Ω → ZW :Ω → BX :Z → Cr :Z → ℝhY :hW :hYW :IndepFun Y W PhX :hr :hrY :Integrable (fun ω => r (Y ω)) Pconclusion=ᵐ[P] P[fun ω => r (Y ω) | comap (X ∘ Y) inferInstance]Proof (Lean source)
theorem condExp_adjoin_independent_eq {Ω Z C B : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [MeasurableSpace Z] [MeasurableSpace C] [MeasurableSpace B] {P : Measure Ω} [IsProbabilityMeasure P] {Y : Ω → Z} {W : Ω → B} {X : Z → C} {r : Z → ℝ} (hY : Measurable Y) (hW : Measurable W) (hYW : IndepFun Y W P) (hX : Measurable X) (hr : Measurable r) (hrY : Integrable (fun ω => r (Y ω)) P) : P[fun ω => r (Y ω) | comap (X ∘ Y) inferInstance ⊔ comap W inferInstance] =ᵐ[P] P[fun ω => r (Y ω) | comap (X ∘ Y) inferInstance] := by have hrY_meas : Measurable (r ∘ Y) := hr.comp hY have hXY_meas : Measurable (X ∘ Y) := hX.comp hY have hpair : IndepFun (fun ω => (r (Y ω), X (Y ω))) W P := hYW.comp (φ := fun z => (r z, X z)) (ψ := id) (hr.prod hX) measurable_id have hbot := condIndepFun_bot_of_indepFun hW (hrY_meas.prod hXY_meas) hpair.symm have hCI : CondIndepFun (comap (X ∘ Y) inferInstance) hXY_meas.comap_le W (r ∘ Y) P := by simpa only [bot_sup_eq] using (condIndepFun_weak_union_of_prodMk (m := ⊥) bot_le hW hrY_meas hXY_meas hbot) exact condExp_sup_comap_eq_of_condIndep hXY_meas.comap_le hW hrY_meas hCI.symm (h := id) measurable_id hrY -
integral_mul_residual_eq_zero_of_leaveOnetheorem — A measurable covariate map and residual, integrability of the residual, one-record conditional centering, probability side and record laws, a selected coordinate, a leave-one almost-everywhere strongly measurable coefficient, and integrability of its residual product imply that the coefficient-residual integral is zero.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4X :sharedZ → Cr :sharedZ → ℝhX :hr :hir :Integrable r μhzero :μ[r | comap X inferInstance] =ᵐ[μ] 0i :ιc :A × (ι → Z) → ℝhc :hcr :Integrable (fun az => c az * r (az.2 i)) (productLaw ρ μ)conclusion∫ az, c az * r (az.2 i) ∂productLaw ρ μ = 0Proof (Lean source)
theorem integral_mul_residual_eq_zero_of_leaveOne (hX : Measurable X) (hr : Measurable r) (hir : Integrable r μ) (hzero : μ[r | comap X inferInstance] =ᵐ[μ] 0) (i : ι) (c : A × (ι → Z) → ℝ) (hc : AEStronglyMeasurable[comap (leaveOneInfo X i) inferInstance] c (productLaw ρ μ)) (hcr : Integrable (fun az => c az * r (az.2 i)) (productLaw ρ μ)) : ∫ az, c az * r (az.2 i) ∂productLaw ρ μ = 0 := by have hm := (measurable_leaveOneInfo (A := A) hX i).comap_le have hi : Integrable (fun az : A × (ι → Z) => r (az.2 i)) (productLaw ρ μ) := (measurePreserving_selectedRecord ρ μ i).integrable_comp_of_integrable hir have hp := condExp_mul_of_aestronglyMeasurable_left hc hcr hi have hfun : c * (fun az => r (az.2 i)) = (fun az => c az * r (az.2 i)) := by funext az exact Pi.mul_apply c _ az rw [hfun] at hp have hz := condExp_residual_eq_zero_of_leaveOne ρ μ hX hr hir hzero i have hpz : (productLaw ρ μ)[fun az => c az * r (az.2 i) | comap (leaveOneInfo X i) inferInstance] =ᵐ[productLaw ρ μ] 0 := by filter_upwards [hp, hz] with az hpa hza simpa only [Pi.mul_apply, hza, Pi.zero_apply, mul_zero] using hpa calc ∫ az, c az * r (az.2 i) ∂productLaw ρ μ = ∫ az, ((productLaw ρ μ)[fun az => c az * r (az.2 i) | comap (leaveOneInfo X i) inferInstance]) az ∂productLaw ρ μ := (integral_condExp hm).symm _ = ∫ _, (0 : ℝ) ∂productLaw ρ μ := integral_congr_ae hpz _ = 0 := integral_zero _ _ -
integral_covariate_mul_residual_eq_zerotheorem — A measurable covariate map and residual, integrability of the residual, one-record conditional centering, probability side and record laws, a selected coordinate, a measurable covariate coefficient, and integrability of its residual product imply that the covariate-weighted residual integral is zero.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4X :sharedZ → Cr :sharedZ → ℝhX :hr :hir :Integrable r μhzero :μ[r | comap X inferInstance] =ᵐ[μ] 0i :ιb :A × (ι → C) → ℝhb :hbr :Integrable (fun az => b (covariateInfo X az) * r (az.2 i)) (productLaw ρ μ)conclusion∫ az, b (covariateInfo X az) * r (az.2 i) ∂productLaw ρ μ = 0Proof (Lean source)
theorem integral_covariate_mul_residual_eq_zero (hX : Measurable X) (hr : Measurable r) (hir : Integrable r μ) (hzero : μ[r | comap X inferInstance] =ᵐ[μ] 0) (i : ι) (b : A × (ι → C) → ℝ) (hb : Measurable b) (hbr : Integrable (fun az => b (covariateInfo X az) * r (az.2 i)) (productLaw ρ μ)) : ∫ az, b (covariateInfo X az) * r (az.2 i) ∂productLaw ρ μ = 0 := by apply integral_mul_residual_eq_zero_of_leaveOne ρ μ hX hr hir hzero i _ _ hbr exact (hb.comp (measurable_covariateInfo_comap_leaveOne hX i)) |>.stronglyMeasurable.aestronglyMeasurable -
integral_covariate_mul_residual_mul_residual_eq_zerotheorem — A measurable covariate map and residual, integrability of the residual, one-record conditional centering, probability side and record laws, distinct coordinates, a measurable covariate coefficient, and integrability of the triple product imply that the covariate-weighted product of the two residuals has zero integral.hypothesesι :sharedType u_1A :sharedType u_2Z :sharedType u_3C :sharedType u_4X :sharedZ → Cr :sharedZ → ℝhX :hr :hir :Integrable r μhzero :μ[r | comap X inferInstance] =ᵐ[μ] 0i j :ιhij :i ≠ jb :A × (ι → C) → ℝhb :hbrr :Integrable (fun az => b (covariateInfo X az) * r (az.2 i) * r (az.2 j)) (productLaw ρ μ)conclusion∫ az, b (covariateInfo X az) * r (az.2 i) * r (az.2 j) ∂productLaw ρ μ = 0Proof (Lean source)
theorem integral_covariate_mul_residual_mul_residual_eq_zero (hX : Measurable X) (hr : Measurable r) (hir : Integrable r μ) (hzero : μ[r | comap X inferInstance] =ᵐ[μ] 0) (i j : ι) (hij : i ≠ j) (b : A × (ι → C) → ℝ) (hb : Measurable b) (hbrr : Integrable (fun az => b (covariateInfo X az) * r (az.2 i) * r (az.2 j)) (productLaw ρ μ)) : ∫ az, b (covariateInfo X az) * r (az.2 i) * r (az.2 j) ∂productLaw ρ μ = 0 := by have hc : AEStronglyMeasurable[comap (leaveOneInfo X i) inferInstance] (fun az => b (covariateInfo X az) * r (az.2 j)) (productLaw ρ μ) := ((hb.comp (measurable_covariateInfo_comap_leaveOne hX i)).mul (hr.comp (measurable_otherRecord_comap_leaveOne X i j (Ne.symm hij)))) |>.stronglyMeasurable.aestronglyMeasurable have hprod : Integrable (fun az => (b (covariateInfo X az) * r (az.2 j)) * r (az.2 i)) (productLaw ρ μ) := by simpa only [mul_right_comm] using hbrr simpa only [mul_right_comm] using integral_mul_residual_eq_zero_of_leaveOne ρ μ hX hr hir hzero i _ hc hprod
Integrability 2 core · 0 supporting This file proves measure-theoretic lemmas that turn conditional positivity and conditional-expectation identities for indicators into positivity and integrability conclusions over sub-σ-algebras. ★ ae_pos_condExp_indicator_of_le★ integrableOn_of_condExp_indicator_mul
Integrability from Conditional-Expectation Indicators
This file proves measure-theoretic lemmas that turn conditional positivity and conditional-expectation identities for indicators into positivity and integrability conclusions over sub-σ-algebras.
The theorem ae_pos_condExp_indicator_of_le derives strict conditional positivity
from overlap on the conditioning σ-algebra. The theorem
integrableOn_of_condExp_indicator_mul turns an m-measurable nonnegative
function satisfying an indicator conditional-expectation product identity into
an integrable-on-stratum conclusion.
theorem ae_pos_condExp_indicator_of_le reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
σ-projection of indicator-conditional positivity. For a sub-σ-algebra m₁ coarser than the ambient σ-algebra, a measurable event E, and an overlap condition — every m₁-measurable set that meets E only on a null set is itself null, then the conditional probability of E given m₁ is strictly positive almost everywhere.
Formal statement
hypotheses
conclusion
∀ᵐ ω ∂μ, 0 < (μ[indicator E (fun _ => (1:ℝ)) | m₁]) ω
Proof (Lean source)
theorem ae_pos_condExp_indicator_of_le
{Ω : Type*} {mΩ : MeasurableSpace Ω}
{μ : @Measure Ω mΩ} [@IsFiniteMeasure Ω mΩ μ]
{m₁ : MeasurableSpace Ω} (_h₁ : m₁ ≤ mΩ)
{E : Set Ω} (hE : @MeasurableSet Ω mΩ E)
(_h_overlap : ∀ s : Set Ω, MeasurableSet[m₁] s →
μ (s ∩ E) = 0 → μ s = 0) :
∀ᵐ ω ∂μ,
0 < (μ[indicator E (fun _ => (1:ℝ)) | m₁]) ω := by
let f : Ω → ℝ := indicator E (fun _ => (1 : ℝ))
let p : Ω → ℝ := μ[f | m₁]
let S : Set Ω := {ω | p ω = 0}
haveI : IsFiniteMeasure (μ.trim _h₁) :=
MeasureTheory.isFiniteMeasure_trim _h₁
have hf_int : Integrable f μ := by
dsimp [f]
exact (MeasureTheory.integrable_const (μ := μ) (1 : ℝ)).indicator hE
have hp_nonneg : 0 ≤ᵐ[μ] p := by
dsimp [p, f]
exact MeasureTheory.condExp_nonneg (Filter.Eventually.of_forall fun ω =>
Set.indicator_nonneg (fun _ _ => zero_le_one) _)
have hp_sm : StronglyMeasurable[m₁] p := by fun_prop
have hS_m1 : MeasurableSet[m₁] S := by
dsimp [S]
exact hp_sm.measurable (measurableSet_singleton (0 : ℝ))
have hS_mΩ : @MeasurableSet Ω mΩ S := _h₁ S hS_m1
have hset : ∫ ω in S, p ω ∂μ = ∫ ω in S, f ω ∂μ := by
dsimp [p]
exact MeasureTheory.setIntegral_condExp _h₁ hf_int hS_m1
have hp_set_zero : ∫ ω in S, p ω ∂μ = 0 := by
have hp_ae_zero_on_S : p =ᵐ[μ.restrict S] 0 := by
filter_upwards [MeasureTheory.self_mem_ae_restrict (μ := μ) hS_mΩ] with ω hω
exact hω
simpa using MeasureTheory.integral_congr_ae hp_ae_zero_on_S
have hf_set_zero : ∫ ω in S, f ω ∂μ = 0 := by
exact hset.symm.trans hp_set_zero
have hf_set_real : ∫ ω in S, f ω ∂μ = μ.real (S ∩ E) := by
dsimp [f]
rw [MeasureTheory.setIntegral_indicator hE]
simp [Set.inter_comm]
have hSE_zero : μ (S ∩ E) = 0 := by
rw [← MeasureTheory.measureReal_eq_zero_iff (μ := μ) (s := S ∩ E)]
rw [← hf_set_real]
exact hf_set_zero
have hS_zero : μ S = 0 := by
exact _h_overlap S hS_m1 hSE_zero
have hS_ae : ∀ᵐ ω ∂μ, ω ∉ S := by
rw [MeasureTheory.ae_iff]
simpa using hS_zero
filter_upwards [hp_nonneg, hS_ae] with ω hp_nonnegω hω_notS
change 0 < p ω
exact lt_of_le_of_ne hp_nonnegω (Ne.symm hω_notS)
theorem integrableOn_of_condExp_indicator_mul reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Integrability on a stratum from a conditional-expectation indicator identity. For a sub-σ-algebra m coarser than the ambient σ-algebra, measurable events B and C, and an m-measurable real-valued function g that is almost everywhere nonnegative, if the conditional expectation of the indicator of B given m, multiplied pointwise by g, equals almost everywhere the conditional expectation of the indicator of C given m, then g is integrable on B.
Formal statement
hypotheses
Ω :
_hm :
m ≤ mΩ
B C :
Set Ω
_hB :
@MeasurableSet Ω mΩ B
_hC :
@MeasurableSet Ω mΩ C
g :
Ω → ℝ
_hg_meas :
Measurable[m] g
_hg_nn :
0 ≤ᵐ[μ] g
conclusion
IntegrableOn g B μ
Proof (Lean source)
theorem integrableOn_of_condExp_indicator_mul
{Ω : Type*} {mΩ : MeasurableSpace Ω}
{μ : @Measure Ω mΩ} [@IsFiniteMeasure Ω mΩ μ]
{m : MeasurableSpace Ω} (_hm : m ≤ mΩ)
{B C : Set Ω} (_hB : @MeasurableSet Ω mΩ B) (_hC : @MeasurableSet Ω mΩ C)
{g : Ω → ℝ} (_hg_meas : Measurable[m] g) (_hg_nn : 0 ≤ᵐ[μ] g)
(_h_eq :
(fun ω =>
(μ[indicator B (fun _ => (1 : ℝ)) | m]) ω * g ω)
=ᵐ[μ]
(μ[indicator C (fun _ => (1 : ℝ)) | m])) :
IntegrableOn g B μ := by
haveI : SigmaFinite (μ.trim _hm) := inferInstance
let IB : Ω → ℝ := indicator B (fun _ => (1 : ℝ))
let IC : Ω → ℝ := indicator C (fun _ => (1 : ℝ))
have hIB_int : Integrable IB μ := by
dsimp [IB]
exact (MeasureTheory.integrable_const (μ := μ) (1 : ℝ)).indicator _hB
have hIB_nn : 0 ≤ᵐ[μ] IB := by
refine Filter.Eventually.of_forall ?_
intro ω
dsimp [IB]
by_cases hω : ω ∈ B
· simp [Set.indicator_of_mem hω]
· simp [Set.indicator_of_notMem hω]
have hIB_bound : ∀ᵐ ω ∂μ, ‖IB ω‖ ≤ (1 : ℝ) := by
refine Filter.Eventually.of_forall ?_
intro ω
dsimp [IB]
by_cases hω : ω ∈ B
· simp [Set.indicator_of_mem hω]
· simp [Set.indicator_of_notMem hω]
have hpB_nn : 0 ≤ᵐ[μ] (μ[IB | m]) :=
MeasureTheory.condExp_nonneg (f := IB) (m := m) (μ := μ) hIB_nn
have hpC_int : Integrable (μ[IC | m]) μ :=
MeasureTheory.integrable_condExp
let gn : ℕ → Ω → ℝ := fun n ω => min (max (g ω) 0) (n : ℝ)
have hgn_meas (n : ℕ) : Measurable[m] (gn n) := by fun_prop
have hgn_sm (n : ℕ) :
@StronglyMeasurable Ω ℝ _ m (gn n) :=
(hgn_meas n).stronglyMeasurable
have hgn_nn (n : ℕ) : 0 ≤ᵐ[μ] gn n := by
refine Filter.Eventually.of_forall ?_
intro ω
dsimp [gn]
exact le_min (le_max_right _ _) (Nat.cast_nonneg n)
have hgn_bound (n : ℕ) : ∀ᵐ ω ∂μ, ‖gn n ω‖ ≤ (n : ℝ) := by
refine Filter.Eventually.of_forall ?_
intro ω
have hnon : 0 ≤ gn n ω :=
le_min (le_max_right _ _) (Nat.cast_nonneg n)
have hle : gn n ω ≤ (n : ℝ) := min_le_right _ _
simpa [Real.norm_of_nonneg hnon] using hle
have hgn_le_g (n : ℕ) : gn n ≤ᵐ[μ] g := by
filter_upwards [_hg_nn] with ω hgω
dsimp [gn]
exact (min_le_left _ _).trans (max_eq_left hgω).le
have hgn_int (n : ℕ) : Integrable (gn n) μ := by
have hmeas : @Measurable Ω ℝ mΩ _ (gn n) :=
(hgn_meas n).mono _hm le_rfl
exact MeasureTheory.Integrable.of_bound
hmeas.aestronglyMeasurable (n : ℝ) (hgn_bound n)
have htrunc_bound :
∀ n : ℕ, ∫⁻ ω in B, ofReal (gn n ω) ∂μ ≤ μ C := by
intro n
have hpull : μ[(gn n) * IB | m] =ᵐ[μ] (gn n) * μ[IB | m] := by
exact MeasureTheory.condExp_stronglyMeasurable_mul_of_bound
_hm (hgn_sm n) hIB_int (n : ℝ) (hgn_bound n)
have hreal_eq :
∫ ω in B, gn n ω ∂μ
= ∫ ω, gn n ω * (μ[IB | m]) ω ∂μ := by
calc
∫ ω in B, gn n ω ∂μ
= ∫ ω, B.indicator (gn n) ω ∂μ :=
(MeasureTheory.integral_indicator _hB).symm
_ = ∫ ω, gn n ω * IB ω ∂μ := by
refine MeasureTheory.integral_congr_ae
(Filter.Eventually.of_forall ?_)
intro ω
dsimp [IB]
by_cases hω : ω ∈ B
· simp [Set.indicator_of_mem hω]
· simp [Set.indicator_of_notMem hω]
_ = ∫ ω, μ[(gn n) * IB | m] ω ∂μ := by
simpa [Pi.mul_apply] using
(MeasureTheory.integral_condExp
_hm (f := (gn n) * IB) (μ := μ)).symm
_ = ∫ ω, gn n ω * (μ[IB | m]) ω ∂μ := by
exact MeasureTheory.integral_congr_ae hpull
have hprod_le :
(fun ω => gn n ω * (μ[IB | m]) ω) ≤ᵐ[μ] (μ[IC | m]) := by
filter_upwards [hgn_le_g n, hpB_nn, _h_eq] with ω hle hpB hEq
calc
gn n ω * (μ[IB | m]) ω
≤ g ω * (μ[IB | m]) ω :=
mul_le_mul_of_nonneg_right hle hpB
_ = (μ[IB | m]) ω * g ω := by ring
_ = (μ[IC | m]) ω := hEq
have hprod_int :
Integrable
(fun ω => gn n ω * (μ[IB | m]) ω) μ := by
exact (MeasureTheory.integrable_condExp
(f := (gn n) * IB) (m := m) (μ := μ)).congr hpull
have hreal_le :
∫ ω in B, gn n ω ∂μ ≤ ∫ ω, (μ[IC | m]) ω ∂μ := by
rw [hreal_eq]
exact MeasureTheory.integral_mono_ae hprod_int hpC_int hprod_le
have hreal_rhs : ∫ ω, (μ[IC | m]) ω ∂μ = μ.real C := by
calc
∫ ω, (μ[IC | m]) ω ∂μ = ∫ ω, IC ω ∂μ :=
MeasureTheory.integral_condExp _hm
_ = μ.real C := by
dsimp [IC]
exact MeasureTheory.integral_indicator_one _hC
have hlin_eq :
ofReal (∫ ω in B, gn n ω ∂μ)
= ∫⁻ ω in B, ofReal (gn n ω) ∂μ := by
exact MeasureTheory.ofReal_integral_eq_lintegral_ofReal
((hgn_int n).restrict) (MeasureTheory.ae_restrict_of_ae (hgn_nn n))
calc
∫⁻ ω in B, ofReal (gn n ω) ∂μ
= ofReal (∫ ω in B, gn n ω ∂μ) := hlin_eq.symm
_ ≤ ofReal (∫ ω, (μ[IC | m]) ω ∂μ) :=
ENNReal.ofReal_le_ofReal hreal_le
_ = ofReal (μ.real C) := by rw [hreal_rhs]
_ = μ C := by
rw [MeasureTheory.measureReal_def,
ENNReal.ofReal_toReal (MeasureTheory.measure_ne_top μ C)]
have hpoint_iSup :
∀ ω, (⨆ n : ℕ, ofReal (gn n ω)) = ofReal (g ω) := by
intro ω
have hmono : Monotone (fun n : ℕ => ofReal (gn n ω)) := by
intro n k hnk
dsimp [gn]
exact ENNReal.ofReal_le_ofReal
(min_le_min le_rfl (by exact_mod_cast hnk))
apply iSup_eq_of_tendsto hmono
have heq :
(fun n : ℕ => ofReal (gn n ω))
=ᶠ[atTop] fun _ => ofReal (g ω) := by
rcases exists_nat_ge (max (g ω) 0) with ⟨N, hN⟩
refine Filter.eventually_atTop.2 ⟨N, ?_⟩
intro n hn
have hn' : max (g ω) 0 ≤ (n : ℝ) :=
hN.trans (by exact_mod_cast hn)
have hmin : min (max (g ω) 0) (n : ℝ) = max (g ω) 0 :=
min_eq_left hn'
simp [gn, hmin, ENNReal.ofReal_max]
exact heq.tendsto
have hmono_ae :
∀ᵐ ω ∂μ.restrict B,
Monotone fun n : ℕ => ofReal (gn n ω) := by
refine Filter.Eventually.of_forall ?_
intro ω n k hnk
dsimp [gn]
exact ENNReal.ofReal_le_ofReal
(min_le_min le_rfl (by exact_mod_cast hnk))
have haemeas :
∀ n : ℕ,
AEMeasurable
(fun ω => ofReal (gn n ω)) (μ.restrict B) := by
intro n
have hmeas : @Measurable Ω ℝ mΩ _ (gn n) :=
(hgn_meas n).mono _hm le_rfl
exact (hmeas.ennreal_ofReal.aemeasurable).restrict
have hmct :
∫⁻ ω in B, (⨆ n : ℕ, ofReal (gn n ω)) ∂μ
= ⨆ n : ℕ, ∫⁻ ω in B, ofReal (gn n ω) ∂μ := by
exact MeasureTheory.lintegral_iSup' (μ := μ.restrict B) haemeas hmono_ae
have hlin_g_le : ∫⁻ ω in B, ofReal (g ω) ∂μ ≤ μ C := by
calc
∫⁻ ω in B, ofReal (g ω) ∂μ
= ∫⁻ ω in B, (⨆ n : ℕ, ofReal (gn n ω)) ∂μ := by
refine MeasureTheory.lintegral_congr_ae
(Filter.Eventually.of_forall ?_)
intro ω
exact (hpoint_iSup ω).symm
_ = ⨆ n : ℕ, ∫⁻ ω in B, ofReal (gn n ω) ∂μ := hmct
_ ≤ μ C := iSup_le htrunc_bound
have hg_aesm :
@AEStronglyMeasurable Ω ℝ _ mΩ mΩ
g (μ.restrict B) := by
have hg_meas : @Measurable Ω ℝ mΩ _ g := _hg_meas.mono _hm le_rfl
exact hg_meas.aestronglyMeasurable.restrict
have hg_hfi : MeasureTheory.HasFiniteIntegral g (μ.restrict B) := by
rw [MeasureTheory.hasFiniteIntegral_iff_ofReal
(MeasureTheory.ae_restrict_of_ae _hg_nn)]
exact lt_of_le_of_lt hlin_g_le (MeasureTheory.measure_lt_top μ C)
exact ⟨hg_aesm, hg_hfi⟩
JoinedBlockProduct 2 core · 0 supporting This module factors the conditional expectation of a three-factor product when each factor may depend on a common training block and one disjoint evaluation block. ★ condExp_joinedBlockProduct_of_integrable
Conditional products on joined training and evaluation blocks
This module factors the conditional expectation of a three-factor product when each factor may depend on a common training block and one disjoint evaluation block.
def joinedBlockProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
The training block, the three evaluation blocks, and one joined-view score for each factor define the product of the three joined-view scores, by evaluating every score on its training-plus-evaluation coordinates and multiplying the resulting values.
theorem condExp_joinedBlockProduct_of_integrable reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
A finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness and pairwise evaluation disjointness, measurable joined-view scores, integrable individual scores, an integrable first two-factor product, and an integrable three-factor product imply that the conditional mean of the joined three-block product given the training block is almost surely the product of the three scores' conditional means given the training block.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
B0 :
Finset ι
htrain :
∀ t, Disjoint B0 (B t)
η :
(t : Fin 3) → ((i : {i // i ∈ B0 ∪ B t}) → Ω i.val) → ℝ
hηmeas :
∀ t, Measurable (η t)
hη :
∀ t, Integrable (fun x : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) x)) (Measure.pi μ)
hη01 :
Integrable (fun x : ∀ i, Ω i => η 0 (finsetCoordProj (B0 ∪ B 0) x) * η 1 (finsetCoordProj (B0 ∪ B 1) x)) (Measure.pi μ)
hηprod :
Integrable (joinedBlockProduct B0 B η) (Measure.pi μ)
conclusion
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (joinedBlockProduct B0 B η)
=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) x)
Proof (Lean source)
theorem condExp_joinedBlockProduct_of_integrable
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
(B0 : Finset ι) (B : Fin 3 → Finset ι)
(htrain : ∀ t, Disjoint B0 (B t))
(heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)))
(η : (t : Fin 3) → ((i : {i // i ∈ B0 ∪ B t}) → Ω i.val) → ℝ)
(hηmeas : ∀ t, Measurable (η t))
(hη : ∀ t, Integrable
(fun x : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) x)) (Measure.pi μ))
(hη01 : Integrable (fun x : ∀ i, Ω i =>
η 0 (finsetCoordProj (B0 ∪ B 0) x) *
η 1 (finsetCoordProj (B0 ∪ B 1) x)) (Measure.pi μ))
(hηprod : Integrable (joinedBlockProduct B0 B η) (Measure.pi μ)) :
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (joinedBlockProduct B0 B η) =ᵐ[Measure.pi μ]
(fun x => ∏ t : Fin 3,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ)
(fun y : ∀ i, Ω i => η t (finsetCoordProj (B0 ∪ B t) y)) x) := by
classical
have _htrain := htrain
let S01 := (B0 ∪ B 0) ∪ (B0 ∪ B 1)
have hm : comap (finsetCoordProj (Ω := Ω) B0) inferInstance ≤
(inferInstance : MeasurableSpace (∀ i, Ω i)) :=
comap_le (measurable_finsetCoordProj (Ω := Ω) B0)
have hF : (ofFinite ι) = (inferInstance : Fintype ι) :=
Subsingleton.elim _ _
have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = Measure.pi μ :=
congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hF
have hinter01 : (B0 ∪ B 0) ∩ (B0 ∪ B 1) ⊆ B0 := by
intro i hi
rcases Finset.mem_inter.mp hi with ⟨hleft, hright⟩
rcases Finset.mem_union.mp hleft with h0 | h0
· exact h0
rcases Finset.mem_union.mp hright with h1 | h1
· exact h1
exact False.elim ((Finset.disjoint_left.mp (heval (by decide : (0 : Fin 3) ≠ 1))) h0 h1)
have hinter012 : S01 ∩ (B0 ∪ B 2) ⊆ B0 := by
intro i hi
rcases Finset.mem_inter.mp hi with ⟨hleft, hright⟩
rcases Finset.mem_union.mp hright with h0 | h2
· exact h0
rcases Finset.mem_union.mp hleft with hleft | hleft
· rcases Finset.mem_union.mp hleft with h0 | h0
· exact h0
exact False.elim ((Finset.disjoint_left.mp (heval (by decide : (0 : Fin 3) ≠ 2))) h0 h2)
· rcases Finset.mem_union.mp hleft with h0 | h1
· exact h0
exact False.elim ((Finset.disjoint_left.mp (heval (by decide : (1 : Fin 3) ≠ 2))) h1 h2)
have hCI01 : CondIndepFun
(comap (finsetCoordProj (Ω := Ω) B0) inferInstance) hm
(finsetCoordProj (Ω := Ω) (B0 ∪ B 0))
(finsetCoordProj (Ω := Ω) (B0 ∪ B 1)) (Measure.pi μ) := by
simpa only [hpi] using
(condIndepFun_pi_of_inter_subset (Ω := Ω) μ hinter01)
have hCI012 : CondIndepFun
(comap (finsetCoordProj (Ω := Ω) B0) inferInstance) hm
(finsetCoordProj (Ω := Ω) S01)
(finsetCoordProj (Ω := Ω) (B0 ∪ B 2)) (Measure.pi μ) := by
simpa only [hpi] using
(condIndepFun_pi_of_inter_subset (Ω := Ω) μ hinter012)
have h01 :=
condExp_mul_of_condIndep
(μ := Measure.pi μ) hm
(measurable_finsetCoordProj (Ω := Ω) (B0 ∪ B 0))
(measurable_finsetCoordProj (Ω := Ω) (B0 ∪ B 1))
hCI01 (hηmeas 0) (hηmeas 1) (hη 0) (hη 1) hη01
let F : ((i : {i // i ∈ S01}) → Ω i.val) → ℝ :=
fun y =>
η 0 (fun i => y ⟨i.val, Finset.mem_union.mpr
(inl i.property)⟩) *
η 1 (fun i => y ⟨i.val, Finset.mem_union.mpr
(inr i.property)⟩)
have hFmeas : Measurable F := by
dsimp [F]
apply mul
· exact (hηmeas 0).comp
(measurable_pi_lambda _ (fun i => measurable_pi_apply _))
· exact (hηmeas 1).comp
(measurable_pi_lambda _ (fun i => measurable_pi_apply _))
have hFint : Integrable (fun x => F (finsetCoordProj S01 x)) (Measure.pi μ) := by
convert hη01 using 1
ext x
rfl
have hprod : Integrable (fun x =>
F (finsetCoordProj S01 x) * η 2 (finsetCoordProj (B0 ∪ B 2) x))
(Measure.pi μ) := by
convert hηprod using 1
ext x
simp only [joinedBlockProduct, Fin.prod_univ_three]
rfl
have hstep2 :=
condExp_mul_of_condIndep
(μ := Measure.pi μ) hm
(measurable_finsetCoordProj (Ω := Ω) S01)
(measurable_finsetCoordProj (Ω := Ω) (B0 ∪ B 2))
hCI012 hFmeas (hηmeas 2) hFint (hη 2) hprod
have hfun : (fun x : ∀ i, Ω i =>
F (finsetCoordProj S01 x) * η 2 (finsetCoordProj (B0 ∪ B 2) x)) =
joinedBlockProduct B0 B η := by
funext x
simp only [joinedBlockProduct, Fin.prod_univ_three]
rfl
have hfun01 : (fun x : ∀ i, Ω i => F (finsetCoordProj S01 x)) =
(fun x => η 0 (finsetCoordProj (B0 ∪ B 0) x) *
η 1 (finsetCoordProj (B0 ∪ B 1) x)) := by
funext x
rfl
rw [hfun, hfun01] at hstep2
have hfinal := hstep2.trans (h01.mul
(Filter.EventuallyEq.refl (ae (Measure.pi μ)) _))
filter_upwards [hfinal] with x hx
simpa [Fin.prod_univ_three] using hx
ShiftedBlockCrossMoment 1 core · 0 supporting The cross moment of two held-out scores shifted by training-measurable functions is their unconditional covariance plus the product of their shifted means. ★ condExp_shiftedBlockCross_eq_covariance_add
Conditional cross moment of one training-shifted held-out block
The cross moment of two held-out scores shifted by training-measurable functions is their unconditional covariance plus the product of their shifted means. This is the local calculation used by the three-block factorization.
theorem condExp_shiftedBlockCross_eq_covariance_add reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
A finite product probability law, disjoint training and held-out blocks, two held-out scores, two training shifts, measurability, integrability of the scores and shifts, an integrable held-out cross product, and square-integrable shifted scores imply that the conditional mean, given the training block, of the product of the two shifted scores almost surely equals the unconditional covariance of the two held-out scores plus the product of the two held-out means each minus its training shift.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
B0 B1 :
Finset ι
hdisj :
Disjoint B0 B1
f g :
((i : {i // i ∈ B1}) → Ω i.val) → ℝ
a b :
((i : {i // i ∈ B0}) → Ω i.val) → ℝ
hfmeas :
hgmeas :
hameas :
hbmeas :
hf :
Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x)) (Measure.pi μ)
hg :
Integrable (fun x : ∀ i, Ω i => g (finsetCoordProj B1 x)) (Measure.pi μ)
ha :
Integrable (fun x : ∀ i, Ω i => a (finsetCoordProj B0 x)) (Measure.pi μ)
hb :
Integrable (fun x : ∀ i, Ω i => b (finsetCoordProj B0 x)) (Measure.pi μ)
hfg :
hflp :
hglp :
conclusion
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => (f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x)) * (g (finsetCoordProj B1 x) - b (finsetCoordProj B0 x)))
=ᵐ[Measure.pi μ] (fun x => covariance (fun y : ∀ i, Ω i => f (finsetCoordProj B1 y)) (fun y : ∀ i, Ω i => g (finsetCoordProj B1 y)) (Measure.pi μ) + ((∫ y : (∀ i, Ω i), f (finsetCoordProj B1 y) ∂Measure.pi μ) - a (finsetCoordProj B0 x)) * ((∫ y : (∀ i, Ω i), g (finsetCoordProj B1 y) ∂Measure.pi μ) - b (finsetCoordProj B0 x)))
Proof (Lean source)
theorem condExp_shiftedBlockCross_eq_covariance_add
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
(B0 B1 : Finset ι) (hdisj : Disjoint B0 B1)
(f g : ((i : {i // i ∈ B1}) → Ω i.val) → ℝ)
(a b : ((i : {i // i ∈ B0}) → Ω i.val) → ℝ)
(hfmeas : Measurable f) (hgmeas : Measurable g)
(hameas : Measurable a) (hbmeas : Measurable b)
(hf : Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x))
(Measure.pi μ))
(hg : Integrable (fun x : ∀ i, Ω i => g (finsetCoordProj B1 x))
(Measure.pi μ))
(ha : Integrable (fun x : ∀ i, Ω i => a (finsetCoordProj B0 x))
(Measure.pi μ))
(hb : Integrable (fun x : ∀ i, Ω i => b (finsetCoordProj B0 x))
(Measure.pi μ))
(hfg : Integrable (fun x : ∀ i, Ω i =>
f (finsetCoordProj B1 x) * g (finsetCoordProj B1 x)) (Measure.pi μ))
(hflp : MemLp (fun x : ∀ i, Ω i =>
f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x)) 2 (Measure.pi μ))
(hglp : MemLp (fun x : ∀ i, Ω i =>
g (finsetCoordProj B1 x) - b (finsetCoordProj B0 x)) 2 (Measure.pi μ)) :
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ)
(fun x : ∀ i, Ω i =>
(f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x)) *
(g (finsetCoordProj B1 x) - b (finsetCoordProj B0 x))) =ᵐ[Measure.pi μ]
(fun x => covariance
(fun y : ∀ i, Ω i => f (finsetCoordProj B1 y))
(fun y : ∀ i, Ω i => g (finsetCoordProj B1 y))
(Measure.pi μ) +
((∫ y : (∀ i, Ω i), f (finsetCoordProj B1 y) ∂Measure.pi μ) -
a (finsetCoordProj B0 x)) *
((∫ y : (∀ i, Ω i), g (finsetCoordProj B1 y) ∂Measure.pi μ) -
b (finsetCoordProj B0 x))) := by
let P : Measure (∀ i, Ω i) := Measure.pi μ
let m : MeasurableSpace (∀ i, Ω i) :=
comap (finsetCoordProj (Ω := Ω) B0) MeasurableSpace.pi
let F : (∀ i, Ω i) → ℝ := fun x => f (finsetCoordProj B1 x)
let G : (∀ i, Ω i) → ℝ := fun x => g (finsetCoordProj B1 x)
let A : (∀ i, Ω i) → ℝ := fun x => a (finsetCoordProj B0 x)
let B : (∀ i, Ω i) → ℝ := fun x => b (finsetCoordProj B0 x)
have hle : m ≤ MeasurableSpace.pi := by
exact (measurable_finsetCoordProj (Ω := Ω) B0).comap_le
haveI : IsFiniteMeasure P := inferInstance
haveI : IsFiniteMeasure (P.trim hle) := isFiniteMeasure_trim hle
have hA : StronglyMeasurable[m] A := by
have hp : Measurable[m] (finsetCoordProj (Ω := Ω) B0) :=
measurable_iff_comap_le.mpr le_rfl
exact (hameas.comp hp).stronglyMeasurable
have hB : StronglyMeasurable[m] B := by
have hp : Measurable[m] (finsetCoordProj (Ω := Ω) B0) :=
measurable_iff_comap_le.mpr le_rfl
exact (hbmeas.comp hp).stronglyMeasurable
have hfg' : Integrable (F * G) P := hfg
have hFint : (ofFinite ι) = (inferInstance : Fintype ι) :=
Subsingleton.elim _ _
have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = P :=
congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hFint
have hfb : Integrable (F * B) P := by
have hi := (indepFun_pi_of_disjoint (Ω := Ω) μ hdisj.symm).comp hfmeas hbmeas
have hi' : IndepFun F B P := by
change IndepFun (fun x : ∀ i, Ω i => f (fun i => x i.val))
(fun x : ∀ i, Ω i => b (fun i => x i.val)) P
simpa only [hpi, Function.comp_def] using hi
exact hi'.integrable_mul hf hb
have hag : Integrable (A * G) P := by
have hi := (indepFun_pi_of_disjoint (Ω := Ω) μ hdisj).comp hameas hgmeas
have hi' : IndepFun A G P := by
change IndepFun (fun x : ∀ i, Ω i => a (fun i => x i.val))
(fun x : ∀ i, Ω i => g (fun i => x i.val)) P
simpa only [hpi, Function.comp_def] using hi
exact hi'.integrable_mul ha hg
have hshift : Integrable ((F - A) * (G - B)) P := hflp.integrable_mul hglp
have hab : Integrable (A * B) P := by
have heq : A * B = ((F - A) * (G - B)) - (F * G) + (F * B) + (A * G) := by
funext x
simp only [Pi.mul_apply, Pi.sub_apply, Pi.add_apply]
ring
rw [heq]
exact ((hshift.sub hfg').add hfb).add hag
have hcov : covariance F G P = (∫ x, F x * G x ∂P) - (∫ x, F x ∂P) * (∫ x, G x ∂P) := by
simp_rw [covariance, sub_mul, mul_sub]
repeat rw [integral_sub]
· simp_rw [integral_mul_const, integral_const_mul, integral_const,
probReal_univ, one_smul]
ring
· exact hg.const_mul _
· exact integrable_const _
· exact hfg'
· exact hf.mul_const _
· exact (hfg'.sub (hf.mul_const _))
· exact (hg.const_mul _).sub (integrable_const _)
have hcross := condExp_heldoutBlock_eq_integral μ B0 B1 hdisj
(fun z => f z * g z) (hfmeas.mul hgmeas)
have hF := condExp_heldoutBlock_eq_integral μ B0 B1 hdisj f hfmeas
have hG := condExp_heldoutBlock_eq_integral μ B0 B1 hdisj g hgmeas
have hAB : condExp m P (A * B) =ᵐ[P] A * B := by
rw [condExp_of_stronglyMeasurable hle (hA.mul hB) hab]
have hFB : condExp m P (F * B) =ᵐ[P] (fun x => (∫ y, F y ∂P) * B x) := by
filter_upwards [condExp_mul_of_stronglyMeasurable_right hB hfb hf, hF]
with x hx hy
simpa only [Pi.mul_apply] using hx.trans (congrArg (fun z : ℝ => z * B x) hy)
have hAG : condExp m P (A * G) =ᵐ[P] (fun x => A x * (∫ y, G y ∂P)) := by
filter_upwards [condExp_mul_of_stronglyMeasurable_left hA hag hg, hG]
with x hx hy
simpa only [Pi.mul_apply] using hx.trans (congrArg (fun z : ℝ => A x * z) hy)
have hexpand : (F - A) * (G - B) = F * G - F * B - A * G + A * B := by
funext x
simp only [Pi.mul_apply, Pi.sub_apply, Pi.add_apply]
ring
change condExp m P ((F - A) * (G - B)) =ᵐ[P]
(fun x => covariance F G P + ((∫ y, F y ∂P) - A x) * ((∫ y, G y ∂P) - B x))
rw [hexpand]
have hlin : condExp m P (F * G - F * B - A * G + A * B) =ᵐ[P]
condExp m P (F * G) - condExp m P (F * B) -
condExp m P (A * G) + condExp m P (A * B) := by
have h1 := condExp_sub hfg' hfb m
have h2 := condExp_sub (hfg'.sub hfb) hag m
have h3 := condExp_add ((hfg'.sub hfb).sub hag) hab m
filter_upwards [h1, h2, h3] with x hx1 hx2 hx3
simp only [Pi.add_apply, Pi.sub_apply] at *
rw [hx3, hx2, hx1]
filter_upwards [hlin, hcross, hFB, hAG, hAB] with x hx hc hfbx hagx habx
simp only [Pi.sub_apply, Pi.add_apply] at hx
have hc' : condExp m P (F * G) x = ∫ y, F y * G y ∂P := hc
rw [hx, hc', hfbx, hagx, habx, hcov]
simp only [Pi.mul_apply]
ring
ShiftedBlockMoments 1 core · 1 supporting A score on a held-out coordinate block has constant conditional mean given a disjoint training block. ★ condExp_shiftedBlock_eq_integral_sub
Conditional moments of a training-shifted held-out block
A score on a held-out coordinate block has constant conditional mean given a disjoint training block. Subtracting a measurable training-block shift subtracts that shift from the conditional mean.
theorem condExp_shiftedBlock_eq_integral_sub reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
A finite product probability law, a disjoint training and held-out block, a held-out score and training shift with measurability and integrability imply that the conditional mean of their difference given the training block is almost surely the unconditional held-out mean minus the same training shift.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
μ :
(i : ι) → Measure (Ω i)
∀ i, IsProbabilityMeasure (μ i)
B0 B1 :
Finset ι
hdisj :
Disjoint B0 B1
f :
((i : {i // i ∈ B1}) → Ω i.val) → ℝ
a :
((i : {i // i ∈ B0}) → Ω i.val) → ℝ
hfmeas :
hameas :
hf :
Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x)) (Measure.pi μ)
ha :
Integrable (fun x : ∀ i, Ω i => a (finsetCoordProj B0 x)) (Measure.pi μ)
conclusion
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x))
=ᵐ[Measure.pi μ] (fun x => (∫ y : (∀ i, Ω i), f (finsetCoordProj B1 y) ∂Measure.pi μ) - a (finsetCoordProj B0 x))
Proof (Lean source)
theorem condExp_shiftedBlock_eq_integral_sub
(μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)]
(B0 B1 : Finset ι) (hdisj : Disjoint B0 B1)
(f : ((i : {i // i ∈ B1}) → Ω i.val) → ℝ)
(a : ((i : {i // i ∈ B0}) → Ω i.val) → ℝ)
(hfmeas : Measurable f) (hameas : Measurable a)
(hf : Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x))
(Measure.pi μ))
(ha : Integrable (fun x : ∀ i, Ω i => a (finsetCoordProj B0 x))
(Measure.pi μ)) :
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ)
(fun x : ∀ i, Ω i => f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x))
=ᵐ[Measure.pi μ]
(fun x => (∫ y : (∀ i, Ω i), f (finsetCoordProj B1 y) ∂Measure.pi μ) -
a (finsetCoordProj B0 x)) := by
have hle := (measurable_finsetCoordProj (Ω := Ω) B0).comap_le
haveI : IsFiniteMeasure (Measure.pi μ) := inferInstance
haveI : IsFiniteMeasure ((Measure.pi μ).trim hle) := isFiniteMeasure_trim hle
have hsm : StronglyMeasurable[comap
(finsetCoordProj (Ω := Ω) B0) inferInstance]
(fun x : ∀ i, Ω i => a (finsetCoordProj B0 x)) := by
have hp : Measurable[comap
(finsetCoordProj (Ω := Ω) B0) inferInstance]
(finsetCoordProj (Ω := Ω) B0) := measurable_iff_comap_le.mpr le_rfl
exact (hameas.comp hp).stronglyMeasurable
have hshift := condExp_of_stronglyMeasurable hle hsm ha
have hfirst := condExp_heldoutBlock_eq_integral μ B0 B1 hdisj f hfmeas
refine (condExp_sub hf ha _).trans ?_
rw [hshift]
filter_upwards [hfirst] with x hx
exact congrArg (fun z : ℝ => z - a (finsetCoordProj B0 x)) hx
1 supporting declaration (lemmas, instances)
-
condExp_heldoutBlock_eq_integraltheorem — A finite product probability law, a training block and held-out block with disjointness, a measurable score imply that its conditional mean given the training block is its unconditional mean.hypothesesι :sharedType u_1ι → Type u_2μ :(i : ι) → Measure (Ω i)∀ i, IsProbabilityMeasure (μ i)B0 B1 :Finset ιhdisj :Disjoint B0 B1f :((i : {i // i ∈ B1}) → Ω i.val) → ℝhfmeas :conclusioncondExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x))=ᵐ[Measure.pi μ] (fun _ => ∫ x : (∀ i, Ω i), f (finsetCoordProj B1 x) ∂Measure.pi μ)Proof (Lean source)
theorem condExp_heldoutBlock_eq_integral (μ : (i : ι) → Measure (Ω i)) [∀ i, IsProbabilityMeasure (μ i)] (B0 B1 : Finset ι) (hdisj : Disjoint B0 B1) (f : ((i : {i // i ∈ B1}) → Ω i.val) → ℝ) (hfmeas : Measurable f) : condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x)) =ᵐ[Measure.pi μ] (fun _ => ∫ x : (∀ i, Ω i), f (finsetCoordProj B1 x) ∂Measure.pi μ) := by have hproj := indepFun_pi_of_disjoint (Ω := Ω) μ hdisj.symm have hF : (ofFinite ι) = (inferInstance : Fintype ι) := Subsingleton.elim _ _ have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = Measure.pi μ := congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hF have hindep : IndepFun (finsetCoordProj (Ω := Ω) B1) (finsetCoordProj (Ω := Ω) B0) (Measure.pi μ) := by change IndepFun (fun x : ∀ i, Ω i => fun i : {i // i ∈ B1} => x i.val) (fun x : ∀ i, Ω i => fun i : {i // i ∈ B0} => x i.val) (Measure.pi μ) simpa only [hpi] using hproj have hmeas : Measurable (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x)) := hfmeas.comp (measurable_finsetCoordProj B1) have hle₁ := (measurable_finsetCoordProj (Ω := Ω) B1).comap_le have hle₂ := (measurable_finsetCoordProj (Ω := Ω) B0).comap_le haveI : IsFiniteMeasure (Measure.pi μ) := inferInstance haveI : IsFiniteMeasure ((Measure.pi μ).trim hle₂) := isFiniteMeasure_trim hle₂ have hsm : StronglyMeasurable[comap (finsetCoordProj (Ω := Ω) B1) inferInstance] (fun x : ∀ i, Ω i => f (finsetCoordProj B1 x)) := by have hp : Measurable[comap (finsetCoordProj (Ω := Ω) B1) inferInstance] (finsetCoordProj (Ω := Ω) B1) := measurable_iff_comap_le.mpr le_rfl exact (hfmeas.comp hp).stronglyMeasurable exact condExp_indep_eq hle₁ hle₂ hsm ((IndepFun_iff_Indep _ _ _).mp hindep)
ShiftedJoinedScore 2 core · 1 supporting A shifted held-out score is represented as a measurable score on the union of the training coordinates and its held-out block. ★ measurable_shiftedJoinedScore
Shifted scores on joined training and evaluation blocks
A shifted held-out score is represented as a measurable score on the union of the training coordinates and its held-out block. This representation connects shifted products to joined-view conditional factorization.
def shiftedJoinedScore reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
The training block, one evaluation block, a held-out score, and a training-block shift define the shifted score on their joined coordinate view, by subtracting the training shift from the held-out score.
Definition (Lean source)
parameters
ι :
Type u_1
ι → Type u_2
B0 B1 :
Finset ι
f :
((i : {i // i ∈ B1}) → Ω i.val) → ℝ
a :
((i : {i // i ∈ B0}) → Ω i.val) → ℝ
def
shiftedJoinedScore B0 B1 f a :
((i : {i // i ∈ B0 ∪ B1}) → Ω i.val) → ℝ
theorem measurable_shiftedJoinedScore reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
The training block and evaluation block, a held-out score, a training-block shift, and measurability of both functions imply that the joined shifted score is measurable.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
B0 B1 :
Finset ι
f :
((i : {i // i ∈ B1}) → Ω i.val) → ℝ
a :
((i : {i // i ∈ B0}) → Ω i.val) → ℝ
hf :
ha :
conclusion
Measurable (shiftedJoinedScore B0 B1 f a)
Proof (Lean source)
@[fun_prop] theorem measurable_shiftedJoinedScore (B0 B1 : Finset ι)
(f : ((i : {i // i ∈ B1}) → Ω i.val) → ℝ)
(a : ((i : {i // i ∈ B0}) → Ω i.val) → ℝ)
(hf : Measurable f) (ha : Measurable a) :
Measurable (shiftedJoinedScore B0 B1 f a) := by
unfold shiftedJoinedScore
apply Measurable.sub
· exact hf.comp (measurable_pi_lambda _ (fun _ => measurable_pi_apply _))
· exact ha.comp (measurable_pi_lambda _ (fun _ => measurable_pi_apply _))
1 supporting declaration (lemmas, instances)
-
shiftedJoinedScore_comp_projtheorem — The training block and evaluation block, a held-out score, a training-block shift, and a full product point imply that evaluating the joined shifted score equals the held-out score minus its training shift.hypothesesι :sharedType u_1ι → Type u_2B0 B1 :Finset ιf :((i : {i // i ∈ B1}) → Ω i.val) → ℝa :((i : {i // i ∈ B0}) → Ω i.val) → ℝx :∀ i, Ω iconclusionshiftedJoinedScore B0 B1 f a (finsetCoordProj (B0 ∪ B1) x)= f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x)Proof (Lean source)
theorem shiftedJoinedScore_comp_proj (B0 B1 : Finset ι) (f : ((i : {i // i ∈ B1}) → Ω i.val) → ℝ) (a : ((i : {i // i ∈ B0}) → Ω i.val) → ℝ) (x : ∀ i, Ω i) : shiftedJoinedScore B0 B1 f a (finsetCoordProj (B0 ∪ B1) x) = f (finsetCoordProj B1 x) - a (finsetCoordProj B0 x) := rfl
ThreeBlockDensity 1 core · 0 supporting This module turns a density whose first two coordinate blocks factor through a third, conditioning block into CondIndepFun for the first two coordinate maps given the third coordinate. ★ condIndepFun_threeBlock_of_density_factors
Conditional independence from a three-block product density
This module turns a density whose first two coordinate blocks factor through a
third, conditioning block into CondIndepFun for the first two coordinate maps
given the third coordinate. It is the reverse direction of the density-factorization
characterization DensityIntersection.condIndepFun_threeBlock_iff_factors, stated in plain
product coordinates.
theorem condIndepFun_threeBlock_of_density_factors reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
On a product of three standard Borel spaces, take three σ-finite coordinate reference measures and a measurable joint density with respect to their product whose induced measure is finite. Suppose there are first and second block factors, both measurable, such that almost everywhere the density equals the first factor evaluated at the first and third coordinates times the second factor evaluated at the second and third coordinates. Then, under the finite density measure, the first and second coordinate maps are conditionally independent given the third coordinate.
Formal statement
hypotheses
Y :
Type uY
Z :
Type uZ
C :
Type uC
muY :
Measure Y
muZ :
Measure Z
muC :
Measure C
SigmaFinite muY
SigmaFinite muZ
SigmaFinite muC
d :
Y × (Z × C) → ℝ≥0∞
hd :
IsFiniteMeasure ((muY.prod (muZ.prod muC)).withDensity d)
a :
Y × C → ℝ≥0∞
b :
Z × C → ℝ≥0∞
ha :
hb :
hfactor :
d =ᵐ[muY.prod (muZ.prod muC)] (fun q ↦ a (q.1, q.2.2) * b (q.2.1, q.2.2))
conclusion
CondIndepFun (comap (fun q : Y × (Z × C) ↦ q.2.2) inferInstance) ((measurable_snd.comp measurable_snd : Measurable (fun q : Y × (Z × C) ↦ q.2.2)).comap_le) (fun q : Y × (Z × C) ↦ q.1) (fun q : Y × (Z × C) ↦ q.2.1) ((muY.prod (muZ.prod muC)).withDensity d)
Proof (Lean source)
theorem condIndepFun_threeBlock_of_density_factors
(muY : Measure Y) (muZ : Measure Z) (muC : Measure C)
[SigmaFinite muY] [SigmaFinite muZ] [SigmaFinite muC]
{d : Y × (Z × C) → ℝ≥0∞} (hd : Measurable d)
[IsFiniteMeasure ((muY.prod (muZ.prod muC)).withDensity d)]
(a : Y × C → ℝ≥0∞) (b : Z × C → ℝ≥0∞)
(ha : Measurable a) (hb : Measurable b)
(hfactor : d =ᵐ[muY.prod (muZ.prod muC)]
(fun q ↦ a (q.1, q.2.2) * b (q.2.1, q.2.2))) :
CondIndepFun
(comap (fun q : Y × (Z × C) ↦ q.2.2) inferInstance)
((measurable_snd.comp measurable_snd :
Measurable (fun q : Y × (Z × C) ↦ q.2.2)).comap_le)
(fun q : Y × (Z × C) ↦ q.1)
(fun q : Y × (Z × C) ↦ q.2.1)
((muY.prod (muZ.prod muC)).withDensity d) := by
haveI : IsFiniteMeasure
((DensityIntersection.threeBlockReference muY muZ muC).withDensity d) :=
‹IsFiniteMeasure ((muY.prod (muZ.prod muC)).withDensity d)›
exact (DensityIntersection.condIndepFun_threeBlock_iff_factors muY muZ muC hd).2
⟨a, b, ha, hb, hfactor⟩
ThreeBlockProduct 4 core · 7 supporting This module packages conditional independence, moment bounds, factorization, centering, and covariance identities for products of scores evaluated on three pairwise-disjoint coordinate blocks of a finite product experime ★ condExp_threeBlockCross★ condExp_threeBlockProduct_zero★ condCov_threeBlockProduct
Conditional products on three held-out blocks
This module packages conditional independence, moment bounds, factorization, centering, and covariance identities for products of scores evaluated on three pairwise-disjoint coordinate blocks of a finite product experiment, conditional on a fourth training block. It is built from the library's binary conditional independence and conditional-expectation factorization interfaces.
def threeBlockProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
For three coordinate blocks and one score on each block, the three-block product score is given by evaluating each score on its block and multiplying the three values.
Definition (Lean source)
parameters
ι :
Type u_1
ι → Type u_2
η :
(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ
def
threeBlockProduct B η :
(∀ i, Ω i) → ℝ
given by
fun x => ∏ t : Fin 3, η t (finsetCoordProj (B t) x)
theorem condExp_threeBlockCross reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Under a finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness, pairwise evaluation disjointness, measurable left and right scores, and square-integrability of every block score, the conditional mean given the training block of the product of the two three-block products is almost surely the product, over the three blocks, of the conditional means given the training block of the blockwise left-times-right scores.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
B0 :
Finset ι
htrain :
∀ t, Disjoint B0 (B t)
η ζ :
(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ
hηmeas :
∀ t, Measurable (η t)
hζmeas :
∀ t, Measurable (ζ t)
hη :
∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)
hζ :
∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)
conclusion
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x => threeBlockProduct B η x * threeBlockProduct B ζ x)
=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B t) y) * ζ t (finsetCoordProj (B t) y)) x)
Proof (Lean source)
theorem condExp_threeBlockCross
(B0 : Finset ι) (B : Fin 3 → Finset ι)
(htrain : ∀ t, Disjoint B0 (B t))
(heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)))
(η ζ : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ)
(hηmeas : ∀ t, Measurable (η t)) (hζmeas : ∀ t, Measurable (ζ t))
(hη : ∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
2 (Measure.pi μ))
(hζ : ∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x))
2 (Measure.pi μ)) :
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun x => threeBlockProduct B η x * threeBlockProduct B ζ x)
=ᵐ[Measure.pi μ]
(fun x => ∏ t : Fin 3,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun y : ∀ i, Ω i =>
η t (finsetCoordProj (B t) y) * ζ t (finsetCoordProj (B t) y)) x) := by
classical
let ξ (t : Fin 3) : ((i : {i // i ∈ B t}) → Ω i.val) → ℝ :=
fun z => η t z * ζ t z
have hξmeas (t : Fin 3) : Measurable (ξ t) :=
(hηmeas t).mul (hζmeas t)
have hξ (t : Fin 3) : Integrable
(fun x : ∀ i, Ω i => ξ t (finsetCoordProj (B t) x)) (Measure.pi μ) :=
(hη t).integrable_mul (hζ t)
have hξ01 : Integrable (fun x : ∀ i, Ω i =>
ξ 0 (finsetCoordProj (B 0) x) * ξ 1 (finsetCoordProj (B 1) x))
(Measure.pi μ) :=
integrable_twoBlockProduct μ (B 0) (B 1)
(heval (by decide : (0 : Fin 3) ≠ 1))
(ξ 0) (ξ 1) (hξmeas 0) (hξmeas 1) (hξ 0) (hξ 1)
have hξprod : Integrable (threeBlockProduct B ξ) (Measure.pi μ) := by
convert integrable_threeBlockCross μ B heval η ζ hηmeas hζmeas hη hζ using 1
ext x
simp only [threeBlockProduct, Fin.prod_univ_three]
dsimp [ξ]
ring
have hfactor := condExp_threeBlockProduct_of_integrable μ B0 B htrain heval
ξ hξmeas hξ hξ01 hξprod
have hfun : threeBlockProduct B ξ =
(fun x => threeBlockProduct B η x * threeBlockProduct B ζ x) := by
funext x
simp only [threeBlockProduct, Fin.prod_univ_three]
dsimp [ξ]
ring
rw [hfun] at hfactor
simpa only [ξ] using hfactor
theorem condExp_threeBlockProduct_zero reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Under a finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness, pairwise evaluation disjointness, measurable square-integrable block scores, and zero conditional mean of every block score given the training block, the conditional mean of their three-block product given the training block is almost surely zero.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
B0 :
Finset ι
htrain :
∀ t, Disjoint B0 (B t)
η :
(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ
hηmeas :
∀ t, Measurable (η t)
hη :
∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)
hcenter :
∀ t,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)
conclusion
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)
Proof (Lean source)
theorem condExp_threeBlockProduct_zero
(B0 : Finset ι) (B : Fin 3 → Finset ι)
(htrain : ∀ t, Disjoint B0 (B t))
(heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)))
(η : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ)
(hηmeas : ∀ t, Measurable (η t))
(hη : ∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
2 (Measure.pi μ))
(hcenter : ∀ t, condExp
(comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)) :
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (threeBlockProduct B η)
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ) := by
classical
have hηint (t : Fin 3) : Integrable
(fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) (Measure.pi μ) :=
(hη t).integrable (by norm_num)
have hη01 : Integrable (fun x : ∀ i, Ω i =>
η 0 (finsetCoordProj (B 0) x) * η 1 (finsetCoordProj (B 1) x))
(Measure.pi μ) :=
integrable_twoBlockProduct μ (B 0) (B 1)
(heval (by decide : (0 : Fin 3) ≠ 1))
(η 0) (η 1) (hηmeas 0) (hηmeas 1) (hηint 0) (hηint 1)
have hηprod : Integrable (threeBlockProduct B η) (Measure.pi μ) :=
(memLp_threeBlockProduct μ B heval η hηmeas hη).integrable (by norm_num)
have hfactor := condExp_threeBlockProduct_of_integrable μ B0 B htrain heval
η hηmeas hηint hη01 hηprod
filter_upwards [hfactor, hcenter 0, hcenter 1, hcenter 2] with x hx h0 h1 h2
simpa [Fin.prod_univ_three, h0, h1, h2] using hx
theorem condCov_threeBlockProduct reviewed
⚑ flagged
Causalean.Mathlib.Probability.Independence.Conditional
Under a finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness, pairwise evaluation disjointness, measurable square-integrable left and right block scores, and zero conditional mean of every left and right block score given the training block, the conditional covariance of the two three-block products given the training block is almost surely the product, over the three blocks, of the conditional means given the training block of the blockwise left-times-right scores.
Formal statement
hypotheses
ι :
Type u_1
ι → Type u_2
B0 :
Finset ι
htrain :
∀ t, Disjoint B0 (B t)
η ζ :
(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ
hηmeas :
∀ t, Measurable (η t)
hζmeas :
∀ t, Measurable (ζ t)
hη :
∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)
hζ :
∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)
hηcenter :
∀ t,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)
hζcenter :
∀ t,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)
conclusion
(fun x => condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y => threeBlockProduct B η y * threeBlockProduct B ζ y) x - condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (threeBlockProduct B η) x * condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (threeBlockProduct B ζ) x)
=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B t) y) * ζ t (finsetCoordProj (B t) y)) x)
Proof (Lean source)
theorem condCov_threeBlockProduct
(B0 : Finset ι) (B : Fin 3 → Finset ι)
(htrain : ∀ t, Disjoint B0 (B t))
(heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)))
(η ζ : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ)
(hηmeas : ∀ t, Measurable (η t)) (hζmeas : ∀ t, Measurable (ζ t))
(hη : ∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
2 (Measure.pi μ))
(hζ : ∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x))
2 (Measure.pi μ))
(hηcenter : ∀ t, condExp
(comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ))
(hζcenter : ∀ t, condExp
(comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x))
=ᵐ[Measure.pi μ] (0 : (∀ i, Ω i) → ℝ)) :
(fun x =>
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun y => threeBlockProduct B η y * threeBlockProduct B ζ y) x -
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (threeBlockProduct B η) x *
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (threeBlockProduct B ζ) x)
=ᵐ[Measure.pi μ]
(fun x => ∏ t : Fin 3,
condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance)
(Measure.pi μ) (fun y : ∀ i, Ω i =>
η t (finsetCoordProj (B t) y) * ζ t (finsetCoordProj (B t) y)) x) := by
have hcross := condExp_threeBlockCross μ B0 B htrain heval η ζ
hηmeas hζmeas hη hζ
have hηzero := condExp_threeBlockProduct_zero μ B0 B htrain heval η
hηmeas hη hηcenter
have hζzero := condExp_threeBlockProduct_zero μ B0 B htrain heval ζ
hζmeas hζ hζcenter
filter_upwards [hcross, hηzero, hζzero] with x hx hηx hζx
simpa [hηx, hζx] using hx
7 supporting declarations (lemmas, instances)
-
condIndepFun_eval_pairtheorem — For a finite product probability law, a training block and three evaluation blocks whose training and evaluation blocks are disjoint and whose evaluation blocks are pairwise disjoint, the views indexed by two distinct evaluation blocks satisfy conditional independence given the training view.hypothesesι :sharedType u_1ι → Type u_2B0 :Finset ιhtrain :∀ t, Disjoint B0 (B t)s t :Fin 3hst :s ≠ tconclusionCondIndepFun (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) B0)) (finsetCoordProj (Ω := Ω) (B s)) (finsetCoordProj (Ω := Ω) (B t)) (Measure.pi μ)Proof (Lean source)
theorem condIndepFun_eval_pair (B0 : Finset ι) (B : Fin 3 → Finset ι) (htrain : ∀ t, Disjoint B0 (B t)) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (s t : Fin 3) (hst : s ≠ t) : CondIndepFun (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) B0)) (finsetCoordProj (Ω := Ω) (B s)) (finsetCoordProj (Ω := Ω) (B t)) (Measure.pi μ) := by classical have _htrain := htrain have hinter : B s ∩ B t ⊆ B0 := by rw [Finset.disjoint_iff_inter_eq_empty.mp (heval hst)] exact empty_subset B0 have h := condIndepFun_pi_of_inter_subset (Ω := Ω) μ hinter have hF : (ofFinite ι) = (inferInstance : Fintype ι) := Subsingleton.elim _ _ have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = Measure.pi μ := congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hF simpa only [hpi] using h -
condIndepFun_eval_uniontheorem — For a finite product probability law, a training block and three evaluation blocks whose training and evaluation blocks are disjoint and whose evaluation blocks are pairwise disjoint, the combined first two evaluation views are conditionally independent of the third given the training view.hypothesesconclusionCondIndepFun (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) B0)) (finsetCoordProj (Ω := Ω) (B 0 ∪ B 1)) (finsetCoordProj (Ω := Ω) (B 2)) (Measure.pi μ)Proof (Lean source)
theorem condIndepFun_eval_union (B0 : Finset ι) (B : Fin 3 → Finset ι) [DecidableEq ι] (htrain : ∀ t, Disjoint B0 (B t)) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) : CondIndepFun (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (comap_le (measurable_finsetCoordProj (Ω := Ω) B0)) (finsetCoordProj (Ω := Ω) (B 0 ∪ B 1)) (finsetCoordProj (Ω := Ω) (B 2)) (Measure.pi μ) := by classical have _htrain := htrain have hdisj : Disjoint (B 0 ∪ B 1) (B 2) := Finset.disjoint_union_left.mpr ⟨heval (by decide : (0 : Fin 3) ≠ 2), heval (by decide : (1 : Fin 3) ≠ 2)⟩ have hinter : (B 0 ∪ B 1) ∩ B 2 ⊆ B0 := by rw [Finset.disjoint_iff_inter_eq_empty.mp hdisj] exact empty_subset B0 have h := condIndepFun_pi_of_inter_subset (Ω := Ω) μ hinter have hF : (ofFinite ι) = (inferInstance : Fintype ι) := Subsingleton.elim _ _ have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = Measure.pi μ := congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hF simpa only [hpi] using h -
integrable_twoBlockProducttheorem — Under a finite product probability law, two coordinate blocks with disjointness, two block scores, their measurability, and integrability after pullback to the full experiment, the product of the pulled-back scores is integrable.hypothesesι :sharedType u_1ι → Type u_2S T :Finset ιhST :Disjoint S Tf :((i : {i // i ∈ S}) → Ω i.val) → ℝg :((i : {i // i ∈ T}) → Ω i.val) → ℝhfmeas :hgmeas :hf :Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj S x)) (Measure.pi μ)hg :Integrable (fun x : ∀ i, Ω i => g (finsetCoordProj T x)) (Measure.pi μ)conclusionProof (Lean source)
theorem integrable_twoBlockProduct (S T : Finset ι) (hST : Disjoint S T) (f : ((i : {i // i ∈ S}) → Ω i.val) → ℝ) (g : ((i : {i // i ∈ T}) → Ω i.val) → ℝ) (hfmeas : Measurable f) (hgmeas : Measurable g) (hf : Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj S x)) (Measure.pi μ)) (hg : Integrable (fun x : ∀ i, Ω i => g (finsetCoordProj T x)) (Measure.pi μ)) : Integrable (fun x : ∀ i, Ω i => f (finsetCoordProj S x) * g (finsetCoordProj T x)) (Measure.pi μ) := by have h := (indepFun_pi_of_disjoint (Ω := Ω) μ hST).comp hfmeas hgmeas have hF : (ofFinite ι) = (inferInstance : Fintype ι) := Subsingleton.elim _ _ have hpi : @Measure.pi ι Ω (ofFinite ι) _ μ = Measure.pi μ := congrArg (fun fi : Fintype ι => @Measure.pi ι Ω fi _ μ) hF have hi : IndepFun (fun x : ∀ i, Ω i => f (finsetCoordProj S x)) (fun x : ∀ i, Ω i => g (finsetCoordProj T x)) (Measure.pi μ) := by change IndepFun (fun x : ∀ i, Ω i => f (fun i => x i.val)) (fun x : ∀ i, Ω i => g (fun i => x i.val)) (Measure.pi μ) simpa only [hpi, Function.comp_def] using h exact hi.integrable_mul hf hg -
memLp_threeBlockProducttheorem — Under a finite product probability law, three pairwise-disjoint coordinate blocks, measurable block scores, and square-integrability of their pullbacks, the three-block product is square-integrable.hypothesesι :sharedType u_1ι → Type u_2η :(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝhηmeas :∀ t, Measurable (η t)hη :∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)conclusionMemLp (threeBlockProduct B η) 2 (Measure.pi μ)Proof (Lean source)
theorem memLp_threeBlockProduct (B : Fin 3 → Finset ι) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (η : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ) (hηmeas : ∀ t, Measurable (η t)) (hη : ∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)) : MemLp (threeBlockProduct B η) 2 (Measure.pi μ) := by classical let X (t : Fin 3) : (∀ i, Ω i) → ℝ := fun x => η t (finsetCoordProj (B t) x) have hXmeas (t : Fin 3) : Measurable (X t) := (hηmeas t).comp (measurable_finsetCoordProj (B t)) have hsq (t : Fin 3) : Integrable (fun x => (X t x) ^ 2) (Measure.pi μ) := (hη t).integrable_sq have h01 : Integrable (fun x => (X 0 x) ^ 2 * (X 1 x) ^ 2) (Measure.pi μ) := integrable_twoBlockProduct μ (B 0) (B 1) (heval (by decide : (0 : Fin 3) ≠ 1)) (fun y => (η 0 y) ^ 2) (fun y => (η 1 y) ^ 2) ((hηmeas 0).pow_const 2) ((hηmeas 1).pow_const 2) (hsq 0) (hsq 1) let F : ((i : {i // i ∈ B 0 ∪ B 1}) → Ω i.val) → ℝ := fun y => (η 0 (fun i => y ⟨i.val, Finset.mem_union.mpr (inl i.property)⟩)) ^ 2 * (η 1 (fun i => y ⟨i.val, Finset.mem_union.mpr (inr i.property)⟩)) ^ 2 have hFmeas : Measurable F := by dsimp [F] apply mul · apply Measurable.pow_const exact (hηmeas 0).comp (measurable_pi_lambda _ (fun i => measurable_pi_apply _)) · apply Measurable.pow_const exact (hηmeas 1).comp (measurable_pi_lambda _ (fun i => measurable_pi_apply _)) have hdisj : Disjoint (B 0 ∪ B 1) (B 2) := Finset.disjoint_union_left.mpr ⟨heval (by decide : (0 : Fin 3) ≠ 2), heval (by decide : (1 : Fin 3) ≠ 2)⟩ have hFint : Integrable (fun x => F (finsetCoordProj (B 0 ∪ B 1) x)) (Measure.pi μ) := by convert h01 using 1 ext x rfl have hprod : Integrable (fun x => F (finsetCoordProj (B 0 ∪ B 1) x) * (X 2 x) ^ 2) (Measure.pi μ) := integrable_twoBlockProduct μ (B 0 ∪ B 1) (B 2) hdisj F (fun y => (η 2 y) ^ 2) hFmeas ((hηmeas 2).pow_const 2) hFint (hsq 2) apply (memLp_two_iff_integrable_sq ?_).2 · convert hprod using 1 ext x simp only [threeBlockProduct, Fin.prod_univ_three, mul_pow] change (X 0 x) ^ 2 * (X 1 x) ^ 2 * (X 2 x) ^ 2 = (X 0 x) ^ 2 * (X 1 x) ^ 2 * (X 2 x) ^ 2 rfl · exact (Finset.measurable_prod _ (fun t _ => hXmeas t)).aestronglyMeasurable -
integrable_threeBlockCrosstheorem — Under a finite product probability law, three pairwise-disjoint coordinate blocks, two families of measurable block scores, and square-integrability of every pulled-back score, the product of the two three-block products is integrable.hypothesesι :sharedType u_1ι → Type u_2η ζ :(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝhηmeas :∀ t, Measurable (η t)hζmeas :∀ t, Measurable (ζ t)hη :∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)hζ :∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)conclusionProof (Lean source)
theorem integrable_threeBlockCross (B : Fin 3 → Finset ι) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (η ζ : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ) (hηmeas : ∀ t, Measurable (η t)) (hζmeas : ∀ t, Measurable (ζ t)) (hη : ∀ t, MemLp (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)) (hζ : ∀ t, MemLp (fun x : ∀ i, Ω i => ζ t (finsetCoordProj (B t) x)) 2 (Measure.pi μ)) : Integrable (fun x : ∀ i, Ω i => threeBlockProduct B η x * threeBlockProduct B ζ x) (Measure.pi μ) := by exact (memLp_threeBlockProduct μ B heval η hηmeas hη).integrable_mul (memLp_threeBlockProduct μ B heval ζ hζmeas hζ) -
condExp_threeBlockProduct_of_integrabletheorem — Under a finite product probability law, a training block and three evaluation blocks with training/evaluation disjointness, pairwise evaluation disjointness, measurable block scores, integrable individual scores, an integrable product over the first two blocks, and an integrable three-block product, the conditional mean of the three-block product is the product of its three blockwise conditional means.hypothesesι :sharedType u_1ι → Type u_2B0 :Finset ιhtrain :∀ t, Disjoint B0 (B t)η :(t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝhηmeas :∀ t, Measurable (η t)hη :∀ t, Integrable (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) (Measure.pi μ)hη01 :Integrable (fun x : ∀ i, Ω i => η 0 (finsetCoordProj (B 0) x) * η 1 (finsetCoordProj (B 1) x)) (Measure.pi μ)hηprod :Integrable (threeBlockProduct B η) (Measure.pi μ)conclusion=ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B t) y)) x)Proof (Lean source)
theorem condExp_threeBlockProduct_of_integrable (B0 : Finset ι) (B : Fin 3 → Finset ι) (htrain : ∀ t, Disjoint B0 (B t)) (heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t))) (η : (t : Fin 3) → ((i : {i // i ∈ B t}) → Ω i.val) → ℝ) (hηmeas : ∀ t, Measurable (η t)) (hη : ∀ t, Integrable (fun x : ∀ i, Ω i => η t (finsetCoordProj (B t) x)) (Measure.pi μ)) (hη01 : Integrable (fun x : ∀ i, Ω i => η 0 (finsetCoordProj (B 0) x) * η 1 (finsetCoordProj (B 1) x)) (Measure.pi μ)) (hηprod : Integrable (threeBlockProduct B η) (Measure.pi μ)) : condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (threeBlockProduct B η) =ᵐ[Measure.pi μ] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := Ω) B0) inferInstance) (Measure.pi μ) (fun y : ∀ i, Ω i => η t (finsetCoordProj (B t) y)) x) := by classical have hm : comap (finsetCoordProj (Ω := Ω) B0) inferInstance ≤ (inferInstance : MeasurableSpace (∀ i, Ω i)) := comap_le (measurable_finsetCoordProj (Ω := Ω) B0) have h01 := condExp_mul_of_condIndep (μ := Measure.pi μ) hm (measurable_finsetCoordProj (Ω := Ω) (B 0)) (measurable_finsetCoordProj (Ω := Ω) (B 1)) (condIndepFun_eval_pair μ B0 B htrain heval 0 1 (by decide)) (hηmeas 0) (hηmeas 1) (hη 0) (hη 1) hη01 let F : ((i : {i // i ∈ B 0 ∪ B 1}) → Ω i.val) → ℝ := fun y => η 0 (fun i => y ⟨i.val, Finset.mem_union.mpr (inl i.property)⟩) * η 1 (fun i => y ⟨i.val, Finset.mem_union.mpr (inr i.property)⟩) have hFmeas : Measurable F := by dsimp [F] apply mul · exact (hηmeas 0).comp (measurable_pi_lambda _ (fun i => measurable_pi_apply _)) · exact (hηmeas 1).comp (measurable_pi_lambda _ (fun i => measurable_pi_apply _)) have hFint : Integrable (fun x => F (finsetCoordProj (B 0 ∪ B 1) x)) (Measure.pi μ) := by convert hη01 using 1 ext x rfl have hprod : Integrable (fun x => F (finsetCoordProj (B 0 ∪ B 1) x) * η 2 (finsetCoordProj (B 2) x)) (Measure.pi μ) := by convert hηprod using 1 ext x simp only [threeBlockProduct, Fin.prod_univ_three] rfl have hstep2 := condExp_mul_of_condIndep (μ := Measure.pi μ) hm (measurable_finsetCoordProj (Ω := Ω) (B 0 ∪ B 1)) (measurable_finsetCoordProj (Ω := Ω) (B 2)) (condIndepFun_eval_union μ B0 B htrain heval) hFmeas (hηmeas 2) hFint (hη 2) hprod have hfun : (fun x : ∀ i, Ω i => F (finsetCoordProj (B 0 ∪ B 1) x) * η 2 (finsetCoordProj (B 2) x)) = threeBlockProduct B η := by funext x simp only [threeBlockProduct, Fin.prod_univ_three] rfl have hfun01 : (fun x : ∀ i, Ω i => F (finsetCoordProj (B 0 ∪ B 1) x)) = (fun x => η 0 (finsetCoordProj (B 0) x) * η 1 (finsetCoordProj (B 1) x)) := by funext x rfl rw [hfun, hfun01] at hstep2 have hfinal := hstep2.trans (h01.mul (Filter.EventuallyEq.refl (ae (Measure.pi μ)) _)) filter_upwards [hfinal] with x hx simpa [Fin.prod_univ_three] using hx -
condExp_threeSingletonCrosstheorem — For a four-coordinate product probability law, left and right scores on the three held-out coordinates, their measurability, and square-integrability of their pullbacks, the conditional cross moment of their two three-coordinate products factors by coordinate.hypothesesX :ν :∀ i, IsProbabilityMeasure (ν i)η ζ :(t : Fin 3) → X t.succ → ℝhηmeas :∀ t, Measurable (η t)hζmeas :∀ t, Measurable (ζ t)hη :∀ t, MemLp (fun x : ∀ i, X i => η t (x t.succ)) 2 (Measure.pi ν)hζ :∀ t, MemLp (fun x : ∀ i, X i => ζ t (x t.succ)) 2 (Measure.pi ν)conclusioncondExp (comap (finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance) (Measure.pi ν) (fun x : ∀ i, X i => (∏ t : Fin 3, η t (x t.succ)) * (∏ t : Fin 3, ζ t (x t.succ)))=ᵐ[Measure.pi ν] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance) (Measure.pi ν) (fun y : ∀ i, X i => η t (y t.succ) * ζ t (y t.succ)) x)Proof (Lean source)
theorem condExp_threeSingletonCross {X : Fin 4 → Type*} [∀ i, MeasurableSpace (X i)] [∀ i, StandardBorelSpace (X i)] (ν : (i : Fin 4) → Measure (X i)) [∀ i, IsProbabilityMeasure (ν i)] (η ζ : (t : Fin 3) → X t.succ → ℝ) (hηmeas : ∀ t, Measurable (η t)) (hζmeas : ∀ t, Measurable (ζ t)) (hη : ∀ t, MemLp (fun x : ∀ i, X i => η t (x t.succ)) 2 (Measure.pi ν)) (hζ : ∀ t, MemLp (fun x : ∀ i, X i => ζ t (x t.succ)) 2 (Measure.pi ν)) : condExp (comap (finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance) (Measure.pi ν) (fun x : ∀ i, X i => (∏ t : Fin 3, η t (x t.succ)) * (∏ t : Fin 3, ζ t (x t.succ))) =ᵐ[Measure.pi ν] (fun x => ∏ t : Fin 3, condExp (comap (finsetCoordProj (Ω := X) ({0} : Finset (Fin 4))) inferInstance) (Measure.pi ν) (fun y : ∀ i, X i => η t (y t.succ) * ζ t (y t.succ)) x) := by classical let B : Fin 3 → Finset (Fin 4) := fun t => {t.succ} have htrain : ∀ t, Disjoint ({0} : Finset (Fin 4)) (B t) := by intro t simpa [B] using (Fin.succ_ne_zero t).symm have heval : Pairwise (fun s t : Fin 3 => Disjoint (B s) (B t)) := by intro s t hst simpa [B] using (Fin.succ_injective 3).ne hst let ξ : (t : Fin 3) → ((i : {i // i ∈ B t}) → X i.val) → ℝ := fun t z => η t (z ⟨t.succ, Finset.mem_singleton_self _⟩) let ψ : (t : Fin 3) → ((i : {i // i ∈ B t}) → X i.val) → ℝ := fun t z => ζ t (z ⟨t.succ, Finset.mem_singleton_self _⟩) have hξmeas (t : Fin 3) : Measurable (ξ t) := (hηmeas t).comp (measurable_pi_apply (⟨t.succ, Finset.mem_singleton_self _⟩ : {i // i ∈ B t})) have hψmeas (t : Fin 3) : Measurable (ψ t) := (hζmeas t).comp (measurable_pi_apply (⟨t.succ, Finset.mem_singleton_self _⟩ : {i // i ∈ B t})) have hξ (t : Fin 3) : MemLp (fun x : ∀ i, X i => ξ t (finsetCoordProj (B t) x)) 2 (Measure.pi ν) := by exact hη t have hψ (t : Fin 3) : MemLp (fun x : ∀ i, X i => ψ t (finsetCoordProj (B t) x)) 2 (Measure.pi ν) := by exact hζ t have h := condExp_threeBlockCross ν ({0} : Finset (Fin 4)) B htrain heval ξ ψ hξmeas hψmeas hξ hψ simpa only [threeBlockProduct, finsetCoordProj, ξ, ψ, B] using h