PO.Conditioning
Conditioning machinery for potential outcomes: σ-algebras generated by regimed variables and reusable event-level conditional-expectation tooling.
Bundle 5 core · 24 supporting This file defines the σ-algebra generated by a bundle of regimed potential-outcome variables and provides conditional expectations, conditional ratios, and bundle-conditioned independence statements relative to that σ-al ★ condExpGiven★ condExpRatio★ CondIndepCFBundle★ project
Bundle Conditional Expectations
This file defines the σ-algebra generated by a bundle of regimed potential-outcome variables and provides conditional expectations, conditional ratios, and bundle-conditioned independence statements relative to that σ-algebra. It extends the single-variable conditioning interface to finite counterfactual bundles.
The key definitions are POCFBundle.sigma, POCFBundle.condExpGiven,
POCFBundle.condExpRatio, and POSystem.CondIndepCFBundle. The file also
provides measurability, integrability, tower, pull-out, a.e.-congruence, ratio,
and projection lemmas used by bundle-conditioned identification arguments.
def sigma reviewed
⚑ flagged
Causalean.PO.POCFBundle
For a potential-outcome system and a finite bundle of counterfactual variables, the conditioning σ-algebra of the bundle is the σ-algebra on the sample space generated by jointly observing every counterfactual value in that bundle.
Definition (Lean source)
def condExpGiven reviewed
⚑ flagged
Causalean.PO.POCFBundle
For a potential-outcome system, a counterfactual bundle, a real-valued quantity on the sample space, and a measure on that sample space, the bundle conditional expectation is the conditional expectation of the quantity given the σ-algebra generated by jointly observing the bundle.
Definition (Lean source)
parameters
def
condExpGiven B g μ :
P.Ω → ℝ
given by
μ[g | B.sigma]
def condExpRatio reviewed
⚑ flagged
Causalean.PO.POCFBundle
For a potential-outcome system, a counterfactual bundle, two real-valued quantities on the sample space, and a measure on that sample space, the bundle conditional-expectation ratio maps each sample point to the conditional expectation of the first quantity given the bundle divided by that of the second at that sample point.
Definition (Lean source)
parameters
def
condExpRatio B g h μ :
P.Ω → ℝ
given by
fun ω => (B.condExpGiven g μ ω) / (B.condExpGiven h μ ω)
def CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POSystem
For a potential-outcome system whose sample space is standard Borel, a measurable outcome space, a potential-outcome variable taking values in that space, a counterfactual bundle, a conditioning counterfactual bundle, and a finite measure on the sample space, the conditional-independence assertion states that the variable and the first bundle are conditionally independent given the σ-algebra generated by jointly observing the conditioning bundle.
Definition (Lean source)
parameters
def
CondIndepCFBundle P a B C μ :
Prop
given by
CondIndepFun C.sigma C.sigma_le a.value B.jointValue μ
lemma project reviewed
⚑ flagged
Causalean.PO.POSystem.CondIndepCFBundle
Bundle-conditional projection. Given a regimed variable a that is conditionally independent, given the σ-algebra generated by a counterfactual bundle C, of another counterfactual bundle B, then for any measurable function ψ of the joint value of B, the value of a remains conditionally independent, given C's σ-algebra, of ψ composed with the joint value of B.
Formal statement
hypotheses
conclusion
CondIndepFun C.sigma C.sigma_le a.value (ψ ∘ B.jointValue) μ
Proof (Lean source)
lemma CondIndepCFBundle.project
[StandardBorelSpace P.Ω]
{α β : Type*} [MeasurableSpace α] [MeasurableSpace β]
{a : RegimedVar P α} {B C : POCFBundle P}
{μ : Measure P.Ω} [IsFiniteMeasure μ]
{ψ : (∀ i, B.type i) → β} (h : P.CondIndepCFBundle a B C μ)
(hψ : Measurable ψ) :
CondIndepFun C.sigma C.sigma_le a.value (ψ ∘ B.jointValue) μ :=
h.toCondIndepFun.comp measurable_id hψ
24 supporting declarations (lemmas, instances)
-
sigma_lelemma — The conditioning σ-algebra B.sigma is a sub-σ-algebra of the ambient σ-algebra on P.Ω.Proof (Lean source)
lemma sigma_le : B.sigma ≤ (inferInstance : MeasurableSpace P.Ω) := B.measurable_jointValue.comap_le -
measurable_jointValue_sigmalemma — The bundle's joint counterfactual-value map is measurable for the very σ-algebra it generates: conditioning information always determines the values that were conditioned on. This is the generator lemma that lets automation discharge measurability of bundle-value compositions relative to B.sigma.Proof (Lean source)
@[fun_prop] lemma measurable_jointValue_sigma : Measurable[B.sigma] B.jointValue := Measurable.of_comap_le le_rfl -
condExpGiven_eqlemma — Averaging a real-valued sample-space quantity given a counterfactual bundle is exactly the standard conditional expectation given the σ-algebra that the bundle generates.hypothesesconclusionB.condExpGiven g μ = μ[g | B.sigma] -
stronglyMeasurable_condExpGiven_comaplemma — condExpGiven yields a function strongly measurable w.r.t. B.sigma.hypothesesconclusionStronglyMeasurable[B.sigma] (B.condExpGiven g μ)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_condExpGiven_comap (g : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable[B.sigma] (B.condExpGiven g μ) := MeasureTheory.stronglyMeasurable_condExp (μ := μ) (m := B.sigma) (f := g) -
stronglyMeasurable_condExpGivenlemma — condExpGiven yields a strongly measurable function w.r.t. the ambient σ-algebra.hypothesesconclusionStronglyMeasurable (B.condExpGiven g μ)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_condExpGiven (g : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable (B.condExpGiven g μ) := (B.stronglyMeasurable_condExpGiven_comap g).mono B.sigma_le -
integrable_condExpGivenlemma — Mathlib's totalized conditional expectation given the bundle's σ-algebra is integrable, even when the original sample-space function is not assumed integrable.hypothesesconclusionIntegrable (B.condExpGiven g μ) μProof (Lean source)
@[fun_prop] lemma integrable_condExpGiven (g : P.Ω → ℝ) {μ : Measure P.Ω} : Integrable (B.condExpGiven g μ) μ := by simpa [condexp_simps] using (MeasureTheory.integrable_condExp (μ := μ) (m := B.sigma) (f := g)) -
condExpGiven_addlemma — Linearity of the bundle conditional expectation: additivity.hypothesesconclusionB.condExpGiven (f + g) μ =ᵐ[μ] B.condExpGiven f μ + B.condExpGiven g μProof (Lean source)
lemma condExpGiven_add {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) (hg : Integrable g μ) : B.condExpGiven (f + g) μ =ᵐ[μ] B.condExpGiven f μ + B.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_add (μ := μ) hf hg B.sigma -
condExpGiven_sublemma — Linearity of the bundle conditional expectation: subtraction.hypothesesconclusionB.condExpGiven (f - g) μ =ᵐ[μ] B.condExpGiven f μ - B.condExpGiven g μProof (Lean source)
lemma condExpGiven_sub {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) (hg : Integrable g μ) : B.condExpGiven (f - g) μ =ᵐ[μ] B.condExpGiven f μ - B.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_sub (μ := μ) hf hg B.sigma -
condExpGiven_add'lemma — Additivity of the bundle conditional expectation with the integrability side conditions discharged automatically.hypothesesconclusionB.condExpGiven (f + g) μ =ᵐ[μ] B.condExpGiven f μ + B.condExpGiven g μProof (Lean source)
lemma condExpGiven_add' {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) : B.condExpGiven (f + g) μ =ᵐ[μ] B.condExpGiven f μ + B.condExpGiven g μ := B.condExpGiven_add hf hg -
condExpGiven_sub'lemma — Subtractivity of the bundle conditional expectation with the integrability side conditions discharged automatically; see POCFBundle.condExpGiven_add'.hypothesesconclusionB.condExpGiven (f - g) μ =ᵐ[μ] B.condExpGiven f μ - B.condExpGiven g μProof (Lean source)
lemma condExpGiven_sub' {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) : B.condExpGiven (f - g) μ =ᵐ[μ] B.condExpGiven f μ - B.condExpGiven g μ := B.condExpGiven_sub hf hg -
condExpGiven_smullemma — Scalar homogeneity of the bundle conditional expectation. No integrability is required.hypothesesconclusionB.condExpGiven (k • g) μ =ᵐ[μ] k • B.condExpGiven g μProof (Lean source)
lemma condExpGiven_smul (k : ℝ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : B.condExpGiven (k • g) μ =ᵐ[μ] k • B.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_smul (μ := μ) k g B.sigma -
condExpGiven_neglemma — Negation passes through the bundle conditional expectation. No integrability is required.hypothesesconclusionB.condExpGiven (-g) μ =ᵐ[μ] -B.condExpGiven g μProof (Lean source)
lemma condExpGiven_neg (g : P.Ω → ℝ) {μ : Measure P.Ω} : B.condExpGiven (-g) μ =ᵐ[μ] -B.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_neg (μ := μ) g B.sigma -
condExpGiven_constlemma — A constant is its own bundle conditional expectation: on a finite measure, averaging a constant given a counterfactual bundle returns that constant, everywhere (not merely almost everywhere).hypothesesconclusionB.condExpGiven (fun _ => k) μ = fun _ => kProof (Lean source)
lemma condExpGiven_const (k : ℝ) {μ : Measure P.Ω} [IsFiniteMeasure μ] : B.condExpGiven (fun _ => k) μ = fun _ => k := MeasureTheory.condExp_const (μ := μ) B.sigma_le k -
condExpGiven_finsetSum'lemma — The bundle conditional expectation commutes with a finite sum, with the family-wide integrability side condition discharged automatically by fun_prop.hypothesesconclusionB.condExpGiven (∑ i ∈ s, F i) μ =ᵐ[μ] ∑ i ∈ s, B.condExpGiven (F i) μProof (Lean source)
lemma condExpGiven_finsetSum' {ι : Type*} {s : Finset ι} {F : ι → P.Ω → ℝ} {μ : Measure P.Ω} (hF : ∀ i ∈ s, Integrable (F i) μ := by intro i _; fun_prop) : B.condExpGiven (∑ i ∈ s, F i) μ =ᵐ[μ] ∑ i ∈ s, B.condExpGiven (F i) μ := by simpa [condexp_simps] using MeasureTheory.condExp_finsetSum (μ := μ) hF B.sigma -
condExpGiven_tower_of_lelemma — Tower property over an arbitrary smaller sub-σ-algebra m ≤ B.sigma. Requires the usual SigmaFinite hypothesis on the trim of μ to B.sigma.hypothesesg :P.Ω → ℝμ :Measure P.Ωm :MeasurableSpace P.Ωhm :m ≤ B.sigmaSigmaFinite (μ.trim B.sigma_le)conclusionμ[B.condExpGiven g μ | m] =ᵐ[μ] μ[g | m]Proof (Lean source)
lemma condExpGiven_tower_of_le {g : P.Ω → ℝ} {μ : Measure P.Ω} {m : MeasurableSpace P.Ω} (hm : m ≤ B.sigma) [SigmaFinite (μ.trim B.sigma_le)] : μ[B.condExpGiven g μ | m] =ᵐ[μ] μ[g | m] := by simpa [condexp_simps] using MeasureTheory.condExp_condExp_of_le (μ := μ) (f := g) hm B.sigma_le -
condExpGiven_mul_of_stronglyMeasurable_leftlemma — Pull-out-left for condExpGiven: if f is strongly measurable w.r.t. B.sigma, then μ[f·g | B.sigma] =ᵐ f · μ[g | B.sigma].hypothesesf g :P.Ω → ℝμ :Measure P.Ωhf :StronglyMeasurable[B.sigma] fhfg :Integrable (f * g) μhg :Integrable g μconclusionB.condExpGiven (f * g) μ =ᵐ[μ] f * B.condExpGiven g μProof (Lean source)
lemma condExpGiven_mul_of_stronglyMeasurable_left {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : StronglyMeasurable[B.sigma] f) (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : B.condExpGiven (f * g) μ =ᵐ[μ] f * B.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := μ) (m := B.sigma) hf hfg hg -
condExpGiven_mul_of_stronglyMeasurable_rightlemma — Pull-out-right for condExpGiven.hypothesesf g :P.Ω → ℝμ :Measure P.Ωhg :StronglyMeasurable[B.sigma] ghfg :Integrable (f * g) μhf :Integrable f μconclusionB.condExpGiven (f * g) μ =ᵐ[μ] B.condExpGiven f μ * gProof (Lean source)
lemma condExpGiven_mul_of_stronglyMeasurable_right {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hg : StronglyMeasurable[B.sigma] g) (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : B.condExpGiven (f * g) μ =ᵐ[μ] B.condExpGiven f μ * g := by simpa [condexp_simps] using MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := μ) (m := B.sigma) hg hfg hf -
condExpGiven_indicator_mullemma — Indicator pull-out for condExpGiven: if s is B.sigma-measurable, the indicator 1_s factors out of the bundle conditional expectation.hypothesesconclusionB.condExpGiven (s.indicator (fun _ => (1 : ℝ)) * g) μ=ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) * B.condExpGiven g μProof (Lean source)
lemma condExpGiven_indicator_mul {s : Set P.Ω} {g : P.Ω → ℝ} {μ : Measure P.Ω} (hs : MeasurableSet[B.sigma] s) (hg : Integrable g μ) : B.condExpGiven (s.indicator (fun _ => (1 : ℝ)) * g) μ =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) * B.condExpGiven g μ := by have hsg : Integrable (s.indicator (fun _ => (1 : ℝ)) * g) μ := by have hs_meas : AEStronglyMeasurable (s.indicator (fun _ => (1 : ℝ))) μ := StronglyMeasurable.aestronglyMeasurable (((stronglyMeasurable_const (b := (1 : ℝ))).indicator hs).mono B.sigma_le) refine hg.mono (hs_meas.mul hg.aestronglyMeasurable) ?_ refine Filter.Eventually.of_forall (fun ω => ?_) by_cases hω : ω ∈ s <;> simp [indicator, hω] exact B.condExpGiven_mul_of_stronglyMeasurable_left ((stronglyMeasurable_const (b := (1 : ℝ))).indicator hs) hsg hg -
condExpGiven_congr_aelemma — a.e. congruence for condExpGiven: if f =ᵐ g, then their bundle conditional expectations agree a.e.hypothesesconclusionB.condExpGiven f μ =ᵐ[μ] B.condExpGiven g μProof (Lean source)
lemma condExpGiven_congr_ae {f g : P.Ω → ℝ} {μ : Measure P.Ω} (h : f =ᵐ[μ] g) : B.condExpGiven f μ =ᵐ[μ] B.condExpGiven g μ := by simp only [condexp_simps] exact MeasureTheory.condExp_congr_ae h -
condExpRatio_deflemma — The bundle conditional-expectation ratio is, pointwise, the quotient of the two bundle conditional expectations.hypothesesconclusionB.condExpRatio g h μ = fun ω => B.condExpGiven g μ ω / B.condExpGiven h μ ω -
measurable_condExpRatiolemma — The conditional-ratio function of two real integrands given a counterfactual bundle is measurable.hypothesesconclusionMeasurable (B.condExpRatio g h μ)Proof (Lean source)
@[fun_prop] lemma measurable_condExpRatio (g h : P.Ω → ℝ) {μ : Measure P.Ω} : Measurable (B.condExpRatio g h μ) := by simp only [condexp_simps] exact (B.stronglyMeasurable_condExpGiven g).measurable.div (B.stronglyMeasurable_condExpGiven h).measurable -
stronglyMeasurable_condExpRatiolemma — The conditional-ratio function of two real integrands given a counterfactual bundle is strongly measurable.hypothesesconclusionStronglyMeasurable (B.condExpRatio g h μ)Proof (Lean source)
@[fun_prop] lemma stronglyMeasurable_condExpRatio (g h : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable (B.condExpRatio g h μ) := (B.measurable_condExpRatio g h).stronglyMeasurable -
condExpRatio_eq_of_mullemma — Characterisation of bundle condExpRatio via a product identity.hypothesesg h target :P.Ω → ℝμ :Measure P.Ωhprod :B.condExpGiven g μ =ᵐ[μ] B.condExpGiven h μ * targethne :∀ᵐ ω ∂μ, B.condExpGiven h μ ω ≠ 0conclusionB.condExpRatio g h μ =ᵐ[μ] targetProof (Lean source)
lemma condExpRatio_eq_of_mul {g h target : P.Ω → ℝ} {μ : Measure P.Ω} (hprod : B.condExpGiven g μ =ᵐ[μ] B.condExpGiven h μ * target) (hne : ∀ᵐ ω ∂μ, B.condExpGiven h μ ω ≠ 0) : B.condExpRatio g h μ =ᵐ[μ] target := by simp only [condexp_simps] filter_upwards [hprod, hne] with ω hω hne simp only [Pi.mul_apply, condexp_simps] at hω hne rw [hω] field_simp -
toCondIndepFunlemma — Bridge: CondIndepCFBundle unfolds to CondIndepFun w.r.t. C.sigma.hypothesesconclusionCondIndepFun C.sigma C.sigma_le a.value B.jointValue μProof (Lean source)
lemma CondIndepCFBundle.toCondIndepFun [StandardBorelSpace P.Ω] {α : Type*} [MeasurableSpace α] {a : RegimedVar P α} {B C : POCFBundle P} {μ : Measure P.Ω} [IsFiniteMeasure μ] : P.CondIndepCFBundle a B C μ → CondIndepFun C.sigma C.sigma_le a.value B.jointValue μ := id
CondExpTooling 3 core · 27 supporting This file wraps conditional expectation so that the conditioning information is the σ-algebra generated by the factual value of a potential-outcome variable. ★ integral_sub_eq_integral_sub_of_condExpGiven_ae_eq
Conditional Expectations Given Potential-Outcome Variables
This file wraps conditional expectation so that the conditioning information is the σ-algebra generated by the factual value of a potential-outcome variable. It supports regression-style identification arguments by also defining ratios of conditional expectations and their basic algebraic properties.
The public interface is centered on POVar.condExpGiven,
POVar.condExpRatio, tower and pull-out lemmas for condExpGiven, the product
identity POVar.condExpRatio_eq_of_mul, and the CATE-to-ATE integration lemma
POVar.integral_sub_eq_integral_sub_of_condExpGiven_ae_eq.
def condExpGiven reviewed
⚑ flagged
Causalean.PO.POVar
For a potential-outcome system, a conditioning variable on a measurable scale, a real-valued sample-space function, and a measure on the sample space, the conditional expectation given the variable is the conditional expectation of the function given the σ-algebra generated by that variable's factual value.
Definition (Lean source)
def condExpRatio reviewed
⚑ flagged
Causalean.PO.POVar
For a potential-outcome system, a conditioning variable on a measurable scale, two real-valued sample-space functions, and a measure on the sample space, the conditional-expectation ratio maps each unit to the conditional expectation of the first function divided by that of the second, with both conditional on the σ-algebra generated by the variable's factual value.
theorem integral_sub_eq_integral_sub_of_condExpGiven_ae_eq reviewed
⚑ flagged
Causalean.PO.POVar
CATE-to-ATE integrator. Fix a conditioning variable c and integrable functions f and g on the same probability space. If f' is an almost-everywhere representative of the conditional expectation of f given c and g' is an almost-everywhere representative of the conditional expectation of g given c, then the integral of f - g equals the integral of f' - g'.
Formal statement
hypotheses
γ :
Type u_1
c :
POVar P γ
f g f' g' :
P.Ω → ℝ
μ :
Measure P.Ω
SigmaFinite (μ.trim c.comap_factual_le)
hf :
Integrable f μ
hg :
Integrable g μ
hf' :
c.condExpGiven f μ =ᵐ[μ] f'
hg' :
c.condExpGiven g μ =ᵐ[μ] g'
conclusion
∫ ω, f ω - g ω ∂μ = ∫ ω, f' ω - g' ω ∂μ
Proof (Lean source)
theorem POVar.integral_sub_eq_integral_sub_of_condExpGiven_ae_eq
(c : POVar P γ) {f g f' g' : P.Ω → ℝ} {μ : Measure P.Ω}
[SigmaFinite (μ.trim c.comap_factual_le)]
(hf : Integrable f μ) (hg : Integrable g μ)
(hf' : c.condExpGiven f μ =ᵐ[μ] f')
(hg' : c.condExpGiven g μ =ᵐ[μ] g') :
∫ ω, f ω - g ω ∂μ = ∫ ω, f' ω - g' ω ∂μ := by
have hIf : ∫ ω, f ω ∂μ = ∫ ω, c.condExpGiven f μ ω ∂μ := by
simp only [condexp_simps]
exact (MeasureTheory.integral_condExp c.comap_factual_le).symm
have hIg : ∫ ω, g ω ∂μ = ∫ ω, c.condExpGiven g μ ω ∂μ := by
simp only [condexp_simps]
exact (MeasureTheory.integral_condExp c.comap_factual_le).symm
rw [MeasureTheory.integral_sub hf hg, hIf, hIg,
← MeasureTheory.integral_sub (c.integrable_condExpGiven f)
(c.integrable_condExpGiven g)]
exact MeasureTheory.integral_congr_ae (hf'.sub hg')
27 supporting declarations (lemmas, instances)
-
condExpGiven_eqlemma — Averaging a real-valued sample-space quantity given a potential-outcome variable is exactly the standard conditional expectation given the σ-algebra generated by that variable's factual value.hypothesesconclusionc.condExpGiven g μ = μ[g | comap c.factual inferInstance]Proof (Lean source)
@[condexp_simps] lemma POVar.condExpGiven_eq (c : POVar P γ) (g : P.Ω → ℝ) (μ : Measure P.Ω) : c.condExpGiven g μ = μ[g | comap c.factual inferInstance] := rfl -
comap_factual_lelemma — The conditioning σ-algebra σ(c.factual) is a sub-σ-algebra of the ambient σ-algebra on P.Ω.hypothesesconclusioncomap c.factual inferInstance ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma POVar.comap_factual_le (c : POVar P γ) : comap c.factual inferInstance ≤ (inferInstance : MeasurableSpace P.Ω) := c.measurable_factual.comap_le -
integrable_mul_indicatorlemma — Multiplying an integrable function by a POVar factual indicator preserves integrability.hypothesesα :Type*a :POVar P αx :αhx :MeasurableSet ({x} : Set α)f :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μconclusionIntegrable (fun ω => f ω * a.indicator x ω) μProof (Lean source)
@[fun_prop] lemma POVar.integrable_mul_indicator {α : Type*} [MeasurableSpace α] (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) {f : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) : Integrable (fun ω => f ω * a.indicator x ω) μ := by refine hf.mono (hf.aestronglyMeasurable.mul (a.measurable_indicator x hx).aestronglyMeasurable) ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rcases a.indicator_eq_one_or_zero x ω with h | h <;> simp [h] -
integrable_indicator_mullemma — Multiplying a POVar factual indicator by an integrable function preserves integrability. This is the indicator-on-the-left companion of POVar.integrable_mul_indicator; the two orders are distinct goal shapes for the function-property tactics.hypothesesα :Type*a :POVar P αx :αhx :MeasurableSet ({x} : Set α)f :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μconclusionIntegrable (fun ω => a.indicator x ω * f ω) μProof (Lean source)
@[fun_prop] lemma POVar.integrable_indicator_mul {α : Type*} [MeasurableSpace α] (a : POVar P α) (x : α) (hx : MeasurableSet ({x} : Set α)) {f : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) : Integrable (fun ω => a.indicator x ω * f ω) μ := by have h := a.integrable_mul_indicator x hx hf exact h.congr (Filter.Eventually.of_forall (fun ω => by ring)) -
integrable_mul_indicator_of_singletonlemma — On a value space whose one-point sets are measurable, multiplying an integrable function by a POVar factual indicator preserves integrability.hypothesesconclusionIntegrable (fun ω => f ω * a.indicator x ω) μProof (Lean source)
@[fun_prop] lemma POVar.integrable_mul_indicator_of_singleton {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (a : POVar P α) (x : α) {f : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) : Integrable (fun ω => f ω * a.indicator x ω) μ := a.integrable_mul_indicator x (MeasurableSet.singleton x) hf -
integrable_indicator_mul_of_singletonlemma — On a value space whose one-point sets are measurable, multiplying a POVar factual indicator by an integrable function preserves integrability.hypothesesconclusionIntegrable (fun ω => a.indicator x ω * f ω) μProof (Lean source)
@[fun_prop] lemma POVar.integrable_indicator_mul_of_singleton {α : Type*} [MeasurableSpace α] [MeasurableSingletonClass α] (a : POVar P α) (x : α) {f : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) : Integrable (fun ω => a.indicator x ω * f ω) μ := a.integrable_indicator_mul x (MeasurableSet.singleton x) hf -
condExpGiven_addlemma — Linearity of condExpGiven: additivity.hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μhg :Integrable g μconclusionc.condExpGiven (f + g) μ =ᵐ[μ] c.condExpGiven f μ + c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_add (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) (hg : Integrable g μ) : c.condExpGiven (f + g) μ =ᵐ[μ] c.condExpGiven f μ + c.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_add (μ := μ) hf hg (comap c.factual inferInstance) -
condExpGiven_sublemma — Linearity of condExpGiven: subtraction.hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μhg :Integrable g μconclusionc.condExpGiven (f - g) μ =ᵐ[μ] c.condExpGiven f μ - c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_sub (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ) (hg : Integrable g μ) : c.condExpGiven (f - g) μ =ᵐ[μ] c.condExpGiven f μ - c.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_sub (μ := μ) hf hg (comap c.factual inferInstance) -
condExpGiven_smullemma — Scalar homogeneity of condExpGiven.hypothesesconclusionc.condExpGiven (k • g) μ =ᵐ[μ] k • c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_smul (c : POVar P γ) (k : ℝ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : c.condExpGiven (k • g) μ =ᵐ[μ] k • c.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_smul (μ := μ) k g (comap c.factual inferInstance) -
condExpGiven_add'lemma — Additivity of condExpGiven with the integrability side conditions discharged automatically.hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μ := by fun_prophg :Integrable g μ := by fun_propconclusionc.condExpGiven (f + g) μ =ᵐ[μ] c.condExpGiven f μ + c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_add' (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) : c.condExpGiven (f + g) μ =ᵐ[μ] c.condExpGiven f μ + c.condExpGiven g μ := c.condExpGiven_add hf hg -
condExpGiven_sub'lemma — Subtractivity of condExpGiven with the integrability side conditions discharged automatically; see POVar.condExpGiven_add'.hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhf :Integrable f μ := by fun_prophg :Integrable g μ := by fun_propconclusionc.condExpGiven (f - g) μ =ᵐ[μ] c.condExpGiven f μ - c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_sub' (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : Integrable f μ := by fun_prop) (hg : Integrable g μ := by fun_prop) : c.condExpGiven (f - g) μ =ᵐ[μ] c.condExpGiven f μ - c.condExpGiven g μ := c.condExpGiven_sub hf hg -
condExpGiven_neglemma — Negation passes through condExpGiven: averaging the negation of a quantity given a variable is the negation of averaging it. No integrability is required.hypothesesconclusionc.condExpGiven (-g) μ =ᵐ[μ] -c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_neg (c : POVar P γ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : c.condExpGiven (-g) μ =ᵐ[μ] -c.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_neg (μ := μ) g (comap c.factual inferInstance) -
condExpGiven_constlemma — A constant is its own conditional expectation: on a finite measure, averaging a constant given a potential-outcome variable returns that constant, everywhere (not merely almost everywhere).hypothesesconclusionc.condExpGiven (fun _ => k) μ = fun _ => kProof (Lean source)
lemma POVar.condExpGiven_const (c : POVar P γ) (k : ℝ) {μ : Measure P.Ω} [IsFiniteMeasure μ] : c.condExpGiven (fun _ => k) μ = fun _ => k := MeasureTheory.condExp_const (μ := μ) c.comap_factual_le k -
condExpGiven_finsetSum'lemma — condExpGiven commutes with a finite sum, with the family-wide integrability side condition discharged automatically by fun_prop.hypothesesγ :sharedType u_1ι :Type*Finset ιc :POVar P γF :ι → P.Ω → ℝμ :Measure P.ΩhF :∀ i ∈ s, Integrable (F i) μ := by intro i _; fun_propconclusionc.condExpGiven (∑ i ∈ s, F i) μ =ᵐ[μ] ∑ i ∈ s, c.condExpGiven (F i) μProof (Lean source)
lemma POVar.condExpGiven_finsetSum' {ι : Type*} {s : Finset ι} (c : POVar P γ) {F : ι → P.Ω → ℝ} {μ : Measure P.Ω} (hF : ∀ i ∈ s, Integrable (F i) μ := by intro i _; fun_prop) : c.condExpGiven (∑ i ∈ s, F i) μ =ᵐ[μ] ∑ i ∈ s, c.condExpGiven (F i) μ := by simpa [condexp_simps] using MeasureTheory.condExp_finsetSum (μ := μ) hF (comap c.factual inferInstance) -
stronglyMeasurable_condExpGiven_comaplemma — condExpGiven yields a function strongly measurable w.r.t. σ(c.factual).hypothesesconclusionProof (Lean source)
@[fun_prop] lemma POVar.stronglyMeasurable_condExpGiven_comap (c : POVar P γ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable[comap c.factual inferInstance] (c.condExpGiven g μ) := MeasureTheory.stronglyMeasurable_condExp (μ := μ) (m := comap c.factual inferInstance) (f := g) -
stronglyMeasurable_condExpGivenlemma — condExpGiven yields a strongly measurable function w.r.t. the ambient σ-algebra.hypothesesconclusionStronglyMeasurable (c.condExpGiven g μ)Proof (Lean source)
@[fun_prop] lemma POVar.stronglyMeasurable_condExpGiven (c : POVar P γ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable (c.condExpGiven g μ) := (c.stronglyMeasurable_condExpGiven_comap g).mono c.comap_factual_le -
integrable_condExpGivenlemma — Mathlib's totalized conditional expectation given the variable's σ-algebra is integrable, even when the original sample-space function is not assumed integrable.hypothesesconclusionIntegrable (c.condExpGiven g μ) μProof (Lean source)
@[fun_prop] lemma POVar.integrable_condExpGiven (c : POVar P γ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : Integrable (c.condExpGiven g μ) μ := by simpa [condexp_simps] using (MeasureTheory.integrable_condExp (μ := μ) (m := comap c.factual inferInstance) (f := g)) -
condExpGiven_mul_of_stronglyMeasurable_leftlemma — Pull-out-left for condExpGiven: if f is strongly measurable w.r.t. σ(c.factual), then μ[f·g | σ(c.factual)] =ᵐ f · μ[g | σ(c.factual)].hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhf :hfg :Integrable (f * g) μhg :Integrable g μconclusionc.condExpGiven (f * g) μ =ᵐ[μ] f * c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_mul_of_stronglyMeasurable_left (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hf : StronglyMeasurable[comap c.factual inferInstance] f) (hfg : Integrable (f * g) μ) (hg : Integrable g μ) : c.condExpGiven (f * g) μ =ᵐ[μ] f * c.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := μ) (m := comap c.factual inferInstance) hf hfg hg -
condExpGiven_mul_of_stronglyMeasurable_rightlemma — Pull-out-right for condExpGiven.hypothesesγ :sharedType u_1c :POVar P γf g :P.Ω → ℝμ :Measure P.Ωhg :hfg :Integrable (f * g) μhf :Integrable f μconclusionc.condExpGiven (f * g) μ =ᵐ[μ] c.condExpGiven f μ * gProof (Lean source)
lemma POVar.condExpGiven_mul_of_stronglyMeasurable_right (c : POVar P γ) {f g : P.Ω → ℝ} {μ : Measure P.Ω} (hg : StronglyMeasurable[comap c.factual inferInstance] g) (hfg : Integrable (f * g) μ) (hf : Integrable f μ) : c.condExpGiven (f * g) μ =ᵐ[μ] c.condExpGiven f μ * g := by simpa [condexp_simps] using MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := μ) (m := comap c.factual inferInstance) hg hfg hf -
condExpGiven_indicator_mullemma — Pull-out version specialised to indicator functions of sets measurable w.r.t. σ(c.factual). If the event is measurable with respect to the conditioning variable's factual σ-algebra, its indicator factors out of the conditional expectation just like any other strongly measurable multiplier.hypothesesconclusionc.condExpGiven (s.indicator (fun _ => (1 : ℝ)) * g) μ=ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) * c.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_indicator_mul (c : POVar P γ) {s : Set P.Ω} {g : P.Ω → ℝ} {μ : Measure P.Ω} (hs : MeasurableSet[comap c.factual inferInstance] s) (hg : Integrable g μ) : c.condExpGiven (s.indicator (fun _ => (1 : ℝ)) * g) μ =ᵐ[μ] s.indicator (fun _ => (1 : ℝ)) * c.condExpGiven g μ := by have hsg : Integrable (s.indicator (fun _ => (1 : ℝ)) * g) μ := by have hs_meas : AEStronglyMeasurable (s.indicator (fun _ => (1 : ℝ))) μ := StronglyMeasurable.aestronglyMeasurable (((stronglyMeasurable_const (b := (1 : ℝ))).indicator hs).mono c.comap_factual_le) refine hg.mono (hs_meas.mul hg.aestronglyMeasurable) ?_ refine Filter.Eventually.of_forall (fun ω => ?_) by_cases hω : ω ∈ s <;> simp [indicator, hω] exact c.condExpGiven_mul_of_stronglyMeasurable_left ((stronglyMeasurable_const (b := (1 : ℝ))).indicator hs) hsg hg -
condExpGiven_tower_of_lelemma — Tower property over an arbitrary smaller sub-σ-algebra m ≤ σ(c.factual). Requires the usual SigmaFinite hypothesis on the trim of μ to σ(c.factual).hypothesesγ :sharedType u_1c :POVar P γg :P.Ω → ℝμ :Measure P.Ωm :MeasurableSpace P.Ωhm :m ≤ comap c.factual inferInstanceSigmaFinite (μ.trim c.comap_factual_le)conclusionμ[c.condExpGiven g μ | m] =ᵐ[μ] μ[g | m]Proof (Lean source)
lemma POVar.condExpGiven_tower_of_le (c : POVar P γ) {g : P.Ω → ℝ} {μ : Measure P.Ω} {m : MeasurableSpace P.Ω} (hm : m ≤ comap c.factual inferInstance) [SigmaFinite (μ.trim c.comap_factual_le)] : μ[c.condExpGiven g μ | m] =ᵐ[μ] μ[g | m] := by simpa [condexp_simps] using MeasureTheory.condExp_condExp_of_le (μ := μ) (f := g) hm c.comap_factual_le -
condExpGiven_towerlemma — Tower property between two POVars: if σ(c₁.factual) ≤ σ(c₂.factual), then μ[μ[g|σ(c₂)] | σ(c₁)] =ᵐ μ[g|σ(c₁)].hypothesesγ :sharedType u_1δ :Type*c₁ :POVar P γc₂ :POVar P δg :P.Ω → ℝμ :Measure P.Ωh :comap c₁.factual inferInstance≤ comap c₂.factual inferInstanceSigmaFinite (μ.trim c₂.comap_factual_le)conclusionc₁.condExpGiven (c₂.condExpGiven g μ) μ =ᵐ[μ] c₁.condExpGiven g μProof (Lean source)
lemma POVar.condExpGiven_tower {δ : Type*} [MeasurableSpace δ] (c₁ : POVar P γ) (c₂ : POVar P δ) {g : P.Ω → ℝ} {μ : Measure P.Ω} (h : comap c₁.factual inferInstance ≤ comap c₂.factual inferInstance) [SigmaFinite (μ.trim c₂.comap_factual_le)] : c₁.condExpGiven (c₂.condExpGiven g μ) μ =ᵐ[μ] c₁.condExpGiven g μ := by simpa [condexp_simps] using MeasureTheory.condExp_condExp_of_le (μ := μ) (f := g) h c₂.comap_factual_le -
condExpRatio_deflemma — The variable conditional-expectation ratio is, pointwise, the quotient of the two conditional expectations given that variable.hypothesesconclusionc.condExpRatio g h μ = fun ω => c.condExpGiven g μ ω / c.condExpGiven h μ ω -
measurable_condExpRatiolemma — condExpRatio is measurable (pointwise division of two strongly measurable functions is measurable).hypothesesconclusionMeasurable (c.condExpRatio g h μ)Proof (Lean source)
@[fun_prop] lemma POVar.measurable_condExpRatio (c : POVar P γ) (g h : P.Ω → ℝ) {μ : Measure P.Ω} : Measurable (c.condExpRatio g h μ) := by simp only [condexp_simps] exact (c.stronglyMeasurable_condExpGiven g).measurable.div (c.stronglyMeasurable_condExpGiven h).measurable -
stronglyMeasurable_condExpRatiolemma — condExpRatio is strongly measurable.hypothesesconclusionStronglyMeasurable (c.condExpRatio g h μ)Proof (Lean source)
@[fun_prop] lemma POVar.stronglyMeasurable_condExpRatio (c : POVar P γ) (g h : P.Ω → ℝ) {μ : Measure P.Ω} : StronglyMeasurable (c.condExpRatio g h μ) := (c.measurable_condExpRatio g h).stronglyMeasurable -
condExpRatio_eq_of_mullemma — Characterisation of condExpRatio via a product identity. If μ[g|σ(c)] = μ[h|σ(c)] · target a.s. and μ[h|σ(c)] ≠ 0 a.s., then condExpRatio c g h =ᵐ target. This is the reusable algebraic step for turning a conditional-expectation product identity into a ratio identity.hypothesesγ :sharedType u_1c :POVar P γg h target :P.Ω → ℝμ :Measure P.Ωhprod :c.condExpGiven g μ =ᵐ[μ] c.condExpGiven h μ * targethne :∀ᵐ ω ∂μ, c.condExpGiven h μ ω ≠ 0conclusionc.condExpRatio g h μ =ᵐ[μ] targetProof (Lean source)
lemma POVar.condExpRatio_eq_of_mul (c : POVar P γ) {g h target : P.Ω → ℝ} {μ : Measure P.Ω} (hprod : c.condExpGiven g μ =ᵐ[μ] c.condExpGiven h μ * target) (hne : ∀ᵐ ω ∂μ, c.condExpGiven h μ ω ≠ 0) : c.condExpRatio g h μ =ᵐ[μ] target := by simp only [condexp_simps] filter_upwards [hprod, hne] with ω hω hne simp only [Pi.mul_apply, condexp_simps] at hω hne rw [hω] field_simp -
condIndepFun_finite_of_measureReal_fiberstheorem — For a finite-valued conditioning map, if the conditioning map and the two conditioned maps are measurable and their ordinary real masses factor on every measurable pair of events inside every conditioning fiber, then the two maps are conditionally independent given the σ-algebra generated by the conditioning map.hypothesesΩ T A B :μ :X :Ω → ThX :f :Ω → Ahf :g :Ω → Bhg :hfactor :ifandthenμ.real (((f ⁻¹' s) ∩ (g ⁻¹' t)) ∩ X ⁻¹' {x}) * μ.real (X ⁻¹' {x})= μ.real ((f ⁻¹' s) ∩ X ⁻¹' {x}) * μ.real ((g ⁻¹' t) ∩ X ⁻¹' {x})conclusionProof (Lean source)
theorem condIndepFun_finite_of_measureReal_fibers {Ω T A B : Type*} [MeasurableSpace Ω] [StandardBorelSpace Ω] [Finite T] [MeasurableSpace T] [MeasurableSingletonClass T] [MeasurableSpace A] [MeasurableSpace B] (μ : Measure Ω) [IsFiniteMeasure μ] (X : Ω → T) (hX : Measurable X) (f : Ω → A) (hf : Measurable f) (g : Ω → B) (hg : Measurable g) (hfactor : ∀ (x : T) (s : Set A) (t : Set B), MeasurableSet s → MeasurableSet t → μ.real (((f ⁻¹' s) ∩ (g ⁻¹' t)) ∩ X ⁻¹' {x}) * μ.real (X ⁻¹' {x}) = μ.real ((f ⁻¹' s) ∩ X ⁻¹' {x}) * μ.real ((g ⁻¹' t) ∩ X ⁻¹' {x})) : CondIndepFun (comap X inferInstance) hX.comap_le f g μ := by rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hf hg] intro s t hs ht have hfg : MeasurableSet (f ⁻¹' s ∩ g ⁻¹' t) := (hf hs).inter (hg ht) have hleft := condExp_indicator_finite_comap μ X hX _ hfg have hfiber := condExp_indicator_finite_comap μ X hX _ (hf hs) have hgiber := condExp_indicator_finite_comap μ X hX _ (hg ht) filter_upwards [hleft, hfiber, hgiber] with ω hleftω hfω hgω rw [hleftω, hfω, hgω] unfold finiteCondProb let m := μ.real (X ⁻¹' {X ω}) by_cases hm : m = 0 · simp only [m] at hm simp [hm] · have hfac := hfactor (X ω) s t hs ht simp only [Set.inter_assoc] at hfac change m⁻¹ * μ.real (X ⁻¹' {X ω} ∩ (f ⁻¹' s ∩ g ⁻¹' t)) = (m⁻¹ * μ.real (X ⁻¹' {X ω} ∩ f ⁻¹' s)) * (m⁻¹ * μ.real (X ⁻¹' {X ω} ∩ g ⁻¹' t)) have hfac' : μ.real (X ⁻¹' {X ω} ∩ (f ⁻¹' s ∩ g ⁻¹' t)) * m = μ.real (X ⁻¹' {X ω} ∩ f ⁻¹' s) * μ.real (X ⁻¹' {X ω} ∩ g ⁻¹' t) := by simpa [m, Set.inter_comm, Set.inter_left_comm, Set.inter_assoc] using hfac field_simp simpa [mul_comm] using hfac'
EventCondExp 4 core · 14 supporting This file provides event-level conditional expectations for real-valued sample-space quantities, together with finite-partition, algebraic, and independence-based conditioning identities. ★ eventCondExp_eq_sum_condProb_mul_eventCondExp★ eventCondExp_eq_integral_of_IndepCF★ eventCondExp_of_consistency_IndepCF
Event-Level Conditional Expectations
This file provides event-level conditional expectations for real-valued sample-space quantities, together with finite-partition, algebraic, and independence-based conditioning identities. It supplies the event-conditioning tools used by potential-outcome identification arguments elsewhere in the library.
def eventCondExp reviewed
⚑ flagged
Causalean.PO
For a measurable sample space, a measure on that space, an event in the sample space, and a real-valued sample-space function, the event-level conditional expectation is the integral of the function over the event divided by the event's real-valued measure.
lemma eventCondExp_eq_sum_condProb_mul_eventCondExp reviewed
⚑ flagged
Causalean.PO
Totalized finite-partition identity for event-level averages. Fix a measurable event A and a finite family of pairwise disjoint measurable sets C i covering the whole space, such that each intersection A ∩ C i has finite measure, and let f be an integrable function. Then the event-level average of f on A equals the sum, over i, of the event-level average of f on A ∩ C i weighted by the ratio of the measure of A ∩ C i to the measure of A:
Formal statement
hypotheses
Ω :
Type u_1
ι :
Type*
Fintype ι
μ :
Measure Ω
A :
Set Ω
C :
ι → Set Ω
hAmeas :
hCmeas :
∀ i, MeasurableSet (C i)
hcov :
(⋃ i, C i) = univ
hAC_fin :
∀ i, μ (A ∩ C i) ≠ ⊤
f :
Ω → ℝ
hf :
Integrable f μ
conclusion
Proof (Lean source)
lemma eventCondExp_eq_sum_condProb_mul_eventCondExp
{ι : Type*} [Fintype ι] (μ : Measure Ω)
(A : Set Ω) (C : ι → Set Ω) (hAmeas : MeasurableSet A)
(hCmeas : ∀ i, MeasurableSet (C i))
(hdisj : Pairwise (onFun Disjoint C))
(hcov : (⋃ i, C i) = univ)
(hAC_fin : ∀ i, μ (A ∩ C i) ≠ ⊤)
(f : Ω → ℝ) (hf : Integrable f μ) :
eventCondExp μ A f
= ∑ i, (μ (A ∩ C i)).toReal / (μ A).toReal * eventCondExp μ (A ∩ C i) f := by
-- The cells `A ∩ C i` are measurable, pairwise disjoint, and cover `A`.
have hAC_meas : ∀ i, MeasurableSet (A ∩ C i) := fun i => hAmeas.inter (hCmeas i)
have hAC_disj : Pairwise (onFun Disjoint (fun i => A ∩ C i)) := by
intro i j hij
exact (hdisj hij).mono Set.inter_subset_right Set.inter_subset_right
have hAC_cov : (⋃ i, A ∩ C i) = A := by
rw [← Set.inter_iUnion, hcov, Set.inter_univ]
-- Step 1: `∫_A f = ∑ i, ∫_{A ∩ C i} f`.
have hsplit : ∫ ω in A, f ω ∂μ = ∑ i, ∫ ω in A ∩ C i, f ω ∂μ := by
have h := MeasureTheory.integral_iUnion_fintype hAC_meas hAC_disj
(fun _ => hf.integrableOn)
rwa [hAC_cov] at h
-- Step 2: each restricted integral is `μ(cell) · E[f | cell]`.
have hcell : ∀ i, ∫ ω in A ∩ C i, f ω ∂μ
= (μ (A ∩ C i)).toReal * eventCondExp μ (A ∩ C i) f := by
intro i
rw [mul_comm, ← eventCondExp_mul_measure_toReal μ (A ∩ C i) (hAC_fin i) f]
-- Assemble and divide through by `(μ A).toReal`.
have hLHS : eventCondExp μ A f = (∫ ω in A, f ω ∂μ) / (μ A).toReal := rfl
rw [hLHS, hsplit, Finset.sum_div]
refine Finset.sum_congr rfl (fun i _ => ?_)
rw [hcell i, mul_div_right_comm]
theorem eventCondExp_eq_integral_of_IndepCF reviewed
⚑ flagged
Causalean.PO.POSystem
Drop-of-conditioning (quotient form). Suppose a regimed variable rv is independent of a counterfactual bundle B, where h is a measurable function of the bundle's joint value and {x} is a measurable singleton in the range of rv. If the event {rv = x} has positive and finite measure, then the event-level conditional expectation of h composed with the bundle's joint value, given {rv = x}, equals the unconditional integral of the same composite.
Formal statement
hypotheses
α :
B :
μ :
Measure P.Ω
hInd :
P.IndepCF rv B μ
h :
(∀ i : Fin B.n, B.type i) → ℝ
hh_meas :
x :
α
hx :
MeasurableSet ({x} : Set α)
hμA_ne_zero :
μ (rv.value ⁻¹' {x}) ≠ 0
hμA_ne_top :
μ (rv.value ⁻¹' {x}) ≠ ⊤
conclusion
eventCondExp μ (rv.value ⁻¹' {x}) (fun ω => h (B.jointValue ω))
= ∫ ω, h (B.jointValue ω) ∂μ
Proof (Lean source)
theorem POSystem.eventCondExp_eq_integral_of_IndepCF
{α : Type*} [MeasurableSpace α]
{rv : RegimedVar P α} {B : POCFBundle P}
{μ : Measure P.Ω}
(hInd : P.IndepCF rv B μ)
{h : (∀ i : Fin B.n, B.type i) → ℝ}
(hh_meas : Measurable h) {x : α}
(hx : MeasurableSet ({x} : Set α))
(hμA_ne_zero : μ (rv.value ⁻¹' {x}) ≠ 0)
(hμA_ne_top : μ (rv.value ⁻¹' {x}) ≠ ⊤) :
eventCondExp μ (rv.value ⁻¹' {x}) (fun ω => h (B.jointValue ω))
= ∫ ω, h (B.jointValue ω) ∂μ := by
simp only [condexp_simps]
rw [POSystem.integral_restrict_value_eq_mul_of_IndepCF hInd hh_meas x hx]
have hpos : (μ (rv.value ⁻¹' {x})).toReal ≠ 0 := by
rw [ENNReal.toReal_ne_zero]
exact ⟨hμA_ne_zero, hμA_ne_top⟩
field_simp
theorem eventCondExp_of_consistency_IndepCF reviewed
⚑ flagged
Causalean.PO.POSystem
Drop-of-conditioning on an event, given a bundle relabeling of the integrand. Suppose a factual variable a is independent of a counterfactual bundle B, where h is a measurable function of the bundle's joint value and {x} is a measurable singleton in the range of a. If the factual integrand factualF agrees, almost everywhere on the event {a = x}, with h composed with the bundle's joint value, and that event has positive and finite measure, then the event-level conditional expectation of factualF given {a = x} equals the unconditional integral of h composed with the bundle's joint value.
Formal statement
hypotheses
α :
B :
μ :
Measure P.Ω
hInd :
P.IndepCF (RegimedVar.ofFactual a) B μ
factualF :
P.Ω → ℝ
h :
(∀ i : Fin B.n, B.type i) → ℝ
hh_meas :
x :
α
hx :
MeasurableSet ({x} : Set α)
hF_eq :
factualF =ᵐ[μ.restrict (a.event x)] fun ω => h (B.jointValue ω)
hμA_ne_zero :
μ (a.event x) ≠ 0
hμA_ne_top :
μ (a.event x) ≠ ⊤
conclusion
eventCondExp μ (a.event x) factualF = ∫ ω, h (B.jointValue ω) ∂μ
Proof (Lean source)
theorem POSystem.eventCondExp_of_consistency_IndepCF
{α : Type*} [MeasurableSpace α]
{a : POVar P α} {B : POCFBundle P}
{μ : Measure P.Ω}
(hInd : P.IndepCF (RegimedVar.ofFactual a) B μ)
{factualF : P.Ω → ℝ}
{h : (∀ i : Fin B.n, B.type i) → ℝ} (hh_meas : Measurable h)
{x : α}
(hx : MeasurableSet ({x} : Set α))
(hF_eq : factualF =ᵐ[μ.restrict (a.event x)] fun ω => h (B.jointValue ω))
(hμA_ne_zero : μ (a.event x) ≠ 0)
(hμA_ne_top : μ (a.event x) ≠ ⊤) :
eventCondExp μ (a.event x) factualF = ∫ ω, h (B.jointValue ω) ∂μ := by
simp only [condexp_simps]
rw [MeasureTheory.integral_congr_ae hF_eq]
rw [POSystem.integral_event_eq_mul_of_IndepCF hInd hh_meas x hx]
have hpos : (μ (a.event x)).toReal ≠ 0 := by
rw [ENNReal.toReal_ne_zero]
exact ⟨hμA_ne_zero, hμA_ne_top⟩
field_simp
14 supporting declarations (lemmas, instances)
-
eventCondExp_eqlemma — The average of a real-valued quantity over an event is its integral restricted to that event, divided by the event's real-valued mass.hypothesesconclusioneventCondExp μ A g = (∫ ω in A, g ω ∂μ) / (μ A).toRealProof (Lean source)
@[condexp_simps] lemma eventCondExp_eq (μ : Measure Ω) (A : Set Ω) (g : Ω → ℝ) : eventCondExp μ A g = (∫ ω in A, g ω ∂μ) / (μ A).toReal := rfl -
eventCondExp_mul_measure_toReallemma — eventCondExp μ A f · (μ A).toReal = ∫_A f, including the zero-measure case where both sides collapse to 0.hypothesesconclusioneventCondExp μ A f * (μ A).toReal = ∫ ω in A, f ω ∂μProof (Lean source)
lemma eventCondExp_mul_measure_toReal (μ : Measure Ω) (A : Set Ω) (hA_fin : μ A ≠ ⊤) (f : Ω → ℝ) : eventCondExp μ A f * (μ A).toReal = ∫ ω in A, f ω ∂μ := by simp only [condexp_simps] by_cases h0 : (μ A).toReal = 0 · rw [h0, mul_zero] have hμ0 : μ A = 0 := by rcases (ENNReal.toReal_eq_zero_iff _).mp h0 with h | h · exact h · exact absurd h hA_fin exact (MeasureTheory.setIntegral_measure_zero f hμ0).symm · field_simp -
integral_eq_sum_measure_mul_eventCondExplemma — Finite-partition total law. For any disjoint covering of univ by a Fintype-indexed family of measurable sets, ∫ f = ∑ i, (μ (A i)).toReal · eventCondExp μ (A i) f.hypothesesΩ :sharedType u_1ι :Type*Fintype ιμ :A :ι → Set Ωhmeas :∀ i, MeasurableSet (A i)hcov :(⋃ i, A i) = univf :Ω → ℝhf :Integrable f μconclusion∫ ω, f ω ∂μ = ∑ i, (μ (A i)).toReal * eventCondExp μ (A i) fProof (Lean source)
lemma integral_eq_sum_measure_mul_eventCondExp {ι : Type*} [Fintype ι] (μ : Measure Ω) [IsFiniteMeasure μ] (A : ι → Set Ω) (hmeas : ∀ i, MeasurableSet (A i)) (hdisj : Pairwise (onFun Disjoint A)) (hcov : (⋃ i, A i) = univ) (f : Ω → ℝ) (hf : Integrable f μ) : ∫ ω, f ω ∂μ = ∑ i, (μ (A i)).toReal * eventCondExp μ (A i) f := by have hsplit : ∫ ω in (⋃ i, A i), f ω ∂μ = ∑ i, ∫ ω in A i, f ω ∂μ := MeasureTheory.integral_iUnion_fintype hmeas hdisj (fun _ => hf.integrableOn) have hcov' : ∫ ω, f ω ∂μ = ∑ i, ∫ ω in A i, f ω ∂μ := by rw [← hsplit, hcov, setIntegral_univ] rw [hcov'] refine Finset.sum_congr rfl (fun i _ => ?_) rw [mul_comm, ← eventCondExp_mul_measure_toReal μ (A i) (measure_ne_top _ _) f] -
eventCondExp_congr_aelemma — a.e.-equal integrands have equal event-level conditional expectations.hypothesesconclusioneventCondExp μ A f = eventCondExp μ A gProof (Lean source)
lemma eventCondExp_congr_ae (μ : Measure Ω) (A : Set Ω) {f g : Ω → ℝ} (h : f =ᵐ[μ.restrict A] g) : eventCondExp μ A f = eventCondExp μ A g := by simp only [condexp_simps] rw [MeasureTheory.integral_congr_ae h] -
eventCondExp_congr_onlemma — Equal-on-A integrands have equal event-level conditional expectations. This specialises eventCondExp_congr_ae to a pointwise identity on a measurable set A.hypothesesconclusioneventCondExp μ A f = eventCondExp μ A gProof (Lean source)
lemma eventCondExp_congr_on (μ : Measure Ω) {A : Set Ω} (hA : MeasurableSet A) {f g : Ω → ℝ} (h : ∀ ω ∈ A, f ω = g ω) : eventCondExp μ A f = eventCondExp μ A g := by simp only [condexp_simps] congr 1 exact MeasureTheory.setIntegral_congr_fun hA h -
eventCondExp_mono_aelemma — Monotonicity of eventCondExp under an a.e. inequality of integrable functions.hypothesesΩ :sharedType u_1μ :Measure ΩA :Set Ωf g :Ω → ℝhf :IntegrableOn f A μhg :IntegrableOn g A μhfg :f ≤ᵐ[μ.restrict A] gconclusioneventCondExp μ A f ≤ eventCondExp μ A gProof (Lean source)
lemma eventCondExp_mono_ae (μ : Measure Ω) {A : Set Ω} {f g : Ω → ℝ} (hf : IntegrableOn f A μ) (hg : IntegrableOn g A μ) (hfg : f ≤ᵐ[μ.restrict A] g) : eventCondExp μ A f ≤ eventCondExp μ A g := by simp only [condexp_simps] have hint_le : ∫ ω in A, f ω ∂μ ≤ ∫ ω in A, g ω ∂μ := MeasureTheory.setIntegral_mono_ae_restrict hf hg hfg have hnn : (0 : ℝ) ≤ (μ A).toReal := ENNReal.toReal_nonneg exact div_le_div_of_nonneg_right hint_le hnn -
eventCondExp_addlemma — Event-level conditional expectation is additive for integrable summands on the event.hypothesesΩ :sharedType u_1μ :Measure ΩA :Set Ωg₁ g₂ :Ω → ℝh₁ :IntegrableOn g₁ A μh₂ :IntegrableOn g₂ A μconclusionProof (Lean source)
lemma eventCondExp_add (μ : Measure Ω) (A : Set Ω) {g₁ g₂ : Ω → ℝ} (h₁ : IntegrableOn g₁ A μ) (h₂ : IntegrableOn g₂ A μ) : eventCondExp μ A (g₁ + g₂) = eventCondExp μ A g₁ + eventCondExp μ A g₂ := by simp only [condexp_simps, Pi.add_apply, integral_add h₁ h₂, add_div] -
eventCondExp_sublemma — Event-level conditional expectation is additive over subtraction for integrable functions on the event.hypothesesΩ :sharedType u_1μ :Measure ΩA :Set Ωg₁ g₂ :Ω → ℝh₁ :IntegrableOn g₁ A μh₂ :IntegrableOn g₂ A μconclusionProof (Lean source)
lemma eventCondExp_sub (μ : Measure Ω) (A : Set Ω) {g₁ g₂ : Ω → ℝ} (h₁ : IntegrableOn g₁ A μ) (h₂ : IntegrableOn g₂ A μ) : eventCondExp μ A (g₁ - g₂) = eventCondExp μ A g₁ - eventCondExp μ A g₂ := by simp only [condexp_simps, Pi.sub_apply, integral_sub h₁ h₂, sub_div] -
eventCondExp_smullemma — Event-level conditional expectation is homogeneous with respect to real scalar multiplication.hypothesesconclusioneventCondExp μ A (fun ω => c * g ω) = c * eventCondExp μ A gProof (Lean source)
lemma eventCondExp_smul (μ : Measure Ω) (A : Set Ω) (c : ℝ) (g : Ω → ℝ) : eventCondExp μ A (fun ω => c * g ω) = c * eventCondExp μ A g := by simp only [condexp_simps, MeasureTheory.integral_const_mul, mul_div_assoc] -
eventCondExp_of_ae_eq_IndepFuntheorem — Consistency + drop-of-conditioning for plain IndepFun. If z is independent of a counterfactual bundle B, and a factual integrand agrees with a measurable projection h ∘ B a.e. on the cell {z = x}, then its event-level conditional expectation on that cell equals the unconditional integral of the projection.hypothesesΩ :sharedType u_1α β :μ :Measure Ωz :Ω → αB :Ω → βhInd :IndepFun z B μhz :hB :factualF :Ω → ℝh :β → ℝhh_meas :x :αhx :MeasurableSet ({x} : Set α)hF_eq :factualF =ᵐ[μ.restrict (z ⁻¹' {x})] fun ω => h (B ω)hμA_ne_zero :(μ (z ⁻¹' {x})).toReal ≠ 0conclusioneventCondExp μ (z ⁻¹' {x}) factualF = ∫ ω, h (B ω) ∂μProof (Lean source)
theorem eventCondExp_of_ae_eq_IndepFun {α β : Type*} [MeasurableSpace α] [MeasurableSpace β] {μ : Measure Ω} {z : Ω → α} {B : Ω → β} (hInd : IndepFun z B μ) (hz : Measurable z) (hB : Measurable B) {factualF : Ω → ℝ} {h : β → ℝ} (hh_meas : Measurable h) {x : α} (hx : MeasurableSet ({x} : Set α)) (hF_eq : factualF =ᵐ[μ.restrict (z ⁻¹' {x})] fun ω => h (B ω)) (hμA_ne_zero : (μ (z ⁻¹' {x})).toReal ≠ 0) : eventCondExp μ (z ⁻¹' {x}) factualF = ∫ ω, h (B ω) ∂μ := by simp only [condexp_simps] rw [MeasureTheory.integral_congr_ae hF_eq] rw [hInd.integral_restrict_preimage_eq_mul hz.aemeasurable hB.aemeasurable hx (hz hx) hh_meas.aestronglyMeasurable] field_simp -
integral_restrict_value_eq_mul_of_IndepCFtheorem — Drop-of-conditioning (multiplied form). If a regimed variable rv is independent of the counterfactual bundle B, then the integral of h ∘ B.jointValue over the preimage rv.value ⁻¹' {x} factors as (μ (rv.value ⁻¹' {x})).toReal * ∫ h ∘ B.jointValue ∂μ.hypothesesα :B :μ :Measure P.ΩhInd :P.IndepCF rv B μh :(∀ i : Fin B.n, B.type i) → ℝhh_meas :x :αhx :MeasurableSet ({x} : Set α)conclusion∫ ω in rv.value ⁻¹' {x}, h (B.jointValue ω) ∂μ= (μ (rv.value ⁻¹' {x})).toReal * ∫ ω, h (B.jointValue ω) ∂μProof (Lean source)
theorem POSystem.integral_restrict_value_eq_mul_of_IndepCF {α : Type*} [MeasurableSpace α] {rv : RegimedVar P α} {B : POCFBundle P} {μ : Measure P.Ω} (hInd : P.IndepCF rv B μ) {h : (∀ i : Fin B.n, B.type i) → ℝ} (hh_meas : Measurable h) (x : α) (hx : MeasurableSet ({x} : Set α)) : ∫ ω in rv.value ⁻¹' {x}, h (B.jointValue ω) ∂μ = (μ (rv.value ⁻¹' {x})).toReal * ∫ ω, h (B.jointValue ω) ∂μ := hInd.toIndepFun.integral_restrict_preimage_eq_mul rv.measurable_value.aemeasurable B.measurable_jointValue.aemeasurable hx (rv.measurable_value hx) hh_meas.aestronglyMeasurable -
integral_event_eq_mul_of_IndepCFtheorem — Drop-of-conditioning for the factual event. Specialisation of POSystem.integral_restrict_value_eq_mul_of_IndepCF to a factual POVar, using POVar.event directly.hypothesesα :B :μ :Measure P.ΩhInd :P.IndepCF (RegimedVar.ofFactual a) B μh :(∀ i : Fin B.n, B.type i) → ℝhh_meas :x :αhx :MeasurableSet ({x} : Set α)conclusion∫ ω in a.event x, h (B.jointValue ω) ∂μ= (μ (a.event x)).toReal * ∫ ω, h (B.jointValue ω) ∂μProof (Lean source)
theorem POSystem.integral_event_eq_mul_of_IndepCF {α : Type*} [MeasurableSpace α] {a : POVar P α} {B : POCFBundle P} {μ : Measure P.Ω} (hInd : P.IndepCF (RegimedVar.ofFactual a) B μ) {h : (∀ i : Fin B.n, B.type i) → ℝ} (hh_meas : Measurable h) (x : α) (hx : MeasurableSet ({x} : Set α)) : ∫ ω in a.event x, h (B.jointValue ω) ∂μ = (μ (a.event x)).toReal * ∫ ω, h (B.jointValue ω) ∂μ := by -- `a.event x = (RegimedVar.ofFactual a).value ⁻¹' {x}` by definition, since -- `(ofFactual a).value = a.cf Regime.empty = a.factual` and -- `a.event x = a.factual ⁻¹' {x}`. have hev : a.event x = (RegimedVar.ofFactual a).value ⁻¹' {x} := by rfl rw [hev] simpa using (POSystem.integral_restrict_value_eq_mul_of_IndepCF hInd hh_meas x hx) -
eventCondExp_event_eq_integral_of_IndepCFtheorem — Drop-of-conditioning on factual events (quotient form). Specialisation of the above to the factual event a.event x.hypothesesα :B :μ :Measure P.ΩhInd :P.IndepCF (RegimedVar.ofFactual a) B μh :(∀ i : Fin B.n, B.type i) → ℝhh_meas :x :αhx :MeasurableSet ({x} : Set α)hμA_ne_zero :μ (a.event x) ≠ 0hμA_ne_top :μ (a.event x) ≠ ⊤conclusioneventCondExp μ (a.event x) (fun ω => h (B.jointValue ω)) = ∫ ω, h (B.jointValue ω) ∂μProof (Lean source)
theorem POSystem.eventCondExp_event_eq_integral_of_IndepCF {α : Type*} [MeasurableSpace α] {a : POVar P α} {B : POCFBundle P} {μ : Measure P.Ω} (hInd : P.IndepCF (RegimedVar.ofFactual a) B μ) {h : (∀ i : Fin B.n, B.type i) → ℝ} (hh_meas : Measurable h) {x : α} (hx : MeasurableSet ({x} : Set α)) (hμA_ne_zero : μ (a.event x) ≠ 0) (hμA_ne_top : μ (a.event x) ≠ ⊤) : eventCondExp μ (a.event x) (fun ω => h (B.jointValue ω)) = ∫ ω, h (B.jointValue ω) ∂μ := by have hev : a.event x = (RegimedVar.ofFactual a).value ⁻¹' {x} := rfl rw [hev] at hμA_ne_zero hμA_ne_top ⊢ exact POSystem.eventCondExp_eq_integral_of_IndepCF hInd hh_meas hx hμA_ne_zero hμA_ne_top -
eventCondExp_cfUnder_eq_factual_on_eventtheorem — Consistency-on-event for eventCondExp. Generic consumer of POVar.cf_eq_factual_on_event: on the event {a = a₀}, the counterfactual y.cfUnder a a₀ agrees with y.factual pointwise, so their conditional means on that event coincide. This is the shared rewrite underlying Manski MTR/MTS and (via the finite-partition total law) the integrated MIV bounds.hypothesesP :β :Type*hC :P.Consistencyy :POVar P ℝa :POVar P βa₀ :βha₀ :MeasurableSet (a.event a₀)hvw :y.v ≠ a.vμ :Measure P.ΩconclusioneventCondExp μ (a.event a₀) (y.cfUnder a a₀) = eventCondExp μ (a.event a₀) y.factualProof (Lean source)
theorem POVar.eventCondExp_cfUnder_eq_factual_on_event {P : POSystem} {β : Type*} [MeasurableSpace β] (hC : P.Consistency) (y : POVar P ℝ) (a : POVar P β) (a₀ : β) (ha₀ : MeasurableSet (a.event a₀)) (hvw : y.v ≠ a.v) (μ : Measure P.Ω) : eventCondExp μ (a.event a₀) (y.cfUnder a a₀) = eventCondExp μ (a.event a₀) y.factual := by simp only [condexp_simps] congr 1 refine MeasureTheory.setIntegral_congr_fun ha₀ ?_ intro ω hω exact POVar.cf_eq_factual_on_event hC y a a₀ hvw hω
EventCondExpBundle 2 core · 0 supporting This file extends the event-level conditional-expectation workhorse to conditioning on a finite bundle of potential-outcome variables. ★ condExpGiven_mul_of_consistency_CondIndepCFBundle★ condExpRatio_of_consistency_CondIndepCFBundle
Bundle-Conditional Event Expectations
This file extends the event-level conditional-expectation workhorse to conditioning on a finite bundle of potential-outcome variables. It provides the product and ratio forms needed for dynamic local-average-treatment-effect bridge arguments.
The theorem POCFBundle.condExpGiven_mul_of_consistency_CondIndepCFBundle
turns bundle-conditional independence and a consistency-on-event product
identity into a factorization of bundle conditional expectations. The theorem
POCFBundle.condExpRatio_of_consistency_CondIndepCFBundle divides that
factorization by the conditional event probability under an a.e. nonzero
denominator assumption.
theorem condExpGiven_mul_of_consistency_CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POCFBundle
Bundle product-form workhorse (analogue of POSystem.eventCondExp_of_consistency_IndepCF). Suppose a factual variable a is conditionally independent, given the σ-algebra of a bundle C, of a counterfactual bundle B, where h is a measurable function whose composite with B's joint value is integrable, and {x} is a measurable singleton in the range of a. If the factual integrand factualF times the indicator of {a = x} agrees almost everywhere with h composed with B's joint value, times the same indicator, then the bundle conditional expectation, given C, of factualF times the indicator of {a = x} factorises almost everywhere as the bundle conditional expectation of h composed with B's joint value, times the bundle conditional expectation of the indicator of {a = x}:
Formal statement
hypotheses
α :
hCI :
P.CondIndepCFBundle (RegimedVar.ofFactual a) B C P.μ
factualF :
P.Ω → ℝ
h :
(∀ i, B.type i) → ℝ
hh_meas :
hh_int :
Integrable (fun ω => h (B.jointValue ω)) P.μ
x :
α
hx :
MeasurableSet ({x} : Set α)
hF_eq :
(fun ω => factualF ω * a.indicator x ω)
=ᵐ[P.μ] fun ω => h (B.jointValue ω) * a.indicator x ω
conclusion
C.condExpGiven (fun ω => factualF ω * a.indicator x ω) P.μ
=ᵐ[P.μ] fun ω => C.condExpGiven (fun ω' => h (B.jointValue ω')) P.μ ω * C.condExpGiven (a.indicator x) P.μ ω
Proof (Lean source)
theorem condExpGiven_mul_of_consistency_CondIndepCFBundle
[StandardBorelSpace P.Ω]
{α : Type*} [MeasurableSpace α]
{a : POVar P α}
(hCI : P.CondIndepCFBundle (RegimedVar.ofFactual a) B C P.μ)
{factualF : P.Ω → ℝ}
{h : (∀ i, B.type i) → ℝ} (hh_meas : Measurable h)
(hh_int : Integrable (fun ω => h (B.jointValue ω)) P.μ)
{x : α} (hx : MeasurableSet ({x} : Set α))
(hF_eq : (fun ω => factualF ω * a.indicator x ω) =ᵐ[P.μ]
fun ω => h (B.jointValue ω) * a.indicator x ω) :
C.condExpGiven (fun ω => factualF ω * a.indicator x ω) P.μ
=ᵐ[P.μ]
fun ω => C.condExpGiven (fun ω' => h (B.jointValue ω')) P.μ ω
* C.condExpGiven (a.indicator x) P.μ ω := by
let u : α → ℝ := ({x} : Set α).indicator (fun _ => (1 : ℝ))
have hu_meas : Measurable u :=
measurable_const.indicator hx
have hu_eq : (fun ω => u (a.factual ω)) = a.indicator x := by
funext ω
unfold POVar.indicator
by_cases hω : a.factual ω = x
· have h1 : a.factual ω ∈ ({x} : Set α) := hω
have h2 : ω ∈ a.event x := hω
rw [show u (a.factual ω) = (1 : ℝ) from Set.indicator_of_mem h1 _,
Set.indicator_of_mem h2]
· have h1 : a.factual ω ∉ ({x} : Set α) := hω
have h2 : ω ∉ a.event x := hω
rw [show u (a.factual ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _,
Set.indicator_of_notMem h2]
have huv_int : Integrable
(fun ω => u (a.factual ω) * h (B.jointValue ω)) P.μ := by
have hEq : (fun ω => u (a.factual ω) * h (B.jointValue ω)) =
(fun ω => a.indicator x ω * h (B.jointValue ω)) := by
funext ω
rw [congr_fun hu_eq ω]
rw [hEq]
refine hh_int.mono
((a.measurable_indicator x hx).mul
(hh_meas.comp B.measurable_jointValue)).aestronglyMeasurable ?_
refine Filter.Eventually.of_forall (fun ω => ?_)
rcases a.indicator_eq_one_or_zero x ω with hω | hω <;> simp [hω]
have hfact :
P.μ[fun ω => u (a.factual ω) * h (B.jointValue ω) | C.sigma]
=ᵐ[P.μ]
P.μ[fun ω => u (a.factual ω) | C.sigma]
* P.μ[fun ω => h (B.jointValue ω) | C.sigma] :=
condExp_mul_of_condIndep (μ := P.μ)
(m := C.sigma) C.sigma_le
(f := a.factual) (g := B.jointValue)
a.measurable_factual B.measurable_jointValue hCI.toCondIndepFun
(u := u) (v := h) hu_meas hh_meas
(by
rw [hu_eq]
exact a.integrable_indicator x hx) hh_int huv_int
have hfact' :
C.condExpGiven (fun ω => h (B.jointValue ω) * a.indicator x ω) P.μ
=ᵐ[P.μ]
fun ω => C.condExpGiven (fun ω' => h (B.jointValue ω')) P.μ ω
* C.condExpGiven (a.indicator x) P.μ ω := by
unfold POCFBundle.condExpGiven
have hprod_rw :
(fun ω => u (a.factual ω) * h (B.jointValue ω)) =
(fun ω => h (B.jointValue ω) * a.indicator x ω) := by
funext ω
rw [congr_fun hu_eq ω]
ring
rw [hprod_rw, hu_eq] at hfact
filter_upwards [hfact] with ω hω
simpa [Pi.mul_apply, mul_comm] using hω
exact (C.condExpGiven_congr_ae hF_eq).trans hfact'
theorem condExpRatio_of_consistency_CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POCFBundle
Bundle ratio-form workhorse: ratio version of condExpGiven_mul_of_consistency_CondIndepCFBundle. Under the same hypotheses as that theorem — bundle-conditional independence of a from B given C, a measurable and integrable composite h ∘ B.jointValue, a measurable singleton {x}, and the consistency-on-event product identity — plus an almost-surely nonzero bundle-conditional probability of {a = x}, the conditional ratio condExpRatio (factualF · 1_{a=x}) (1_{a=x}) collapses almost everywhere to the bundle conditional mean of h ∘ B.jointValue.
Formal statement
hypotheses
α :
hCI :
P.CondIndepCFBundle (RegimedVar.ofFactual a) B C P.μ
factualF :
P.Ω → ℝ
h :
(∀ i, B.type i) → ℝ
hh_meas :
hh_int :
Integrable (fun ω => h (B.jointValue ω)) P.μ
x :
α
hx :
MeasurableSet ({x} : Set α)
hF_eq :
(fun ω => factualF ω * a.indicator x ω)
=ᵐ[P.μ] fun ω => h (B.jointValue ω) * a.indicator x ω
hOver :
∀ᵐ ω ∂P.μ, C.condExpGiven (a.indicator x) P.μ ω ≠ 0
conclusion
C.condExpRatio (fun ω => factualF ω * a.indicator x ω) (a.indicator x) P.μ
=ᵐ[P.μ] C.condExpGiven (fun ω' => h (B.jointValue ω')) P.μ
Proof (Lean source)
theorem condExpRatio_of_consistency_CondIndepCFBundle
[StandardBorelSpace P.Ω]
{α : Type*} [MeasurableSpace α]
{a : POVar P α}
(hCI : P.CondIndepCFBundle (RegimedVar.ofFactual a) B C P.μ)
{factualF : P.Ω → ℝ}
{h : (∀ i, B.type i) → ℝ} (hh_meas : Measurable h)
(hh_int : Integrable (fun ω => h (B.jointValue ω)) P.μ)
{x : α} (hx : MeasurableSet ({x} : Set α))
(hF_eq : (fun ω => factualF ω * a.indicator x ω) =ᵐ[P.μ]
fun ω => h (B.jointValue ω) * a.indicator x ω)
(hOver : ∀ᵐ ω ∂P.μ, C.condExpGiven (a.indicator x) P.μ ω ≠ 0) :
C.condExpRatio (fun ω => factualF ω * a.indicator x ω) (a.indicator x) P.μ
=ᵐ[P.μ]
C.condExpGiven (fun ω' => h (B.jointValue ω')) P.μ := by
refine C.condExpRatio_eq_of_mul ?_ hOver
filter_upwards [condExpGiven_mul_of_consistency_CondIndepCFBundle B C
hCI hh_meas hh_int hx hF_eq] with ω hω
simpa [Pi.mul_apply, mul_comm] using hω