PO.Conditioning
Conditioning machinery for potential outcomes: σ-algebras generated by regimed variables and reusable event-level conditional-expectation tooling.
Bundle 5 core · 13 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
The conditioning σ-algebra of a counterfactual bundle B (a finite collection of counterfactual variables over a potential-outcome system): the σ-algebra on the sample space generated by jointly observing all of B's counterfactual values — i.e. the information content of the whole bundle. It is the bundle analogue of the single-variable conditioning σ-algebra σ(c.factual) (the information in one variable c), generalised from one variable to the bundle's joint value map.
Definition (Lean source)
def condExpGiven reviewed
⚑ flagged
Causalean.PO.POCFBundle
The bundle conditional expectation averages a real-valued sample-space quantity given the sigma-algebra generated by the bundle's joint counterfactual-value map.
Definition (Lean source)
def condExpGiven (g : P.Ω → ℝ) (μ : Measure P.Ω := P.μ) : P.Ω → ℝ :=
μ[g | B.sigma]
def condExpRatio reviewed
⚑ flagged
Causalean.PO.POCFBundle
The bundle conditional-expectation ratio compares two real-valued sample-space quantities after conditioning on the sigma-algebra generated by the bundle's joint counterfactual-value map.
Definition (Lean source)
def condExpRatio (g h : P.Ω → ℝ) (μ : Measure P.Ω := P.μ) : P.Ω → ℝ :=
fun ω => (B.condExpGiven g μ ω) / (B.condExpGiven h μ ω)
def CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POSystem
A regimed potential-outcome variable and one counterfactual bundle are conditionally independent given the sigma-algebra generated by another counterfactual bundle's joint counterfactual-value map.
Definition (Lean source)
def POSystem.CondIndepCFBundle
(P : POSystem) [StandardBorelSpace P.Ω]
{α : Type*} [MeasurableSpace α]
(a : RegimedVar P α) (B : POCFBundle P) (C : POCFBundle P)
(μ : Measure P.Ω := P.μ) [IsFiniteMeasure μ] : Prop :=
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ψ
13 supporting declarations (lemmas, instances)
-
sigma_lelemma — The conditioning σ-algebra B.sigma is a sub-σ-algebra of the ambient σ-algebra on P.Ω.conclusionB.sigma ≤ (inferInstance : MeasurableSpace P.Ω)Proof (Lean source)
lemma sigma_le : B.sigma ≤ (inferInstance : MeasurableSpace P.Ω) := B.measurable_jointValue.comap_le -
stronglyMeasurable_condExpGiven_comaplemma — condExpGiven yields a function strongly measurable w.r.t. B.sigma.Proof (Lean source)
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.Proof (Lean source)
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.Proof (Lean source)
lemma integrable_condExpGiven (g : P.Ω → ℝ) {μ : Measure P.Ω} : Integrable (B.condExpGiven g μ) μ := by simpa [POCFBundle.condExpGiven] using (MeasureTheory.integrable_condExp (μ := μ) (m := B.sigma) (f := g)) -
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 [POCFBundle.condExpGiven] 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 [POCFBundle.condExpGiven] 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 [POCFBundle.condExpGiven] 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 unfold POCFBundle.condExpGiven exact MeasureTheory.condExp_congr_ae h -
measurable_condExpRatiolemma — The conditional-ratio function of two real integrands given a counterfactual bundle is measurable.Proof (Lean source)
lemma measurable_condExpRatio (g h : P.Ω → ℝ) {μ : Measure P.Ω} : Measurable (B.condExpRatio g h μ) := by unfold POCFBundle.condExpRatio 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.Proof (Lean source)
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 unfold POCFBundle.condExpRatio filter_upwards [hprod, hne] with ω hω hne simp only [Pi.mul_apply] at hω rw [hω] field_simp -
toCondIndepFunlemma — Bridge: CondIndepCFBundle unfolds to CondIndepFun w.r.t. C.sigma.hypothesesconclusionP.CondIndepCFBundle a B C μ → CondIndepFun 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 · 16 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 conditioning potential-outcome variable, a real-valued function on the sample space, and a measure on the sample space, this is the conditional expectation of that function given the σ-algebra generated by the factual value of the conditioning variable.
Definition (Lean source)
def POVar.condExpGiven (c : POVar P γ) (g : P.Ω → ℝ)
(μ : Measure P.Ω := P.μ) : P.Ω → ℝ :=
μ[g | comap c.factual inferInstance]
def condExpRatio reviewed
⚑ flagged
Causalean.PO.POVar
For a conditioning potential-outcome variable, two real-valued functions on the sample space, and a measure on the sample space, this is the pointwise ratio of the conditional expectation of the first function to the conditional expectation of the second function, both given the σ-algebra generated by the factual value of the conditioning variable.
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
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
unfold POVar.condExpGiven
exact (MeasureTheory.integral_condExp c.comap_factual_le).symm
have hIg : ∫ ω, g ω ∂μ = ∫ ω, c.condExpGiven g μ ω ∂μ := by
unfold POVar.condExpGiven
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')
16 supporting declarations (lemmas, instances)
-
comap_factual_lelemma — The conditioning σ-algebra σ(c.factual) is a sub-σ-algebra of the ambient σ-algebra on P.Ω.hypothesesc :POVar P γconclusioncomap 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)
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] -
condExpGiven_addlemma — Linearity of condExpGiven: additivity.hypothesesconclusionc.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 [POVar.condExpGiven] using MeasureTheory.condExp_add (μ := μ) hf hg (comap c.factual inferInstance) -
condExpGiven_sublemma — Linearity of condExpGiven: subtraction.hypothesesconclusionc.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 [POVar.condExpGiven] 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 [POVar.condExpGiven] using MeasureTheory.condExp_smul (μ := μ) k g (comap c.factual inferInstance) -
stronglyMeasurable_condExpGiven_comaplemma — condExpGiven yields a function strongly measurable w.r.t. σ(c.factual).hypothesesconclusionProof (Lean source)
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)
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.Proof (Lean source)
lemma POVar.integrable_condExpGiven (c : POVar P γ) (g : P.Ω → ℝ) {μ : Measure P.Ω} : Integrable (c.condExpGiven g μ) μ := by simpa [POVar.condExpGiven] 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)].hypothesesconclusionc.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 [POVar.condExpGiven] 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.hypothesesconclusionc.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 [POVar.condExpGiven] 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).hypothesesc :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 [POVar.condExpGiven] 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δ :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 [POVar.condExpGiven] using MeasureTheory.condExp_condExp_of_le (μ := μ) (f := g) h c₂.comap_factual_le -
measurable_condExpRatiolemma — condExpRatio is measurable (pointwise division of two strongly measurable functions is measurable).Proof (Lean source)
lemma POVar.measurable_condExpRatio (c : POVar P γ) (g h : P.Ω → ℝ) {μ : Measure P.Ω} : Measurable (c.condExpRatio g h μ) := by unfold POVar.condExpRatio 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)
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.hypothesesc :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 unfold POVar.condExpRatio filter_upwards [hprod, hne] with ω hω hne simp only [Pi.mul_apply] at hω rw [hω] field_simp
EventCondExp 4 core · 13 supporting This file packages conditioning on an event as a reusable event-level conditional expectation and proves finite-partition and drop-of-conditioning identities used throughout potential-outcome identification arguments. ★ eventCondExp_eq_sum_condProb_mul_eventCondExp★ eventCondExp_eq_integral_of_IndepCF★ eventCondExp_of_consistency_IndepCF
Event-Level Conditional Expectations
This file packages conditioning on an event as a reusable event-level conditional expectation and proves finite-partition and drop-of-conditioning identities used throughout potential-outcome identification arguments.
The API starts with eventCondExp, its measure identity, finite-partition
decompositions, congruence, monotonicity, and algebra lemmas. The main
potential-outcome workhorses are the IndepCF drop-of-conditioning theorems,
the consistency-on-event rewrite POVar.eventCondExp_cfUnder_eq_factual_on_event,
and POSystem.eventCondExp_of_consistency_IndepCF, which combines a supplied
event relabeling with independence.
def eventCondExp reviewed
⚑ flagged
Causalean.PO
Event-level conditional expectation is the average of a real-valued sample-space quantity over an event, computed as its integral over the event divided by the event's real mass.
Definition (Lean source)
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*
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
eventCondExp μ A f = ∑ i, (μ (A ∩ C i)).toReal / (μ A).toReal * eventCondExp μ (A ∩ C i) f
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
unfold eventCondExp
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
unfold eventCondExp
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
13 supporting declarations (lemmas, instances)
-
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 unfold eventCondExp 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ι :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 unfold eventCondExp 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 unfold eventCondExp congr 1 exact MeasureTheory.setIntegral_congr_fun hA h -
eventCondExp_mono_aelemma — Monotonicity of eventCondExp under an a.e. inequality of integrable functions.hypothesesμ :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 unfold eventCondExp 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.hypothesesconclusionProof (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 [eventCondExp, 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.hypothesesconclusionProof (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 [eventCondExp, 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 [eventCondExp, 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α β :μ :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 unfold eventCondExp 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 unfold eventCondExp 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ω