Mathlib.CondIndep
Conditional-independence infrastructure staged for Mathlib: kernels, factorization characterizations, and the graphoid-style calculus.
AELift 3 core · 3 supporting This file proves generic almost-everywhere equality and inequality lifting lemmas under overlap and conditional-independence hypotheses. ★ ae_eq_of_ae_eq_restrict_arm★ ae_le_YofA_of_ae_le_Y★ ae_le_YofA_of_ae_le_Y_below
Almost-Everywhere Lifts Under Overlap
This file proves generic almost-everywhere equality and inequality lifting lemmas under overlap and conditional-independence hypotheses. These tools transfer restricted-arm statements and essential bounds to global potential-outcome statements in partial-identification arguments.
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 theorems are
ae_eq_of_ae_eq_restrict_arm, ae_le_YofA_of_ae_le_Y, and
ae_le_YofA_of_ae_le_Y_below.
theorem ae_eq_of_ae_eq_restrict_arm reviewed
⚑ flagged
Causalean
Single-arm 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 the conditional probability of E given m is positive almost everywhere — every m-measurable set overlapping E only on a null set 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
theorem ae_le_YofA_of_ae_le_Y reviewed
⚑ flagged
Causalean
Y(a) inherits Y's a.e. upper bound under latent exchangeability and consistency. For a sub-σ-algebra σ_UX coarser than the ambient σ-algebra, a measurable treatment map A, a measurable potential outcome Ya, and a treatment value a, if Ya is conditionally independent of A given σ_UX — latent exchangeability, the observed outcome Y agrees with Ya almost everywhere on the restriction of the measure to the event {A = a} — consistency, the conditional probability of {A = a} given σ_UX is positive almost everywhere — overlap, and Y is at most M almost everywhere, then Ya is at most M almost everywhere as well.
Formal statement
hypotheses
Ω :
_hσUX :
σ_UX ≤ mΩ
α :
Y Ya :
Ω → ℝ
_hA :
@Measurable Ω α mΩ _ A
_hYa :
@Measurable Ω ℝ mΩ _ Ya
a :
α
_latent_exch :
CondIndepFun σ_UX _hσUX Ya A μ
_consistency :
Y =ᵐ[μ.restrict {ω | A ω = a}] Ya
_h_overlap :
∀ s : Set Ω
M :
ℝ
_hY_le :
∀ᵐ ω ∂μ, Y ω ≤ M
conclusion
∀ᵐ ω ∂μ, Ya ω ≤ M
Proof (Lean source)
theorem ae_le_YofA_of_ae_le_Y
{Ω : Type*} {mΩ : MeasurableSpace Ω}
[@StandardBorelSpace Ω mΩ]
{μ : @Measure Ω mΩ} [@IsFiniteMeasure Ω mΩ μ]
{σ_UX : MeasurableSpace Ω} (_hσUX : σ_UX ≤ mΩ)
{α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
{A : Ω → α} {Y Ya : Ω → ℝ}
(_hA : @Measurable Ω α mΩ _ A)
(_hYa : @Measurable Ω ℝ mΩ _ Ya)
(a : α)
(_latent_exch : CondIndepFun σ_UX _hσUX Ya A μ)
(_consistency : Y =ᵐ[μ.restrict {ω | A ω = a}] Ya)
(_h_overlap : ∀ s : Set Ω, MeasurableSet[σ_UX] s →
μ (s ∩ {ω | A ω = a}) = 0 → μ s = 0)
{M : ℝ} (_hY_le : ∀ᵐ ω ∂μ, Y ω ≤ M) :
∀ᵐ ω ∂μ, Ya ω ≤ M := by
let E : Set Ω := {ω | A ω = a}
let B : Set Ω := {ω | M < Ya ω}
have hE : @MeasurableSet Ω mΩ E := by
dsimp [E]
exact _hA (measurableSet_singleton a)
have hB : @MeasurableSet Ω mΩ B := by
dsimp [B]
exact _hYa measurableSet_Ioi
have hYa_le_on_E : ∀ᵐ ω ∂μ.restrict E, Ya ω ≤ M := by
filter_upwards [_consistency, MeasureTheory.ae_restrict_of_ae _hY_le] with ω hcons hYle
rw [← hcons]
exact hYle
have hBE_zero : μ (B ∩ E) = 0 := by
have hbad : (μ.restrict E) B = 0 := by
have := MeasureTheory.ae_iff.mp hYa_le_on_E
simpa [B, not_le] using this
rwa [MeasureTheory.Measure.restrict_apply hB] at hbad
have hCI :
μ⟦B ∩ E | σ_UX⟧ =ᵐ[μ]
fun ω => (μ⟦B | σ_UX⟧) ω * (μ⟦E | σ_UX⟧) ω := by
have hraw :=
(ProbabilityTheory.condIndepFun_iff_condExp_inter_preimage_eq_mul _hYa _hA).mp
_latent_exch (Ioi M) ({a} : Set α) measurableSet_Ioi
(measurableSet_singleton a)
simpa [B, E, preimage, Set.mem_Ioi, Set.mem_singleton_iff] using hraw
have hBE_indicator_zero :
indicator (B ∩ E) (fun _ : Ω => (1 : ℝ)) =ᵐ[μ] 0 := by
have hnot : ∀ᵐ ω ∂μ, ω ∉ B ∩ E := by
rw [MeasureTheory.ae_iff]
simpa using hBE_zero
filter_upwards [hnot] with ω hω
simp [Set.indicator_of_notMem, hω]
have hCE_BE_zero : μ⟦B ∩ E | σ_UX⟧ =ᵐ[μ] 0 := by
simpa using
(MeasureTheory.condExp_congr_ae (m := σ_UX) (μ := μ) hBE_indicator_zero)
have hE_pos : ∀ᵐ ω ∂μ, 0 < (μ⟦E | σ_UX⟧) ω := by
simpa [E] using
(ae_pos_condExp_indicator_of_le (mΩ := mΩ) (μ := μ)
(m₁ := σ_UX) _hσUX hE _h_overlap)
have hCE_B_zero : μ⟦B | σ_UX⟧ =ᵐ[μ] 0 := by
have hprod_zero :
(fun ω => (μ⟦B | σ_UX⟧) ω * (μ⟦E | σ_UX⟧) ω) =ᵐ[μ] 0 :=
hCI.symm.trans hCE_BE_zero
filter_upwards [hprod_zero, hE_pos] with ω hprod hpos
exact (mul_eq_zero.mp hprod).resolve_right (ne_of_gt hpos)
haveI : IsFiniteMeasure (μ.trim _hσUX) :=
MeasureTheory.isFiniteMeasure_trim _hσUX
haveI : SigmaFinite (μ.trim _hσUX) := inferInstance
have hB_zero : μ B = 0 := by
have hInt_cond_zero : ∫ ω, (μ⟦B | σ_UX⟧) ω ∂μ = 0 := by
simpa using MeasureTheory.integral_congr_ae hCE_B_zero
have hInt_cond_eq :
∫ ω, (μ⟦B | σ_UX⟧) ω ∂μ
= ∫ ω, indicator B (fun _ : Ω => (1 : ℝ)) ω ∂μ := by
exact MeasureTheory.integral_condExp _hσUX
have hInt_B_zero :
∫ ω, indicator B (fun _ : Ω => (1 : ℝ)) ω ∂μ = 0 :=
hInt_cond_eq.symm.trans hInt_cond_zero
have hB_real_zero : μ.real B = 0 := by
rw [← MeasureTheory.integral_indicator_one (μ := μ) hB]
exact hInt_B_zero
exact (MeasureTheory.measureReal_eq_zero_iff (μ := μ) (s := B)).mp hB_real_zero
rw [MeasureTheory.ae_iff]
simpa [B, not_le] using hB_zero
theorem ae_le_YofA_of_ae_le_Y_below reviewed
⚑ flagged
Causalean
Y(a) inherits Y's a.e. lower bound under latent exchangeability and consistency. For a sub-σ-algebra σ_UX coarser than the ambient σ-algebra, a measurable treatment map A, a measurable potential outcome Ya, and a treatment value a, if Ya is conditionally independent of A given σ_UX — latent exchangeability, the observed outcome Y agrees with Ya almost everywhere on the restriction of the measure to the event {A = a} — consistency, the conditional probability of {A = a} given σ_UX is positive almost everywhere — overlap, and Y is at least M almost everywhere, then Ya is at least M almost everywhere as well.
Formal statement
hypotheses
Ω :
_hσUX :
σ_UX ≤ mΩ
α :
Y Ya :
Ω → ℝ
_hA :
@Measurable Ω α mΩ _ A
_hYa :
@Measurable Ω ℝ mΩ _ Ya
a :
α
_latent_exch :
CondIndepFun σ_UX _hσUX Ya A μ
_consistency :
Y =ᵐ[μ.restrict {ω | A ω = a}] Ya
_h_overlap :
∀ s : Set Ω
M :
ℝ
_hY_ge :
∀ᵐ ω ∂μ, M ≤ Y ω
conclusion
∀ᵐ ω ∂μ, M ≤ Ya ω
Proof (Lean source)
theorem ae_le_YofA_of_ae_le_Y_below
{Ω : Type*} {mΩ : MeasurableSpace Ω}
[@StandardBorelSpace Ω mΩ]
{μ : @Measure Ω mΩ} [@IsFiniteMeasure Ω mΩ μ]
{σ_UX : MeasurableSpace Ω} (_hσUX : σ_UX ≤ mΩ)
{α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α]
{A : Ω → α} {Y Ya : Ω → ℝ}
(_hA : @Measurable Ω α mΩ _ A)
(_hYa : @Measurable Ω ℝ mΩ _ Ya)
(a : α)
(_latent_exch : CondIndepFun σ_UX _hσUX Ya A μ)
(_consistency : Y =ᵐ[μ.restrict {ω | A ω = a}] Ya)
(_h_overlap : ∀ s : Set Ω, MeasurableSet[σ_UX] s →
μ (s ∩ {ω | A ω = a}) = 0 → μ s = 0)
{M : ℝ} (_hY_ge : ∀ᵐ ω ∂μ, M ≤ Y ω) :
∀ᵐ ω ∂μ, M ≤ Ya ω := by
have hneg : ∀ᵐ ω ∂μ, -Ya ω ≤ -M :=
ae_le_YofA_of_ae_le_Y (mΩ := mΩ) (μ := μ) (σ_UX := σ_UX) _hσUX
(A := A) (Y := fun ω => -Y ω) (Ya := fun ω => -Ya ω)
_hA _hYa.neg a
_latent_exch.neg_left
(_consistency.mono fun ω hω => by simp [hω])
_h_overlap
(_hY_ge.mono fun ω hω => neg_le_neg hω)
exact hneg.mono fun ω hω => neg_le_neg_iff.mp hω
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 3 core · 4 supporting This file proves conditional-expectation identities implied by conditional independence, including drop-of-conditioning, product factorization, weak union, and contraction. ★ condExp_mul_of_condIndep★ condIndepFun_weak_union_of_prodMk★ condIndepFun_contraction_of_prodMk
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 supply the graph-independent conditional independence algebra used by causal identification proofs.
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 condExp_mul_of_condIndep reviewed
⚑ flagged
Causalean
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))
theorem condIndepFun_weak_union_of_prodMk reviewed
⚑ flagged
Causalean
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
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
4 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 — Drop-of-conditioning for conditional expectation under conditional independence.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 -
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
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. ★ 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. The results support proxy and partial-identification arguments that reason through 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
σ-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
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 (moreover ∫_B g dμ ≤ μ C).
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⟩
ThreeBlockDensity 1 core · 0 supporting This module isolates the measure-theoretic bridge needed by finite-DAG local Markov proofs. ★ condIndepFun_threeBlock_of_density_factors
Conditional independence from a three-block product density
This module isolates the measure-theoretic bridge needed by finite-DAG local Markov proofs.
It turns a density whose two random blocks interact only through a third, conditioning block
into CondIndepFun for the two coordinate maps given the third coordinate.
theorem condIndepFun_threeBlock_of_density_factors reviewed
⚑ flagged
Causalean
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
/-
This is the lowest analytic obligation in the ordered local-Markov proof. A direct route is
to compute the conditioning marginal and the two random-block-with-conditioning marginals by
Tonelli, prove the cross-multiplied density identity, and use Mathlib's conditional-expectation
characterization of `CondIndepFun`. The empty `Y` and empty `Z` cases must be discharged
separately; no positivity or nonemptiness assumption is valid here.
-/
classical
cases isEmpty_or_nonempty Y with
| inl hY =>
letI := hY
rw [condIndepFun_iff_condExp_inter_preimage_eq_mul
(show Measurable (fun q : Y × (Z × C) ↦ q.1) from measurable_fst)
(show Measurable (fun q : Y × (Z × C) ↦ q.2.1) from
measurable_fst.comp measurable_snd)]
intro s t hs ht
exact ae_of_all _ fun q ↦ isEmptyElim q.1
| inr hY =>
letI := hY
cases isEmpty_or_nonempty Z with
| inl hZ =>
letI := hZ
rw [condIndepFun_iff_condExp_inter_preimage_eq_mul
(show Measurable (fun q : Y × (Z × C) ↦ q.1) from measurable_fst)
(show Measurable (fun q : Y × (Z × C) ↦ q.2.1) from
measurable_fst.comp measurable_snd)]
intro s t hs ht
exact ae_of_all _ fun q ↦ isEmptyElim q.2.1
| inr hZ =>
letI := hZ
let ref : Measure (Y × (Z × C)) := muY.prod (muZ.prod muC)
let fact : Y × (Z × C) → ℝ≥0∞ :=
fun q ↦ a (q.1, q.2.2) * b (q.2.1, q.2.2)
let P : Measure (Y × (Z × C)) := ref.withDensity fact
have hP : (muY.prod (muZ.prod muC)).withDensity d = P := by
exact withDensity_congr_ae hfactor
letI : IsFiniteMeasure P := hP ▸ inferInstance
let massY : C → ℝ≥0∞ := fun c ↦ ∫⁻ y, a (y, c) ∂muY
let massZ : C → ℝ≥0∞ := fun c ↦ ∫⁻ z, b (z, c) ∂muZ
let mass : C → ℝ≥0∞ := fun c ↦ massY c * massZ c
have hmassY : Measurable massY := by
unfold massY
fun_prop
have hmassZ : Measurable massZ := by
unfold massZ
fun_prop
have hmass : Measurable mass := hmassY.mul hmassZ
let ccoord : Y × (Z × C) → C := fun q ↦ q.2.2
let yzcoord : Y × (Z × C) → Y × Z := fun q ↦ (q.1, q.2.1)
have hccoord : Measurable ccoord := measurable_snd.comp measurable_snd
have hyzcoord : Measurable yzcoord := measurable_fst.prodMk
(measurable_fst.comp measurable_snd)
have hPmapC : P.map ccoord = muC.withDensity mass := by
refine Measure.ext_of_lintegral _ fun f hf ↦ ?_
rw [lintegral_map hf hccoord,
lintegral_withDensity_eq_lintegral_mul _ (by
unfold fact
fun_prop) (by fun_prop),
lintegral_withDensity_eq_lintegral_mul _ hmass hf]
change (∫⁻ q : Y × (Z × C),
a (q.1, q.2.2) * b (q.2.1, q.2.2) * f q.2.2
∂muY.prod (muZ.prod muC)) =
∫⁻ c, (∫⁻ y, a (y, c) ∂muY) * (∫⁻ z, b (z, c) ∂muZ) * f c ∂muC
rw [lintegral_prod _ (by fun_prop)]
calc
_ = ∫⁻ y, ∫⁻ z, ∫⁻ c,
a (y, c) * b (z, c) * f c ∂muC ∂muZ ∂muY := by
apply lintegral_congr
intro y
rw [lintegral_prod _ (by fun_prop)]
_ = ∫⁻ y, ∫⁻ c, ∫⁻ z,
a (y, c) * b (z, c) * f c ∂muZ ∂muC ∂muY := by
apply lintegral_congr
intro y
exact lintegral_lintegral_swap (by fun_prop)
_ = ∫⁻ c, ∫⁻ y, ∫⁻ z,
a (y, c) * b (z, c) * f c ∂muZ ∂muY ∂muC := by
exact lintegral_lintegral_swap (by fun_prop)
_ = _ := by
apply lintegral_congr
intro c
calc
_ = ∫⁻ y, a (y, c) * (massZ c * f c) ∂muY := by
apply lintegral_congr
intro y
calc
_ = ∫⁻ z, a (y, c) * (b (z, c) * f c) ∂muZ := by
apply lintegral_congr
intro z
ac_rfl
_ = a (y, c) * (∫⁻ z, b (z, c) * f c ∂muZ) := by
rw [lintegral_const_mul]
fun_prop
_ = _ := by
rw [lintegral_mul_const]
fun_prop
_ = massY c * (massZ c * f c) := by
rw [lintegral_mul_const]
fun_prop
_ = massY c * massZ c * f c := by ac_rfl
let ν : Measure C := muC.withDensity mass
haveI : IsFiniteMeasure ν := by
change IsFiniteMeasure (muC.withDensity mass)
rw [← hPmapC]
infer_instance
have hmassInt : ∫⁻ c, mass c ∂muC ≠ ∞ := by
have h := measure_ne_top ν univ
simpa [ν, withDensity_apply] using h
have hmassFinite : ∀ᵐ c ∂muC, mass c ≠ ∞ :=
(ae_lt_top hmass hmassInt).mono fun _ h ↦ h.ne
let goodY : Set C := {c | massY c ≠ 0 ∧ massY c ≠ ∞}
let goodZ : Set C := {c | massZ c ≠ 0 ∧ massZ c ≠ ∞}
have hgoodY : MeasurableSet goodY :=
((hmassY (measurableSet_singleton 0)).compl.inter
(hmassY (measurableSet_singleton ∞)).compl)
have hgoodZ : MeasurableSet goodZ :=
((hmassZ (measurableSet_singleton 0)).compl.inter
(hmassZ (measurableSet_singleton ∞)).compl)
have hgoodY_ae : ∀ᵐ c ∂ν, c ∈ goodY := by
change ∀ᵐ c ∂muC.withDensity mass, c ∈ goodY
rw [ae_withDensity_iff hmass]
filter_upwards [hmassFinite] with c hcTop hc0
have hy0 : massY c ≠ 0 := by
intro hy
apply hc0
simp [mass, hy]
have hyTop : massY c ≠ ∞ := by
intro hy
have hz0 : massZ c ≠ 0 := by
intro hz
apply hc0
simp [mass, hz]
apply hcTop
simp [mass, hy, hz0]
exact ⟨hy0, hyTop⟩
have hgoodZ_ae : ∀ᵐ c ∂ν, c ∈ goodZ := by
change ∀ᵐ c ∂muC.withDensity mass, c ∈ goodZ
rw [ae_withDensity_iff hmass]
filter_upwards [hmassFinite] with c hcTop hc0
have hz0 : massZ c ≠ 0 := by
intro hz
apply hc0
simp [mass, hz]
have hzTop : massZ c ≠ ∞ := by
intro hz
have hy0 : massY c ≠ 0 := by
intro hy
apply hc0
simp [mass, hy]
apply hcTop
simp [mass, hz, hy0]
exact ⟨hz0, hzTop⟩
let fallbackY : Kernel C Y :=
Kernel.const C (Measure.dirac (choice hY))
let fallbackZ : Kernel C Z :=
Kernel.const C (Measure.dirac (choice hZ))
have hrawY : Measurable
(fun c ↦ muY.withDensity (fun y ↦ a (y, c) / massY c)) := by
apply Measure.measurable_of_measurable_coe
intro s hs
simp_rw [withDensity_apply _ hs]
fun_prop
have hrawZ : Measurable
(fun c ↦ muZ.withDensity (fun z ↦ b (z, c) / massZ c)) := by
apply Measure.measurable_of_measurable_coe
intro s hs
simp_rw [withDensity_apply _ hs]
fun_prop
let κY : Kernel C Y :=
⟨fun c ↦ if c ∈ goodY then
muY.withDensity (fun y ↦ a (y, c) / massY c) else fallbackY c,
hrawY.piecewise hgoodY fallbackY.measurable⟩
let κZ : Kernel C Z :=
⟨fun c ↦ if c ∈ goodZ then
muZ.withDensity (fun z ↦ b (z, c) / massZ c) else fallbackZ c,
hrawZ.piecewise hgoodZ fallbackZ.measurable⟩
have hκYmarkov : IsMarkovKernel κY := by
refine ⟨fun c ↦ ⟨?_⟩⟩
change (if c ∈ goodY then
muY.withDensity (fun y ↦ a (y, c) / massY c) else fallbackY c) univ = 1
split_ifs with hc
· rw [withDensity_apply' _ univ, Measure.restrict_univ]
simp only [ENNReal.div_eq_inv_mul]
rw [lintegral_const_mul]
· exact ENNReal.inv_mul_cancel hc.1 hc.2
· fun_prop
· simp [fallbackY]
have hκZmarkov : IsMarkovKernel κZ := by
refine ⟨fun c ↦ ⟨?_⟩⟩
change (if c ∈ goodZ then
muZ.withDensity (fun z ↦ b (z, c) / massZ c) else fallbackZ c) univ = 1
split_ifs with hc
· rw [withDensity_apply' _ univ, Measure.restrict_univ]
simp only [ENNReal.div_eq_inv_mul]
rw [lintegral_const_mul]
· exact ENNReal.inv_mul_cancel hc.1 hc.2
· fun_prop
· simp [fallbackZ]
letI : IsMarkovKernel κY := hκYmarkov
letI : IsMarkovKernel κZ := hκZmarkov
have hgoodY_imp : ∀ᵐ c ∂muC, mass c ≠ 0 → c ∈ goodY :=
(ae_withDensity_iff hmass).1 hgoodY_ae
have hgoodZ_imp : ∀ᵐ c ∂muC, mass c ≠ 0 → c ∈ goodZ :=
(ae_withDensity_iff hmass).1 hgoodZ_ae
let jointcoord : Y × (Z × C) → C × (Y × Z) :=
fun q ↦ (ccoord q, yzcoord q)
have hjointcoord : Measurable jointcoord := hccoord.prodMk hyzcoord
have hjoint : P.map jointcoord = ν ⊗ₘ (κY ×ₖ κZ) := by
refine Measure.ext_of_lintegral _ fun g hg ↦ ?_
rw [lintegral_map hg hjointcoord,
lintegral_withDensity_eq_lintegral_mul _ (by
unfold fact
fun_prop) (by fun_prop), Measure.lintegral_compProd hg]
change (∫⁻ q : Y × (Z × C),
a (q.1, q.2.2) * b (q.2.1, q.2.2) * g (q.2.2, (q.1, q.2.1))
∂muY.prod (muZ.prod muC)) =
∫⁻ c, ∫⁻ yz, g (c, yz) ∂(κY ×ₖ κZ) c ∂ν
rw [lintegral_prod _ (by fun_prop)]
calc
_ = ∫⁻ y, ∫⁻ z, ∫⁻ c,
a (y, c) * b (z, c) * g (c, (y, z)) ∂muC ∂muZ ∂muY := by
apply lintegral_congr
intro y
rw [lintegral_prod _ (by fun_prop)]
_ = ∫⁻ y, ∫⁻ c, ∫⁻ z,
a (y, c) * b (z, c) * g (c, (y, z)) ∂muZ ∂muC ∂muY := by
apply lintegral_congr
-- … truncated; follow the source link for the rest …