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★ 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 · 26 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 sigma-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 sigma-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')
26 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
EventCondExp 2 core · 4 supporting This file specializes normalized restricted integrals to potential-outcome variables. ★ eventCondExp_eq_integral_of_IndepCF★ eventCondExp_of_ae_eq_IndepCF
Event-Level Conditional Expectations
This file specializes normalized restricted integrals to potential-outcome variables. It provides
multiplied and quotient drop-of-conditioning identities under independence, a consistency-on-event
identity, and an eventwise relabeling workhorse. The general measure-theoretic definition and
algebra live in Causalean.Mathlib.Probability.FiniteCellConditionalMomentBridge.
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
normalizedRestrictedIntegral μ (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}) ≠ ⊤) :
normalizedRestrictedIntegral μ (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_ae_eq_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
normalizedRestrictedIntegral μ (a.event x) factualF = ∫ ω, h (B.jointValue ω) ∂μ
Proof (Lean source)
theorem POSystem.eventCondExp_of_ae_eq_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) ≠ ⊤) :
normalizedRestrictedIntegral μ (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
4 supporting declarations (lemmas, instances)
-
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) ≠ ⊤conclusionnormalizedRestrictedIntegral μ (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) ≠ ⊤) : normalizedRestrictedIntegral μ (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 an event for normalizedRestrictedIntegral. Given a consistent potential-outcome system, an outcome variable y, a conditioning variable a, a level a₀, and a measure μ, if the event {a = a₀} is measurable and y and a have distinct variable labels, then the normalized restricted integrals of the counterfactual and factual outcomes are equal. These totalized quantities are conditional means only when the event has positive finite measure.hypothesesP :β :Type*hC :P.Consistencyy :POVar P ℝa :POVar P βa₀ :βha₀ :MeasurableSet (a.event a₀)hvw :y.v ≠ a.vμ :Measure P.ΩconclusionnormalizedRestrictedIntegral μ (a.event a₀) (y.cfUnder a a₀)= normalizedRestrictedIntegral μ (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.Ω) : normalizedRestrictedIntegral μ (a.event a₀) (y.cfUnder a a₀) = normalizedRestrictedIntegral μ (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_indicator_ae_eq_CondIndepCFBundle★ condExpRatio_of_indicator_ae_eq_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_indicator_ae_eq_CondIndepCFBundle
turns bundle-conditional independence and an indicator-weighted product
identity into a factorization of bundle conditional expectations. The theorem
POCFBundle.condExpRatio_of_indicator_ae_eq_CondIndepCFBundle divides that
factorization by the conditional event probability under an a.e. nonzero
denominator assumption.
theorem condExpGiven_mul_of_indicator_ae_eq_CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POCFBundle
Bundle product-form workhorse (analogue of POSystem.eventCondExp_of_ae_eq_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_indicator_ae_eq_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_indicator_ae_eq_CondIndepCFBundle reviewed
⚑ flagged
Causalean.PO.POCFBundle
Bundle ratio-form workhorse: ratio version of condExpGiven_mul_of_indicator_ae_eq_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 an indicator-weighted almost-everywhere 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_indicator_ae_eq_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_indicator_ae_eq_CondIndepCFBundle B C
hCI hh_meas hh_int hx hF_eq] with ω hω
simpa [Pi.mul_apply, mul_comm] using hω