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 : ℝ))) :=
measurable_const.indicator hs
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 : ℝ))) :=
measurable_const.indicator hs
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 := hY.prod hW
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 : ℝ))) :=
measurable_const.indicator hs_meas
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 (Function.support u) (Function.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
dsimp [p, f]
exact MeasureTheory.stronglyMeasurable_condExp
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
dsimp [gn]
exact (_hg_meas.max measurable_const).min measurable_const
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⟩