Estimation.CATE.Core
Core DR-Learner pseudo-outcome theory for CATE: conditional bias, directional derivatives, conditional-mean identities, and second-order bias.
PseudoOutcome 3 core · 1 supporting Defines doubly robust pseudo-outcomes for conditional average treatment effect estimation. ★ measurable_phi₀
Defines doubly robust pseudo-outcomes for conditional average treatment effect
estimation. The main definitions are phi_eta, the uncentered AIPW
pseudo-outcome at an arbitrary nuisance vector, and phi₀, its specialization
to the truth nuisance carried by a CATEEstimationSystem. The lemmas
measurable_phi_eta and measurable_phi₀ provide the measurability facts used
by the conditional-mean, bias, and orthogonal-learning developments.
def phi_eta reviewed
⚑ flagged
Causalean.Estimation.CATE
Uncentered AIPW pseudo-outcome (Kennedy's φ_η):
Definition (Lean source)
noncomputable def phi_eta (z : γ × Bool × ℝ) (η : NuisanceVec γ) : ℝ :=
BackdoorEstimationSystem.aipwMoment z η.μ_fn η.e_fn 0
def phi₀ reviewed
⚑ flagged
Causalean.Estimation.CATE
True DR pseudo-outcome: φ_0(z) := φ_{η_0}(z) where η_0 is the truth nuisance vector carried by the back-door substrate of S.
Definition (Lean source)
noncomputable def phi₀ (S : CATEEstimationSystem P γ) (z : γ × Bool × ℝ) : ℝ :=
phi_eta z S.toBackdoorEstimationSystem.η₀
lemma measurable_phi₀ reviewed
⚑ flagged
Causalean.Estimation.CATE
For a CATE estimation system, the true doubly-robust pseudo-outcome φ_0 is measurable as a function of the observed data.
Formal statement
Proof (Lean source)
lemma measurable_phi₀ (S : CATEEstimationSystem P γ) :
Measurable (fun z : γ × Bool × ℝ => phi₀ S z) := by
unfold phi₀
exact measurable_phi_eta _
1 supporting declaration (lemmas, instances)
-
measurable_phi_etalemma — The uncentered AIPW pseudo-outcome is measurable in the data argument.Proof (Lean source)
lemma measurable_phi_eta (η : NuisanceVec γ) : Measurable (fun z : γ × Bool × ℝ => phi_eta z η) := by unfold phi_eta BackdoorEstimationSystem.aipwMoment BackdoorEstimationSystem.indA BackdoorEstimationSystem.projX BackdoorEstimationSystem.projA BackdoorEstimationSystem.projY have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := by measurability have hμt : Measurable (fun z : γ × Bool × ℝ => η.μ_fn true z.1) := (η.μ_meas true).comp hx have hμf : Measurable (fun z : γ × Bool × ℝ => η.μ_fn false z.1) := (η.μ_meas false).comp hx have he : Measurable (fun z : γ × Bool × ℝ => η.e_fn z.1) := η.e_meas.comp hx have hind : Measurable (fun z : γ × Bool × ℝ => if z.2.1 = true then (1 : ℝ) else 0) := by have ha : Measurable (fun z : γ × Bool × ℝ => z.2.1) := by measurability exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp ha exact ((((hμt.sub hμf).add ((hind.div he).mul (hy.sub hμt))).sub (((measurable_const.sub hind).div (measurable_const.sub he)).mul (hy.sub hμf))).sub measurable_const)
PhiEtaDeriv 2 core · 1 supporting Computes directional derivatives for CATE doubly robust pseudo-outcome maps. ★ phi_eta_dir_deriv_tendsto
Computes directional derivatives for CATE doubly robust pseudo-outcome maps. The
definition phi_eta_dir_deriv gives the closed-form derivative in a nuisance
direction, measurable_phi_eta_dir_deriv proves measurability in the data
argument, and phi_eta_dir_deriv_tendsto proves convergence of the pointwise
difference quotient under strict overlap.
These derivative formulas are the analytic core of the CATE orthogonality and
second-order bias arguments, including the conditional mean-zero result for the
derivative at the truth in ConditionalBias.lean.
def phi_eta_dir_deriv reviewed
⚑ flagged
Causalean.Estimation.CATE
Closed-form directional derivative of phi_eta z η in η at g₀ along the direction v : NuisanceVec γ.
Definition (Lean source)
noncomputable def phi_eta_dir_deriv
(g₀ v : NuisanceVec γ) (z : γ × Bool × ℝ) : ℝ :=
(v.μ_fn true (projX z) - v.μ_fn false (projX z))
+ indA z * (- v.e_fn (projX z) / (g₀.e_fn (projX z))^2 *
(projY z - g₀.μ_fn true (projX z))
- 1 / g₀.e_fn (projX z) * v.μ_fn true (projX z))
- (1 - indA z) * (v.e_fn (projX z) / (1 - g₀.e_fn (projX z))^2 *
(projY z - g₀.μ_fn false (projX z))
- 1 / (1 - g₀.e_fn (projX z)) * v.μ_fn false (projX z))
theorem phi_eta_dir_deriv_tendsto reviewed
⚑ flagged
Causalean.Estimation.CATE
Pointwise convergence of the DR pseudo-outcome difference quotient. Fix an anchor nuisance pair g₀, a perturbation direction v, and a data point z. If ε is strictly positive and the anchor g₀ has propensity uniformly bounded in [ε, 1 − ε] for every covariate value, then as the step size t tends to 0 along nonzero values, the difference quotient (phi_eta z (g₀ + t•v) − phi_eta z g₀) / t converges to the closed-form directional derivative phi_eta_dir_deriv g₀ v z.
Formal statement
hypotheses
g₀ v :
ε :
ℝ
hε_pos :
0 < ε
h_overlap_g₀ :
g₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
z :
γ × Bool × ℝ
conclusion
Tendsto (fun t : ℝ => (phi_eta z (g₀ + t • v) - phi_eta z g₀) / t) (𝓝[≠] 0) (𝓝 (phi_eta_dir_deriv g₀ v z))
Proof (Lean source)
theorem phi_eta_dir_deriv_tendsto
(g₀ v : NuisanceVec γ) {ε : ℝ} (hε_pos : 0 < ε)
(h_overlap_g₀ : g₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε)
(z : γ × Bool × ℝ) :
Tendsto (fun t : ℝ => (phi_eta z (g₀ + t • v) - phi_eta z g₀) / t)
(𝓝[≠] 0) (𝓝 (phi_eta_dir_deriv g₀ v z)) := by
let x := projX z
let a := indA z
let y := projY z
let m1 := g₀.μ_fn true x
let m0 := g₀.μ_fn false x
let e := g₀.e_fn x
let dm1 := v.μ_fn true x
let dm0 := v.μ_fn false x
let de := v.e_fn x
have he_pos : 0 < e := by
exact lt_of_lt_of_le hε_pos (h_overlap_g₀ x).1
have he : e ≠ 0 := ne_of_gt he_pos
have h1e_pos : 0 < 1 - e := by
have he_lt_one : e < 1 := by
calc
e ≤ 1 - ε := by simpa [e, x] using (h_overlap_g₀ x).2
_ < 1 := sub_lt_self 1 hε_pos
exact sub_pos.mpr he_lt_one
have h1e : 1 - e ≠ 0 := ne_of_gt h1e_pos
have hderiv :
HasDerivAt
(fun t : ℝ => phi_eta z (g₀ + t • v))
(phi_eta_dir_deriv g₀ v z) 0 := by
change HasDerivAt
(fun t : ℝ =>
((m1 + t * dm1) - (m0 + t * dm0))
+ (a / (e + t * de)) * (y - (m1 + t * dm1))
- ((1 - a) / (1 - (e + t * de))) * (y - (m0 + t * dm0))
- 0)
(phi_eta_dir_deriv g₀ v z) 0
convert phi_eta_real_line_hasDerivAt m1 m0 e y a dm1 dm0 de he h1e using 1
unfold phi_eta_dir_deriv
dsimp [x, a, y, m1, m0, e, dm1, dm0, de]
have he' : g₀.e_fn (projX z) ≠ 0 := by simpa [e, x] using he
have h1e' : 1 - g₀.e_fn (projX z) ≠ 0 := by simpa [e, x] using h1e
field_simp [he', h1e', pow_two]
ring
simpa [div_eq_inv_mul] using hderiv.tendsto_slope_zero
1 supporting declaration (lemmas, instances)
-
measurable_phi_eta_dir_derivlemma — phi_eta_dir_deriv g₀ v is measurable in z.hypothesesg₀ v :conclusionProof (Lean source)
lemma measurable_phi_eta_dir_deriv (g₀ v : NuisanceVec γ) : Measurable (fun z : γ × Bool × ℝ => phi_eta_dir_deriv g₀ v z) := by unfold phi_eta_dir_deriv indA projX projA projY have hx : Measurable (fun z : γ × Bool × ℝ => z.1) := measurable_fst have hy : Measurable (fun z : γ × Bool × ℝ => z.2.2) := by measurability have hμvT : Measurable (fun z : γ × Bool × ℝ => v.μ_fn true z.1) := (v.μ_meas true).comp hx have hμvF : Measurable (fun z : γ × Bool × ℝ => v.μ_fn false z.1) := (v.μ_meas false).comp hx have hev : Measurable (fun z : γ × Bool × ℝ => v.e_fn z.1) := v.e_meas.comp hx have hμgT : Measurable (fun z : γ × Bool × ℝ => g₀.μ_fn true z.1) := (g₀.μ_meas true).comp hx have hμgF : Measurable (fun z : γ × Bool × ℝ => g₀.μ_fn false z.1) := (g₀.μ_meas false).comp hx have heg : Measurable (fun z : γ × Bool × ℝ => g₀.e_fn z.1) := g₀.e_meas.comp hx have hind : Measurable (fun z : γ × Bool × ℝ => if z.2.1 = true then (1 : ℝ) else 0) := by have ha : Measurable (fun z : γ × Bool × ℝ => z.2.1) := by measurability exact (Measurable.of_discrete (f := fun b : Bool => if b = true then (1 : ℝ) else 0)).comp ha have hbase : Measurable (fun z : γ × Bool × ℝ => v.μ_fn true z.1 - v.μ_fn false z.1) := hμvT.sub hμvF -- Inner bracket of the indA branch. have hbrA : Measurable (fun z : γ × Bool × ℝ => -v.e_fn z.1 / (g₀.e_fn z.1)^2 * (z.2.2 - g₀.μ_fn true z.1) - 1 / g₀.e_fn z.1 * v.μ_fn true z.1) := by have h1 : Measurable (fun z : γ × Bool × ℝ => -v.e_fn z.1 / (g₀.e_fn z.1)^2) := hev.neg.div (heg.pow_const 2) have h2 : Measurable (fun z : γ × Bool × ℝ => z.2.2 - g₀.μ_fn true z.1) := hy.sub hμgT have h3 : Measurable (fun z : γ × Bool × ℝ => (1 : ℝ) / g₀.e_fn z.1) := measurable_const.div heg exact (h1.mul h2).sub (h3.mul hμvT) -- Inner bracket of the (1-indA) branch. have hbrB : Measurable (fun z : γ × Bool × ℝ => v.e_fn z.1 / (1 - g₀.e_fn z.1)^2 * (z.2.2 - g₀.μ_fn false z.1) - 1 / (1 - g₀.e_fn z.1) * v.μ_fn false z.1) := by have h1m : Measurable (fun z : γ × Bool × ℝ => 1 - g₀.e_fn z.1) := measurable_const.sub heg have h1 : Measurable (fun z : γ × Bool × ℝ => v.e_fn z.1 / (1 - g₀.e_fn z.1)^2) := hev.div (h1m.pow_const 2) have h2 : Measurable (fun z : γ × Bool × ℝ => z.2.2 - g₀.μ_fn false z.1) := hy.sub hμgF have h3 : Measurable (fun z : γ × Bool × ℝ => (1 : ℝ) / (1 - g₀.e_fn z.1)) := measurable_const.div h1m exact (h1.mul h2).sub (h3.mul hμvF) exact (hbase.add (hind.mul hbrA)).sub ((measurable_const.sub hind).mul hbrB)
ConditionalBias 3 core · 4 supporting Derives closed-form conditional-bias and orthogonality formulas for CATE doubly robust pseudo-outcomes. ★ phi_eta_minus_phi₀_cond_exp★ phi_eta_minus_phi₀_at_x
Derives closed-form conditional-bias and orthogonality formulas for CATE doubly
robust pseudo-outcomes. The value-space function condBias records the
cross-product remainder, with measurable_condBias providing measurability.
The main theorem phi_eta_minus_phi₀_cond_exp identifies the σ(X)-conditional
mean of phi_eta - phi₀ with condBias, and phi_eta_minus_phi₀_at_x transports
that identity to the covariate law through the regular conditional
distribution. The double-robustness corollaries
condBias_zero_of_propensity_match and condBias_zero_of_outcome_match show the
remainder vanishes when either nuisance block is correct. The final theorem
cond_exp_phi_eta_dir_deriv_at_truth_zero proves the corresponding conditional
mean-zero statement for the directional derivative at the truth.
def condBias reviewed
⚑ flagged
Causalean.Estimation.CATE
The closed-form σ(X)-conditional bias of the DR pseudo-outcome contrast φ_η − φ_0, summed over the two treatment arms:
Definition (Lean source)
noncomputable def condBias (η η₀ : NuisanceVec γ) (x : γ) : ℝ :=
∑ a : Bool, ((η.e_fn x - η₀.e_fn x) * (η.μ_fn a x - η₀.μ_fn a x)) /
(if a then η.e_fn x else 1 - η.e_fn x)
theorem phi_eta_minus_phi₀_cond_exp reviewed
⚑ flagged
Causalean.Estimation.CATE
σ(X)-conditional bias identity for the DR pseudo-outcome (Kennedy / DR-Learner Proposition 2). Fix a candidate nuisance pair η. Under the back-door identification assumptions, if η's propensity is uniformly bounded in [ε, 1 − ε] for every covariate value, the truth nuisance likewise has propensity uniformly bounded in [ε, 1 − ε], ε is strictly positive, and each candidate outcome-regression arm, composed with the covariate, is integrable, then the σ(X)-conditional expectation of the DR pseudo-outcome contrast φ_η − φ_0 equals the closed-form cross-product remainder condBias η η₀, evaluated at the covariate, almost surely.
Formal statement
hypotheses
P :
IsFiniteMeasure P.μ
S :
hA :
S.toPOBackdoorSystem.Assumptions
η :
ε :
ℝ
h_overlap_η :
η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
h_overlap_η₀ :
S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
hε_pos :
0 < ε
Per-arm integrability of the candidate outcome regressions on Ω. Required to build per-summand integrability witnesses for the AIPW expansion (truth-side η₀-pieces are derivable from `μ_compat` + `cate_backdoor`, but the candidate η-side needs an explicit hypothesis).
h_μ_η_int :
∀ a : Bool, Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ
Proof (Lean source)
theorem phi_eta_minus_phi₀_cond_exp
{P : POSystem} [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
(S : CATEEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions)
(η : NuisanceVec γ) {ε : ℝ}
(h_overlap_η : η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε)
(h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈
BackdoorEstimationSystem.H_ε (γ := γ) ε)
(hε_pos : 0 < ε)
-- Per-arm integrability of the candidate outcome regressions on Ω.
-- Required to build per-summand integrability witnesses for the AIPW
-- expansion (truth-side η₀-pieces are derivable from `μ_compat` +
-- `cate_backdoor`, but the candidate η-side needs an explicit hypothesis).
(h_μ_η_int : ∀ a : Bool,
Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ) :
P.μ[fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)
| S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
(fun ω => condBias η S.toBackdoorEstimationSystem.η₀
(S.toBackdoorEstimationSystem.factualX ω)) := by
let X : P.Ω → γ := S.toPOBackdoorSystem.factualX
let Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY
let indT : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator true
let indF : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator false
let base : P.Ω → ℝ := fun ω =>
η.μ_fn true (X ω) - η.μ_fn false (X ω) -
(S.μ_val true (X ω) - S.μ_val false (X ω))
let BηT : P.Ω → ℝ := fun ω =>
(1 / η.e_fn (X ω)) *
(indT ω * (Y ω - η.μ_fn true (X ω)))
let B₀T : P.Ω → ℝ := fun ω =>
(1 / S.e_val (X ω)) *
(indT ω * (Y ω - S.μ_val true (X ω)))
let CηF : P.Ω → ℝ := fun ω =>
(1 / (1 - η.e_fn (X ω))) *
(indF ω * (Y ω - η.μ_fn false (X ω)))
let C₀F : P.Ω → ℝ := fun ω =>
(1 / (1 - S.e_val (X ω))) *
(indF ω * (Y ω - S.μ_val false (X ω)))
have hindA_true : ∀ ω, BackdoorEstimationSystem.indA
(S.toBackdoorEstimationSystem.factualZ ω) = indT ω := by
intro ω
by_cases hD : S.toPOBackdoorSystem.factualD ω = true
· have hInd : indT ω = 1 :=
S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD
simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA,
BackdoorEstimationSystem.projA, indT, hD, hInd]
· have hInd : indT ω = 0 :=
S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD
simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA,
BackdoorEstimationSystem.projA, indT, hD, hInd]
have hφ_eq :
(fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω))
= (fun ω => base ω + BηT ω - B₀T ω - CηF ω + C₀F ω) := by
funext ω
have hind_true_z :
BackdoorEstimationSystem.indA
(S.toPOBackdoorSystem.factualX ω,
S.toPOBackdoorSystem.factualD ω,
S.toPOBackdoorSystem.factualY ω)
= indT ω := by
simpa [BackdoorEstimationSystem.factualZ] using hindA_true ω
have hind_not : 1 - indT ω = indF ω := by
have hsum : indT ω + indF ω = 1 :=
S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω
linarith
simp [base, BηT, B₀T, CηF, C₀F, X, Y, indT, indF, phi₀, phi_eta,
BackdoorEstimationSystem.aipwMoment, BackdoorEstimationSystem.factualZ,
BackdoorEstimationSystem.projX, BackdoorEstimationSystem.projY,
BackdoorEstimationSystem.η₀, hind_true_z, hind_not, mul_assoc, mul_comm,
sub_eq_add_neg, add_assoc, add_comm]
ring_nf
have hμ_val_int : ∀ d : Bool, Integrable (fun ω => S.μ_val d (X ω)) P.μ := by
intro d
have hcate_int : Integrable (S.toPOBackdoorSystem.CATE d) P.μ := by
unfold POBackdoorSystem.CATE
exact MeasureTheory.integrable_condExp
exact hcate_int.congr (S.μ_compat hA d)
have hbase_int : Integrable base P.μ := by
have hη := (h_μ_η_int true).sub (h_μ_η_int false)
have hμ := (hμ_val_int true).sub (hμ_val_int false)
refine (hη.sub hμ).congr ?_
exact Filter.Eventually.of_forall (fun ω => by simp [base, X])
have hbase_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] base := by
change StronglyMeasurable[
comap S.toPOBackdoorSystem.factualX inferInstance]
(fun ω =>
η.μ_fn true (S.toPOBackdoorSystem.factualX ω) -
η.μ_fn false (S.toPOBackdoorSystem.factualX ω) -
(S.μ_val true (S.toPOBackdoorSystem.factualX ω) -
S.μ_val false (S.toPOBackdoorSystem.factualX ω)))
exact ((((η.μ_meas true).comp
(comap_measurable S.toPOBackdoorSystem.factualX)).sub
((η.μ_meas false).comp
(comap_measurable S.toPOBackdoorSystem.factualX))).sub
(((S.μ_meas true).comp
(comap_measurable S.toPOBackdoorSystem.factualX)).sub
((S.μ_meas false).comp
(comap_measurable S.toPOBackdoorSystem.factualX)))).stronglyMeasurable
have hbase_ce :
P.μ[base | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] base :=
Filter.EventuallyEq.of_eq
(MeasureTheory.condExp_of_stronglyMeasurable
S.toPOBackdoorSystem.sigmaX_le hbase_sm hbase_int)
have hηe_lower : ∀ ω, ε ≤ η.e_fn (X ω) := fun ω => (h_overlap_η (X ω)).1
have hηe_upper : ∀ ω, η.e_fn (X ω) ≤ 1 - ε := fun ω => (h_overlap_η (X ω)).2
have h₀e_lower : ∀ ω, ε ≤ S.e_val (X ω) := by
intro ω
exact (h_overlap_η₀ (X ω)).1
have h₀e_upper : ∀ ω, S.e_val (X ω) ≤ 1 - ε := by
intro ω
exact (h_overlap_η₀ (X ω)).2
have hwηT_Linf : MemLp (fun ω => 1 / η.e_fn (X ω)) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(η.e_meas.comp S.toPOBackdoorSystem.measurable_factualX))).aestronglyMeasurable
· exact Filter.Eventually.of_forall (fun ω => by
have hpos : 0 < η.e_fn (X ω) := lt_of_lt_of_le hε_pos (hηe_lower ω)
have hle : (η.e_fn (X ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos hε_pos).2 (hηe_lower ω)
simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle)
have hwηF_Linf : MemLp (fun ω => 1 / (1 - η.e_fn (X ω))) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(measurable_const.sub
(η.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)))).aestronglyMeasurable
· exact Filter.Eventually.of_forall (fun ω => by
have hden : ε ≤ 1 - η.e_fn (X ω) := by linarith [hηe_upper ω]
have hpos : 0 < 1 - η.e_fn (X ω) := lt_of_lt_of_le hε_pos hden
have hle : (1 - η.e_fn (X ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos hε_pos).2 hden
simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle)
have hw₀T_Linf : MemLp (fun ω => 1 / S.e_val (X ω)) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX))).aestronglyMeasurable
· exact Filter.Eventually.of_forall (fun ω => by
have hpos : 0 < S.e_val (X ω) := S.e_pos _
have hle : (S.e_val (X ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos hε_pos).2 (h₀e_lower ω)
simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle)
have hw₀F_Linf : MemLp (fun ω => 1 / (1 - S.e_val (X ω))) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(measurable_const.sub
(S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)))).aestronglyMeasurable
· exact Filter.Eventually.of_forall (fun ω => by
have hpos : 0 < 1 - S.e_val (X ω) := by linarith [S.e_lt_one (X ω)]
have hden : ε ≤ 1 - S.e_val (X ω) := by linarith [h₀e_upper ω]
have hle : (1 - S.e_val (X ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos hε_pos).2 hden
simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle)
have hYind_int : ∀ d : Bool,
Integrable (fun ω => Y ω * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ :=
fun d => S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (MeasurableSet.singleton d)
hA.integrable_factualY
have hημind_int : ∀ d : Bool,
Integrable (fun ω => η.μ_fn d (X ω) *
S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := by
intro d
exact S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (MeasurableSet.singleton d)
(h_μ_η_int d)
have hμind_int : ∀ d : Bool,
Integrable (fun ω => S.μ_val d (X ω) *
S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := by
intro d
exact S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (MeasurableSet.singleton d)
(hμ_val_int d)
have hresη_int : ∀ d : Bool,
Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω *
(Y ω - η.μ_fn d (X ω))) P.μ := by
intro d
have hY' : Integrable
(fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * Y ω) P.μ := by
simpa [Y, mul_comm] using hYind_int d
have hμ' : Integrable
(fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * η.μ_fn d (X ω)) P.μ := by
simpa [mul_comm] using hημind_int d
refine (hY'.sub hμ').congr ?_
exact Filter.Eventually.of_forall (fun ω => by
change S.toPOBackdoorSystem.dVar.indicator d ω * Y ω -
S.toPOBackdoorSystem.dVar.indicator d ω * η.μ_fn d (X ω) =
S.toPOBackdoorSystem.dVar.indicator d ω * (Y ω - η.μ_fn d (X ω))
ring_nf)
have hresμ_int : ∀ d : Bool,
Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω *
(Y ω - S.μ_val d (X ω))) P.μ := by
intro d
have hY' : Integrable
(fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * Y ω) P.μ := by
simpa [Y, mul_comm] using hYind_int d
have hμ' : Integrable
(fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (X ω)) P.μ := by
simpa [mul_comm] using hμind_int d
refine (hY'.sub hμ').congr ?_
exact Filter.Eventually.of_forall (fun ω => by
change S.toPOBackdoorSystem.dVar.indicator d ω * Y ω -
S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (X ω) =
S.toPOBackdoorSystem.dVar.indicator d ω * (Y ω - S.μ_val d (X ω))
ring_nf)
have hBηT_int : Integrable BηT P.μ := by
have hL1 : MemLp BηT 1 P.μ := by
have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1)
hwηT_Linf (memLp_one_iff_integrable.2 (hresη_int true))
exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by
simp [BηT, X, Y, indT]
ring))
exact hL1.integrable (by norm_num)
have hCηF_int : Integrable CηF P.μ := by
have hL1 : MemLp CηF 1 P.μ := by
have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1)
hwηF_Linf (memLp_one_iff_integrable.2 (hresη_int false))
exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by
simp [CηF, X, Y, indF]
ring))
exact hL1.integrable (by norm_num)
have hB₀T_int : Integrable B₀T P.μ := by
have hL1 : MemLp B₀T 1 P.μ := by
have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1)
-- … truncated; follow the source link for the rest …
theorem phi_eta_minus_phi₀_at_x reviewed
⚑ flagged
Causalean.Estimation.CATE
Value-space form of the DR pseudo-outcome bias identity. Fix a candidate nuisance pair η. Under the back-door identification assumptions, if η's propensity is uniformly bounded in [ε, 1 − ε] for every covariate value, the truth nuisance likewise has propensity uniformly bounded in [ε, 1 − ε], ε is strictly positive, each candidate outcome-regression arm, composed with the covariate, is integrable, and the DR pseudo-outcome contrast φ_η − φ_0 is integrable, then for covariate-law-almost-every x, the mean of φ_η − φ_0 under the regular conditional distribution of the data triple given the covariate value x equals the closed-form cross-product remainder condBias η η₀ x.
Formal statement
hypotheses
P :
IsFiniteMeasure P.μ
Nonempty γ
S :
hA :
S.toPOBackdoorSystem.Assumptions
η :
ε :
ℝ
h_overlap_η :
η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
h_overlap_η₀ :
S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
hε_pos :
0 < ε
h_μ_η_int :
∀ a : Bool, Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ
h_int :
Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ
Proof (Lean source)
theorem phi_eta_minus_phi₀_at_x
{P : POSystem} [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ]
[StandardBorelSpace γ] [Nonempty γ]
(S : CATEEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions)
(η : NuisanceVec γ) {ε : ℝ}
(h_overlap_η : η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε)
(h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈
BackdoorEstimationSystem.H_ε (γ := γ) ε)
(hε_pos : 0 < ε)
(h_μ_η_int : ∀ a : Bool,
Integrable
(fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ)
(h_int : Integrable
(fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ) :
∀ᵐ x ∂(S.toBackdoorEstimationSystem.P_X),
(∫ z, (phi_eta z η - phi₀ S z)
∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ x)
= condBias η S.toBackdoorEstimationSystem.η₀ x := by
have hcondΩ :
P.μ[fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)
| S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
(fun ω => condBias η S.toBackdoorEstimationSystem.η₀
(S.toBackdoorEstimationSystem.factualX ω)) :=
phi_eta_minus_phi₀_cond_exp S hA η h_overlap_η h_overlap_η₀ hε_pos
h_μ_η_int
have hf_sm : StronglyMeasurable
(fun z : γ × Bool × ℝ => phi_eta z η - phi₀ S z) :=
((measurable_phi_eta η).sub (measurable_phi₀ S)).stronglyMeasurable
have hkernel :
P.μ[fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)
| comap S.toPOBackdoorSystem.factualX inferInstance]
=ᵐ[P.μ]
(fun ω =>
∫ z, (phi_eta z η - phi₀ S z)
∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ
(S.toPOBackdoorSystem.factualX ω)) :=
ProbabilityTheory.condExp_ae_eq_integral_condDistrib
S.toPOBackdoorSystem.measurable_factualX
S.toBackdoorEstimationSystem.measurable_factualZ.aemeasurable
hf_sm h_int
have hΩ :
(fun ω =>
∫ z, (phi_eta z η - phi₀ S z)
∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ
(S.toPOBackdoorSystem.factualX ω))
=ᵐ[P.μ]
(fun ω => condBias η S.toBackdoorEstimationSystem.η₀
(S.toBackdoorEstimationSystem.factualX ω)) :=
hkernel.symm.trans (by
simpa [POBackdoorSystem.sigmaX] using hcondΩ)
have hleft_meas : Measurable
(fun x : γ =>
∫ z, (phi_eta z η - phi₀ S z)
∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ x) := by
have hpair_sm : StronglyMeasurable
(fun p : γ × (γ × Bool × ℝ) => phi_eta p.2 η - phi₀ S p.2) :=
(hf_sm.comp_measurable measurable_snd)
exact (MeasureTheory.StronglyMeasurable.integral_condDistrib
(Y := S.toBackdoorEstimationSystem.factualZ)
(X := S.toPOBackdoorSystem.factualX) (μ := P.μ) hpair_sm).measurable
have hset : MeasurableSet
{x : γ |
(∫ z, (phi_eta z η - phi₀ S z)
∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ x)
= condBias η S.toBackdoorEstimationSystem.η₀ x} :=
measurableSet_eq_fun hleft_meas
(measurable_condBias η S.toBackdoorEstimationSystem.η₀)
unfold BackdoorEstimationSystem.P_X
rw [MeasureTheory.ae_map_iff
S.toPOBackdoorSystem.measurable_factualX.aemeasurable hset]
exact hΩ
4 supporting declarations (lemmas, instances)
-
measurable_condBiaslemma — condBias η η₀ is measurable in x.Proof (Lean source)
lemma measurable_condBias (η η₀ : NuisanceVec γ) : Measurable (fun x : γ => condBias η η₀ x) := by unfold condBias refine measurable_sum _ ?_ intro a _ cases a · have h_num : Measurable (fun x : γ => (η.e_fn x - η₀.e_fn x) * (η.μ_fn false x - η₀.μ_fn false x)) := (η.e_meas.sub η₀.e_meas).mul ((η.μ_meas false).sub (η₀.μ_meas false)) have h_den : Measurable (fun x : γ => 1 - η.e_fn x) := measurable_const.sub η.e_meas simpa using h_num.fun_div h_den · have h_num : Measurable (fun x : γ => (η.e_fn x - η₀.e_fn x) * (η.μ_fn true x - η₀.μ_fn true x)) := (η.e_meas.sub η₀.e_meas).mul ((η.μ_meas true).sub (η₀.μ_meas true)) simpa using h_num.fun_div η.e_meas -
condBias_zero_of_propensity_matchlemma — If the propensity matches the truth at x, then condBias η η₀ x = 0.Proof (Lean source)
lemma condBias_zero_of_propensity_match (η η₀ : NuisanceVec γ) (x : γ) (h_e : η.e_fn x = η₀.e_fn x) : condBias η η₀ x = 0 := by unfold condBias apply Finset.sum_eq_zero intro a _ rw [show η.e_fn x - η₀.e_fn x = 0 from sub_eq_zero.mpr h_e] ring -
condBias_zero_of_outcome_matchlemma — If both outcome arms match the truth at x, then condBias η η₀ x = 0.hypothesesconclusioncondBias η η₀ x = 0Proof (Lean source)
lemma condBias_zero_of_outcome_match (η η₀ : NuisanceVec γ) (x : γ) (h_μ : ∀ a : Bool, η.μ_fn a x = η₀.μ_fn a x) : condBias η η₀ x = 0 := by unfold condBias apply Finset.sum_eq_zero intro a _ rw [show η.μ_fn a x - η₀.μ_fn a x = 0 from sub_eq_zero.mpr (h_μ a)] ring -
cond_exp_phi_eta_dir_deriv_at_truth_zerotheorem — The σ(X)-conditional expectation of the directional derivative phi_eta_dir_deriv at the truth g₀ = η₀ is zero a.e.hypothesesP :IsFiniteMeasure P.μS :hA :S.toPOBackdoorSystem.Assumptionsε :ℝhε_pos :0 < εh_overlap_η₀ :S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) εv :h_v_μ_bdd :∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |v.μ_fn b x| ≤ Cμh_v_e_bdd :∃ Ce : ℝ, ∀ x : γ, |v.e_fn x| ≤ CeconclusionP.μ[fun ω => phi_eta_dir_deriv S.toBackdoorEstimationSystem.η₀ v (S.toBackdoorEstimationSystem.factualZ ω) | S.toPOBackdoorSystem.sigmaX]=ᵐ[P.μ] (fun _ => (0 : ℝ))Proof (Lean source)
theorem cond_exp_phi_eta_dir_deriv_at_truth_zero {P : POSystem} [StandardBorelSpace P.Ω] [IsFiniteMeasure P.μ] (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) {ε : ℝ} (hε_pos : 0 < ε) (h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (v : NuisanceVec γ) (h_v_μ_bdd : ∃ Cμ : ℝ, ∀ b : Bool, ∀ x : γ, |v.μ_fn b x| ≤ Cμ) (h_v_e_bdd : ∃ Ce : ℝ, ∀ x : γ, |v.e_fn x| ≤ Ce) : P.μ[fun ω => phi_eta_dir_deriv S.toBackdoorEstimationSystem.η₀ v (S.toBackdoorEstimationSystem.factualZ ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by let X : P.Ω → γ := S.toPOBackdoorSystem.factualX let Y : P.Ω → ℝ := S.toPOBackdoorSystem.factualY let indT : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator true let indF : P.Ω → ℝ := S.toPOBackdoorSystem.dVar.indicator false let T1 : P.Ω → ℝ := fun ω => v.μ_fn true (X ω) - v.μ_fn false (X ω) let T2 : P.Ω → ℝ := fun ω => (-v.e_fn (X ω) * (1 / S.e_val (X ω)) * (1 / S.e_val (X ω))) * (indT ω * (Y ω - S.μ_val true (X ω))) let T3 : P.Ω → ℝ := fun ω => (-1 / S.e_val (X ω) * v.μ_fn true (X ω)) * indT ω let T4 : P.Ω → ℝ := fun ω => (-v.e_fn (X ω) * (1 / (1 - S.e_val (X ω))) * (1 / (1 - S.e_val (X ω)))) * (indF ω * (Y ω - S.μ_val false (X ω))) let T5 : P.Ω → ℝ := fun ω => (1 / (1 - S.e_val (X ω)) * v.μ_fn false (X ω)) * indF ω have hindA_true : ∀ ω, BackdoorEstimationSystem.indA (S.toBackdoorEstimationSystem.factualZ ω) = indT ω := by intro ω by_cases hD : S.toPOBackdoorSystem.factualD ω = true · have hInd : indT ω = 1 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA, BackdoorEstimationSystem.projA, indT, hD, hInd] · have hInd : indT ω = 0 := S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA, BackdoorEstimationSystem.projA, indT, hD, hInd] have hφ_eq : (fun ω => phi_eta_dir_deriv S.toBackdoorEstimationSystem.η₀ v (S.toBackdoorEstimationSystem.factualZ ω)) = (fun ω => T1 ω + T2 ω + T3 ω + T4 ω + T5 ω) := by funext ω have hind_true_z : BackdoorEstimationSystem.indA (S.toPOBackdoorSystem.factualX ω, S.toPOBackdoorSystem.factualD ω, S.toPOBackdoorSystem.factualY ω) = indT ω := by simpa [BackdoorEstimationSystem.factualZ] using hindA_true ω have hind_not : 1 - indT ω = indF ω := by have hsum : indT ω + indF ω = 1 := S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω linarith simp only [T1, T2, T3, T4, T5, X, Y, indT, indF, phi_eta_dir_deriv, BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.projX, BackdoorEstimationSystem.projY, BackdoorEstimationSystem.η₀, hind_true_z, hind_not] have hneT : S.e_val (S.toPOBackdoorSystem.factualX ω) ≠ 0 := by exact ne_of_gt (lt_of_lt_of_le hε_pos (h_overlap_η₀ (S.toPOBackdoorSystem.factualX ω)).1) have hden : ε ≤ 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := by have hu : S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by simpa [BackdoorEstimationSystem.η₀] using (h_overlap_η₀ (S.toPOBackdoorSystem.factualX ω)).2 linarith have hneF : 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) ≠ 0 := by exact ne_of_gt (lt_of_lt_of_le hε_pos hden) field_simp [hneT, hneF] ring have hμ_val_int : ∀ d : Bool, Integrable (fun ω => S.μ_val d (X ω)) P.μ := by intro d have hcate_int : Integrable (S.toPOBackdoorSystem.CATE d) P.μ := by unfold POBackdoorSystem.CATE exact MeasureTheory.integrable_condExp exact hcate_int.congr (S.μ_compat hA d) rcases h_v_μ_bdd with ⟨Cμ, hCμ⟩ rcases h_v_e_bdd with ⟨Ce, hCe⟩ have hvμ_int : ∀ d : Bool, Integrable (fun ω => v.μ_fn d (X ω)) P.μ := by intro d refine MeasureTheory.Integrable.of_bound (((v.μ_meas d).comp S.toPOBackdoorSystem.measurable_factualX).aestronglyMeasurable) |Cμ| (Filter.Eventually.of_forall ?_) intro ω simpa [X, Real.norm_eq_abs] using le_trans (hCμ d (X ω)) (le_abs_self Cμ) have hv_e_top : MemLp (fun ω => v.e_fn (X ω)) ⊤ P.μ := by refine MemLp.of_bound ?_ |Ce| (Filter.Eventually.of_forall ?_) · exact ((v.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)).aestronglyMeasurable · intro ω simpa [X, Real.norm_eq_abs] using le_trans (hCe (X ω)) (le_abs_self Ce) have hvμ_top : ∀ d : Bool, MemLp (fun ω => v.μ_fn d (X ω)) ⊤ P.μ := by intro d refine MemLp.of_bound ?_ |Cμ| (Filter.Eventually.of_forall ?_) · exact (((v.μ_meas d).comp S.toPOBackdoorSystem.measurable_factualX)).aestronglyMeasurable · intro ω simpa [X, Real.norm_eq_abs] using le_trans (hCμ d (X ω)) (le_abs_self Cμ) have hT1_int : Integrable T1 P.μ := by simp only [T1] exact (hvμ_int true).sub (hvμ_int false) have hT1_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] T1 := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => v.μ_fn true (S.toPOBackdoorSystem.factualX ω) - v.μ_fn false (S.toPOBackdoorSystem.factualX ω)) exact (((v.μ_meas true).comp (comap_measurable S.toPOBackdoorSystem.factualX)).sub ((v.μ_meas false).comp (comap_measurable S.toPOBackdoorSystem.factualX))).stronglyMeasurable have hT1_ce : P.μ[T1 | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] T1 := Filter.EventuallyEq.of_eq (MeasureTheory.condExp_of_stronglyMeasurable S.toPOBackdoorSystem.sigmaX_le hT1_sm hT1_int) have h₀e_lower : ∀ ω, ε ≤ S.e_val (X ω) := by intro ω exact (h_overlap_η₀ (X ω)).1 have h₀e_upper : ∀ ω, S.e_val (X ω) ≤ 1 - ε := by intro ω exact (h_overlap_η₀ (X ω)).2 have hw₀T_Linf : MemLp (fun ω => 1 / S.e_val (X ω)) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ ?_ · exact ((measurable_const.div (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX))).aestronglyMeasurable · exact Filter.Eventually.of_forall (fun ω => by have hpos : 0 < S.e_val (X ω) := lt_of_lt_of_le hε_pos (h₀e_lower ω) have hle : (S.e_val (X ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos hε_pos).2 (h₀e_lower ω) simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle) have hw₀F_Linf : MemLp (fun ω => 1 / (1 - S.e_val (X ω))) ⊤ P.μ := by refine MemLp.of_bound ?_ ε⁻¹ ?_ · exact ((measurable_const.div (measurable_const.sub (S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)))).aestronglyMeasurable · exact Filter.Eventually.of_forall (fun ω => by have hden : ε ≤ 1 - S.e_val (X ω) := by linarith [h₀e_upper ω] have hpos : 0 < 1 - S.e_val (X ω) := lt_of_lt_of_le hε_pos hden have hle : (1 - S.e_val (X ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos hε_pos).2 hden simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle) have hYind_int : ∀ d : Bool, Integrable (fun ω => Y ω * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := fun d => S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (MeasurableSet.singleton d) hA.integrable_factualY have hμind_int : ∀ d : Bool, Integrable (fun ω => S.μ_val d (X ω) * S.toPOBackdoorSystem.dVar.indicator d ω) P.μ := by intro d exact S.toPOBackdoorSystem.dVar.integrable_mul_indicator d (MeasurableSet.singleton d) (hμ_val_int d) have hresμ_int : ∀ d : Bool, Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * (Y ω - S.μ_val d (X ω))) P.μ := by intro d have hY' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * Y ω) P.μ := by simpa [Y, mul_comm] using hYind_int d have hμ' : Integrable (fun ω => S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (X ω)) P.μ := by simpa [mul_comm] using hμind_int d refine (hY'.sub hμ').congr ?_ exact Filter.Eventually.of_forall (fun ω => by change S.toPOBackdoorSystem.dVar.indicator d ω * Y ω - S.toPOBackdoorSystem.dVar.indicator d ω * S.μ_val d (X ω) = S.toPOBackdoorSystem.dVar.indicator d ω * (Y ω - S.μ_val d (X ω)) ring_nf) have hgET_top : MemLp (fun ω => -v.e_fn (X ω) * (1 / S.e_val (X ω)) * (1 / S.e_val (X ω))) ⊤ P.μ := by have htmp : MemLp (fun ω => -v.e_fn (X ω) * (1 / S.e_val (X ω))) ⊤ P.μ := by simpa [mul_comm, mul_left_comm, mul_assoc] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀T_Linf hv_e_top.neg simpa [mul_comm, mul_left_comm, mul_assoc] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀T_Linf htmp have hgEF_top : MemLp (fun ω => -v.e_fn (X ω) * (1 / (1 - S.e_val (X ω))) * (1 / (1 - S.e_val (X ω)))) ⊤ P.μ := by have htmp : MemLp (fun ω => -v.e_fn (X ω) * (1 / (1 - S.e_val (X ω)))) ⊤ P.μ := by simpa [mul_comm, mul_left_comm, mul_assoc] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀F_Linf hv_e_top.neg simpa [mul_comm, mul_left_comm, mul_assoc] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀F_Linf htmp have hgMT_top : MemLp (fun ω => -1 / S.e_val (X ω) * v.μ_fn true (X ω)) ⊤ P.μ := by simpa [div_eq_mul_inv, one_div, mul_assoc, mul_left_comm, mul_comm] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀T_Linf.neg (hvμ_top true) have hgMF_top : MemLp (fun ω => 1 / (1 - S.e_val (X ω)) * v.μ_fn false (X ω)) ⊤ P.μ := by simpa [div_eq_mul_inv, one_div, mul_assoc, mul_left_comm, mul_comm] using MemLp.mul' (p := ⊤) (q := ⊤) (r := ⊤) hw₀F_Linf (hvμ_top false) have hT2_int : Integrable T2 P.μ := by have hL1 : MemLp T2 1 P.μ := by have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1) hgET_top (memLp_one_iff_integrable.2 (hresμ_int true)) exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by simp [T2, X, Y, indT] ring)) exact hL1.integrable (by norm_num) have hT4_int : Integrable T4 P.μ := by have hL1 : MemLp T4 1 P.μ := by have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1) hgEF_top (memLp_one_iff_integrable.2 (hresμ_int false)) exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by simp [T4, X, Y, indF] ring)) exact hL1.integrable (by norm_num) have hT3_int : Integrable T3 P.μ := by have hL1 : MemLp T3 1 P.μ := by have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1) hgMT_top (memLp_one_iff_integrable.2 (S.toPOBackdoorSystem.dVar.integrable_indicator true (MeasurableSet.singleton true))) exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by simp [T3, X, indT] ring)) -- … truncated; follow the source link for the rest …
PseudoOutcomeMean 2 core · 0 supporting This file proves the conditional-mean identity for the doubly robust pseudo-outcome used to estimate conditional average treatment effects. ★ phi₀_factualZ_cond_exp★ phi_eta_cond_exp_eq_tau
Mean of the CATE Pseudo-Outcome
This file proves the conditional-mean identity for the doubly robust
pseudo-outcome used to estimate conditional average treatment effects. The
identity shows that, under the back-door assumptions and strict overlap, the
conditional expectation of the true pseudo-outcome given covariates equals the
target conditional treatment effect. The theorem phi₀_factualZ_cond_exp
proves the σ(X)-conditional statement on the source probability space, while
phi_eta_cond_exp_eq_tau transports it to the value-space law P_X using
conditional distributions.
theorem phi₀_factualZ_cond_exp reviewed
⚑ flagged
Causalean.Estimation.CATE.CATEEstimationSystem
σ(X)-conditional mean of the true DR pseudo-outcome equals the CATE. Under the back-door identification assumptions and two-sided strict overlap: the treatment propensity lies in [ε, 1 − ε] for some ε ∈ (0, 1/2] almost surely, the σ(X)-conditional expectation of the true DR pseudo-outcome φ₀, evaluated at the factual data triple, equals the value-space CATE τ_val pulled back along the covariate, almost surely.
Formal statement
hypotheses
S :
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
h_overlap :
S.toBackdoorEstimationSystem.StrictOverlap ε
conclusion
P.μ[fun ω => phi₀ S (S.toBackdoorEstimationSystem.factualZ ω) | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ] (fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω))
Proof (Lean source)
theorem phi₀_factualZ_cond_exp
(S : CATEEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions)
{ε : ℝ}
(h_overlap : S.toBackdoorEstimationSystem.StrictOverlap ε) :
P.μ[fun ω => phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)
| S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
(fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω)) := by
let base : P.Ω → ℝ := fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω)
let B : P.Ω → ℝ := fun ω =>
(1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) *
(S.toPOBackdoorSystem.dVar.indicator true ω *
(S.toPOBackdoorSystem.factualY ω -
S.μ_val true (S.toPOBackdoorSystem.factualX ω)))
let C : P.Ω → ℝ := fun ω =>
(1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) *
(S.toPOBackdoorSystem.dVar.indicator false ω *
(S.toPOBackdoorSystem.factualY ω -
S.μ_val false (S.toPOBackdoorSystem.factualX ω)))
have hindA_true : ∀ ω, BackdoorEstimationSystem.indA
(S.toBackdoorEstimationSystem.factualZ ω) =
S.toPOBackdoorSystem.dVar.indicator true ω := by
intro ω
by_cases hD : S.toPOBackdoorSystem.factualD ω = true
· have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 1 :=
S.toPOBackdoorSystem.dVar.indicator_apply_eq_one hD
simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA,
BackdoorEstimationSystem.projA, hD, hInd]
· have hInd : S.toPOBackdoorSystem.dVar.indicator true ω = 0 :=
S.toPOBackdoorSystem.dVar.indicator_apply_eq_zero (x := true) hD
simp [BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.indA,
BackdoorEstimationSystem.projA, hD, hInd]
have hindA_false : ∀ ω, 1 - BackdoorEstimationSystem.indA
(S.toBackdoorEstimationSystem.factualZ ω) =
S.toPOBackdoorSystem.dVar.indicator false ω := by
intro ω
have hsum : S.toPOBackdoorSystem.dVar.indicator true ω +
S.toPOBackdoorSystem.dVar.indicator false ω = 1 :=
S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω
rw [hindA_true ω]
linarith
have hφ_eq :
(fun ω => phi₀ S (S.toBackdoorEstimationSystem.factualZ ω))
= (fun ω => base ω + B ω - C ω) := by
funext ω
have hind_true_z :
BackdoorEstimationSystem.indA
(S.toPOBackdoorSystem.factualX ω,
S.toPOBackdoorSystem.factualD ω,
S.toPOBackdoorSystem.factualY ω)
= S.toPOBackdoorSystem.dVar.indicator true ω := by
simpa [BackdoorEstimationSystem.factualZ] using hindA_true ω
have hind_not :
1 - S.toPOBackdoorSystem.dVar.indicator true ω =
S.toPOBackdoorSystem.dVar.indicator false ω := by
have hsum : S.toPOBackdoorSystem.dVar.indicator true ω +
S.toPOBackdoorSystem.dVar.indicator false ω = 1 :=
S.toPOBackdoorSystem.dVar.indicator_add_indicator_not ω
linarith
simp [base, B, C, phi₀, phi_eta, BackdoorEstimationSystem.aipwMoment,
BackdoorEstimationSystem.factualZ, BackdoorEstimationSystem.projX,
BackdoorEstimationSystem.projY,
BackdoorEstimationSystem.η₀, CATEEstimationSystem.τ_val, hind_true_z,
hind_not, mul_assoc, mul_comm, sub_eq_add_neg, add_assoc, add_comm]
ring_nf
have hμx_int : ∀ d : Bool,
Integrable (fun ω => S.μ_val d (S.toPOBackdoorSystem.factualX ω)) P.μ := by
intro d
have hcate_int : Integrable (S.toPOBackdoorSystem.CATE d) P.μ := by
unfold POBackdoorSystem.CATE
exact MeasureTheory.integrable_condExp
exact hcate_int.congr (S.μ_compat hA d)
have hbase_int : Integrable base P.μ := by
have hsub := (hμx_int true).sub (hμx_int false)
refine hsub.congr ?_
refine Filter.Eventually.of_forall (fun ω => ?_)
simp [base, CATEEstimationSystem.τ_val]
have hbase_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] base := by
change StronglyMeasurable[
comap S.toPOBackdoorSystem.factualX inferInstance]
(fun ω => S.τ_val (S.toPOBackdoorSystem.factualX ω))
exact ((S.measurable_τ_val).comp
(comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable
have hbase_ce :
P.μ[base | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] base :=
Filter.EventuallyEq.of_eq
(MeasureTheory.condExp_of_stronglyMeasurable
S.toPOBackdoorSystem.sigmaX_le hbase_sm hbase_int)
have he_lower :
∀ᵐ ω ∂P.μ, ε ≤ S.e_val (S.toPOBackdoorSystem.factualX ω) := by
filter_upwards [h_overlap.2.2, S.e_compat] with ω hprop hcomp
simpa [hcomp] using hprop.1
have he_upper :
∀ᵐ ω ∂P.μ, S.e_val (S.toPOBackdoorSystem.factualX ω) ≤ 1 - ε := by
filter_upwards [h_overlap.2.2, S.e_compat] with ω hprop hcomp
simpa [hcomp] using hprop.2
have hw_true_Linf : MemLp
(fun ω => 1 / S.e_val (S.toPOBackdoorSystem.factualX ω)) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX))).aestronglyMeasurable
· filter_upwards [he_lower] with ω he
have hpos : 0 < S.e_val (S.toPOBackdoorSystem.factualX ω) :=
S.e_pos _
have hle : (S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos h_overlap.1).2 he
simpa [one_div, Real.norm_eq_abs, abs_of_pos hpos] using hle
have hw_false_Linf : MemLp
(fun ω => 1 / (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ ?_
· exact ((measurable_const.div
(measurable_const.sub
(S.e_meas.comp S.toPOBackdoorSystem.measurable_factualX)))).aestronglyMeasurable
· filter_upwards [he_upper] with ω he
have hden : ε ≤ 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) := by
linarith
have hdenpos : 0 < 1 - S.e_val (S.toPOBackdoorSystem.factualX ω) :=
lt_of_lt_of_le h_overlap.1 hden
have hle : (1 - S.e_val (S.toPOBackdoorSystem.factualX ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hdenpos h_overlap.1).2 hden
simpa [one_div, Real.norm_eq_abs, abs_of_pos hdenpos] using hle
have hresid_true_int :=
residual_integrable S.toBackdoorEstimationSystem hA true
have hresid_false_int :=
residual_integrable S.toBackdoorEstimationSystem hA false
have hB_int : Integrable B P.μ := by
have hresid_L1 : MemLp
(fun ω => S.toPOBackdoorSystem.dVar.indicator true ω *
(S.toPOBackdoorSystem.factualY ω -
S.μ_val true (S.toPOBackdoorSystem.factualX ω))) 1 P.μ :=
memLp_one_iff_integrable.2 hresid_true_int
have hL1 : MemLp B 1 P.μ := by
have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1)
hw_true_Linf hresid_L1
exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by
simp [B]
ring))
exact hL1.integrable (by norm_num)
have hC_int : Integrable C P.μ := by
have hresid_L1 : MemLp
(fun ω => S.toPOBackdoorSystem.dVar.indicator false ω *
(S.toPOBackdoorSystem.factualY ω -
S.μ_val false (S.toPOBackdoorSystem.factualX ω))) 1 P.μ :=
memLp_one_iff_integrable.2 hresid_false_int
have hL1 : MemLp C 1 P.μ := by
have hmul := MemLp.mul' (p := 1) (q := ⊤) (r := 1)
hw_false_Linf hresid_L1
exact hmul.ae_eq (Filter.Eventually.of_forall (fun ω => by
simp [C]
ring))
exact hL1.integrable (by norm_num)
have hB_zero :
P.μ[B | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
have hg_meas : Measurable (fun x => 1 / S.e_val x) :=
measurable_const.div S.e_meas
exact weighted_residual_cond_exp_zero S.toBackdoorEstimationSystem hA true
(fun x => 1 / S.e_val x) hg_meas hB_int
have hC_zero :
P.μ[C | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
have hg_meas : Measurable (fun x => 1 / (1 - S.e_val x)) :=
measurable_const.div (measurable_const.sub S.e_meas)
exact weighted_residual_cond_exp_zero S.toBackdoorEstimationSystem hA false
(fun x => 1 / (1 - S.e_val x)) hg_meas hC_int
have hsum_int : Integrable (fun ω => base ω + B ω) P.μ :=
hbase_int.add hB_int
have hadd :
P.μ[fun ω => base ω + B ω | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
P.μ[base | S.toPOBackdoorSystem.sigmaX]
+ P.μ[B | S.toPOBackdoorSystem.sigmaX] :=
MeasureTheory.condExp_add hbase_int hB_int S.toPOBackdoorSystem.sigmaX
have hsub :
P.μ[fun ω => base ω + B ω - C ω | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ]
P.μ[fun ω => base ω + B ω | S.toPOBackdoorSystem.sigmaX]
- P.μ[C | S.toPOBackdoorSystem.sigmaX] :=
MeasureTheory.condExp_sub hsum_int hC_int S.toPOBackdoorSystem.sigmaX
rw [hφ_eq]
refine hsub.trans ?_
filter_upwards [hadd, hbase_ce, hB_zero, hC_zero] with ω haddω hbaseω hBω hCω
change P.μ[fun ω => base ω + B ω | S.toPOBackdoorSystem.sigmaX] ω -
P.μ[C | S.toPOBackdoorSystem.sigmaX] ω =
S.τ_val (S.toPOBackdoorSystem.factualX ω)
rw [haddω, Pi.add_apply, hbaseω, hBω, hCω]
simp [base]
theorem phi_eta_cond_exp_eq_tau reviewed
⚑ flagged
Causalean.Estimation.CATE.CATEEstimationSystem
Value-space form of the DR pseudo-outcome mean-CATE identity. Under the back-door identification assumptions, two-sided strict overlap: the treatment propensity lies in [ε, 1 − ε] for some ε ∈ (0, 1/2] almost surely, and integrability of the true DR pseudo-outcome φ₀ evaluated at the factual data triple, for covariate-law-almost-every x, the mean of φ₀ under the regular conditional distribution of the data triple given the covariate value x equals the value-space CATE τ_val x.
Formal statement
hypotheses
Nonempty γ
S :
hA :
S.toPOBackdoorSystem.Assumptions
ε :
ℝ
h_overlap :
S.toBackdoorEstimationSystem.StrictOverlap ε
h_int :
Integrable (fun ω => phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ
conclusion
∀ᵐ x ∂(S.toBackdoorEstimationSystem.P_X),
(∫ z, phi₀ S z ∂condDistrib S.toBackdoorEstimationSystem.factualZ S.toPOBackdoorSystem.factualX P.μ x)
= S.τ_val x
Proof (Lean source)
theorem phi_eta_cond_exp_eq_tau [StandardBorelSpace γ] [Nonempty γ]
(S : CATEEstimationSystem P γ)
(hA : S.toPOBackdoorSystem.Assumptions)
{ε : ℝ}
(h_overlap : S.toBackdoorEstimationSystem.StrictOverlap ε)
(h_int : Integrable
(fun ω => phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ) :
∀ᵐ x ∂(S.toBackdoorEstimationSystem.P_X),
(∫ z, phi₀ S z ∂condDistrib S.toBackdoorEstimationSystem.factualZ
S.toPOBackdoorSystem.factualX P.μ x)
= S.τ_val x := by
let X := S.toPOBackdoorSystem.factualX
let Z := S.toBackdoorEstimationSystem.factualZ
let lhs : γ → ℝ := fun x =>
∫ z, phi₀ S z ∂condDistrib Z X P.μ x
have hcond :
P.μ[fun ω => phi₀ S (Z ω) | S.toPOBackdoorSystem.sigmaX]
=ᵐ[P.μ] fun ω => lhs (X ω) := by
simpa [lhs, X, Z, POBackdoorSystem.sigmaX] using
(ProbabilityTheory.condExp_ae_eq_integral_condDistrib
(μ := P.μ) (X := X) (Y := Z)
S.toPOBackdoorSystem.measurable_factualX
S.toBackdoorEstimationSystem.measurable_factualZ.aemeasurable
(measurable_phi₀ S).stronglyMeasurable h_int)
have hΩ : ∀ᵐ ω ∂P.μ, lhs (X ω) = S.τ_val (X ω) :=
hcond.symm.trans (phi₀_factualZ_cond_exp S hA h_overlap)
have hlhs_meas : Measurable lhs := by
have hφ : StronglyMeasurable
(fun p : γ × (γ × Bool × ℝ) => phi₀ S p.2) :=
(measurable_phi₀ S).stronglyMeasurable.comp_measurable measurable_snd
have hsm : StronglyMeasurable
(fun x => ∫ z, phi₀ S z ∂condDistrib Z X P.μ x) := by
simpa using
(MeasureTheory.StronglyMeasurable.integral_condDistrib
(X := X) (Y := Z) (μ := P.μ) hφ)
simpa [lhs] using hsm.measurable
have hset : MeasurableSet {x : γ | lhs x = S.τ_val x} :=
measurableSet_eq_fun hlhs_meas S.measurable_τ_val
unfold BackdoorEstimationSystem.P_X
change ∀ᵐ x ∂P.μ.map X, lhs x = S.τ_val x
rw [MeasureTheory.ae_map_iff
S.toPOBackdoorSystem.measurable_factualX.aemeasurable hset]
simpa [X] using hΩ
SecondOrderBias 1 core · 1 supporting This file proves that the weighted population bias of the doubly robust CATE pseudo-outcome is governed by a second-order product of nuisance errors. ★ abs_integral_phiDiff_mul_le_product
Second-Order CATE Bias
This file proves that the weighted population bias of the doubly robust CATE
pseudo-outcome is governed by a second-order product of nuisance errors. It
first converts the weighted pseudo-outcome bias into a conditional-bias
integral over covariates with integral_phiDiff_mul_eq_condBias and then
bounds that integral in abs_integral_phiDiff_mul_le_product by a product of
outcome-regression and propensity-score error norms.
theorem abs_integral_phiDiff_mul_le_product reviewed
⚑ flagged
Causalean.Estimation.CATE
Second-order product bias bound for the DR-Learner. Fix a candidate nuisance pair η and a test function w. Under ε strictly positive, the back-door identification assumptions, if η's propensity is uniformly bounded in [ε, 1 − ε] for every covariate value, the truth nuisance likewise has propensity uniformly bounded in [ε, 1 − ε], each candidate outcome-regression arm, composed with the covariate, is integrable, w is measurable, w is dominated by a nonnegative bound B, the w-weighted pseudo-outcome bias is integrable, each candidate outcome-regression error is square-integrable against the covariate law, and the propensity error is square-integrable against the covariate law, then the absolute value of the population integral of the w-weighted pseudo-outcome bias (phi_eta η − φ₀) · w is bounded by B/ε times the sum, over the two treatment arms, of ‖η.μ_fn a − μ_val a‖_{L²(P_X)} · ‖η.e_fn − e_val‖_{L²(P_X)}.
Formal statement
hypotheses
S :
ε :
ℝ
hε_pos :
0 < ε
hA :
S.toPOBackdoorSystem.Assumptions
η :
h_overlap_η :
η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
h_overlap_η₀ :
S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε
h_μ_η_int :
∀ a : Bool, Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ
w :
γ → ℝ
hw_meas :
B :
ℝ
hB_nonneg :
0 ≤ B
hw_bound :
∀ x, |w x| ≤ B
h_phi_int :
Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ
h_phiw_int :
Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) * w (S.toBackdoorEstimationSystem.factualX ω)) P.μ
hΔμ_memLp :
∀ a, MemLp (fun x => η.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X
hΔe_memLp :
MemLp (fun x => η.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X
Proof (Lean source)
theorem abs_integral_phiDiff_mul_le_product
(S : CATEEstimationSystem P γ) {ε : ℝ} (hε_pos : 0 < ε)
(hA : S.toPOBackdoorSystem.Assumptions)
(η : NuisanceVec γ)
(h_overlap_η : η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε)
(h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈
BackdoorEstimationSystem.H_ε (γ := γ) ε)
(h_μ_η_int : ∀ a : Bool,
Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ)
(w : γ → ℝ) (hw_meas : Measurable w)
{B : ℝ} (hB_nonneg : 0 ≤ B) (hw_bound : ∀ x, |w x| ≤ B)
(h_phi_int :
Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ)
(h_phiw_int :
Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η -
phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) *
w (S.toBackdoorEstimationSystem.factualX ω)) P.μ)
(hΔμ_memLp : ∀ a, MemLp
(fun x => η.μ_fn a x - S.μ_val a x) 2 S.toBackdoorEstimationSystem.P_X)
(hΔe_memLp : MemLp
(fun x => η.e_fn x - S.e_val x) 2 S.toBackdoorEstimationSystem.P_X) :
|∫ z, (phi_eta z η - phi₀ S z) * w z.1
∂S.toBackdoorEstimationSystem.P_Z|
≤ (B / ε) *
∑ a : Bool,
(eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2
S.toBackdoorEstimationSystem.P_X).toReal *
(eLpNorm (fun x => η.e_fn x - S.e_val x) 2
S.toBackdoorEstimationSystem.P_X).toReal := by
set PX := S.toBackdoorEstimationSystem.P_X with hPX
set η₀ := S.toBackdoorEstimationSystem.η₀ with hη₀
haveI : IsFiniteMeasure PX := by rw [hPX]; unfold BackdoorEstimationSystem.P_X; infer_instance
haveI : ENNReal.HolderTriple (2 : ENNReal) (2 : ENNReal) (1 : ENNReal) := by
constructor; simpa using ENNReal.inv_two_add_inv_two
have hBε_nonneg : 0 ≤ B / ε := div_nonneg hB_nonneg hε_pos.le
have hη_lower : ∀ x, ε ≤ η.e_fn x := fun x => (h_overlap_η x).1
have hη_upper : ∀ x, η.e_fn x ≤ 1 - ε := fun x => (h_overlap_η x).2
have hη_pos : ∀ x, 0 < η.e_fn x := fun x => lt_of_lt_of_le hε_pos (hη_lower x)
have hη_false_pos : ∀ x, 0 < 1 - η.e_fn x := by
intro x; have hx : ε ≤ 1 - η.e_fn x := by linarith [hη_upper x]
exact lt_of_lt_of_le hε_pos hx
-- The bound integrand (explicit, so it matches the eLpNorm summands).
set bnd : γ → ℝ := fun x =>
(B / ε) * |(η.μ_fn true x - S.μ_val true x) * (η.e_fn x - S.e_val x)| +
(B / ε) * |(η.μ_fn false x - S.μ_val false x) * (η.e_fn x - S.e_val x)| with hbnd
-- Pointwise bound `|condBias η η₀ x * w x| ≤ bnd x`.
have hpoint : ∀ x, |condBias η η₀ x * w x| ≤ bnd x := by
intro x
-- Reusable single-arm bound: `|a/c * w x| ≤ (B/ε)·|a|` for `0 < ε ≤ c`.
have key : ∀ a c : ℝ, 0 < c → ε ≤ c → |a / c * w x| ≤ (B / ε) * |a| := by
intro a c hc hεc
have hwc : |w x| / c ≤ B / ε := by
rw [div_eq_mul_inv, div_eq_mul_inv]
exact mul_le_mul (hw_bound x) ((inv_le_inv₀ hc hε_pos).2 hεc)
(inv_nonneg.mpr hc.le) hB_nonneg
calc |a / c * w x| = |a| * (|w x| / c) := by
rw [abs_mul, abs_div, abs_of_pos hc]; ring
_ ≤ |a| * (B / ε) := mul_le_mul_of_nonneg_left hwc (abs_nonneg _)
_ = (B / ε) * |a| := by ring
-- condBias expands to two arms `(Δμ_a · Δe) / denom_a`.
have hexp : condBias η η₀ x =
(η.μ_fn true x - S.μ_val true x) * (η.e_fn x - S.e_val x) / η.e_fn x +
(η.μ_fn false x - S.μ_val false x) * (η.e_fn x - S.e_val x) /
(1 - η.e_fn x) := by
rw [hη₀]
unfold condBias
rw [Fintype.sum_bool, if_pos (rfl : (true : Bool) = true),
if_neg (by decide : ¬((false : Bool) = true))]
simp only [BackdoorEstimationSystem.η₀]
ring
rw [hexp, add_mul]
refine (abs_add_le _ _).trans ?_
simp only [hbnd]
exact add_le_add
(key _ _ (hη_pos x) (hη_lower x))
(key _ _ (hη_false_pos x) (by linarith [hη_upper x]))
-- Integrability of the product terms and of `bnd`.
have hprod_int : ∀ a, Integrable
(fun x => (η.μ_fn a x - S.μ_val a x) * (η.e_fn x - S.e_val x)) PX := by
intro a
have hmul : MemLp
(fun x => (η.μ_fn a x - S.μ_val a x) * (η.e_fn x - S.e_val x)) 1 PX := by
exact hΔe_memLp.mul' (hΔμ_memLp a)
exact hmul.integrable le_rfl
have hbnd_int : Integrable bnd PX := by
simp only [hbnd]
exact ((hprod_int true).abs.const_mul (B / ε)).add
((hprod_int false).abs.const_mul (B / ε))
have hcw_meas : Measurable (fun x => condBias η η₀ x * w x) :=
(measurable_condBias η η₀).mul hw_meas
have hcw_int : Integrable (fun x => condBias η η₀ x * w x) PX :=
hbnd_int.mono' hcw_meas.aestronglyMeasurable
(Filter.Eventually.of_forall fun x => by
simpa [Real.norm_eq_abs] using hpoint x)
-- Cauchy–Schwarz on each product term.
have hCS : ∀ a, ∫ x, |(η.μ_fn a x - S.μ_val a x) * (η.e_fn x - S.e_val x)| ∂PX
≤ (eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2 PX).toReal *
(eLpNorm (fun x => η.e_fn x - S.e_val x) 2 PX).toReal := by
intro a
exact integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := PX) (hΔμ_memLp a) hΔe_memLp
-- Assemble.
rw [integral_phiDiff_mul_eq_condBias S hA η hε_pos h_overlap_η h_overlap_η₀
h_μ_η_int w hw_meas h_phi_int h_phiw_int]
calc
|∫ x, condBias η η₀ x * w x ∂PX|
≤ ∫ x, |condBias η η₀ x * w x| ∂PX :=
MeasureTheory.abs_integral_le_integral_abs
_ ≤ ∫ x, bnd x ∂PX :=
integral_mono_ae hcw_int.abs hbnd_int (Filter.Eventually.of_forall hpoint)
_ = (B / ε) * (∫ x, |(η.μ_fn true x - S.μ_val true x) *
(η.e_fn x - S.e_val x)| ∂PX) +
(B / ε) * (∫ x, |(η.μ_fn false x - S.μ_val false x) *
(η.e_fn x - S.e_val x)| ∂PX) := by
simp only [hbnd]
rw [integral_add ((hprod_int true).abs.const_mul (B / ε))
((hprod_int false).abs.const_mul (B / ε)),
integral_const_mul, integral_const_mul]
_ ≤ (B / ε) * ((eLpNorm (fun x => η.μ_fn true x - S.μ_val true x) 2 PX).toReal *
(eLpNorm (fun x => η.e_fn x - S.e_val x) 2 PX).toReal) +
(B / ε) * ((eLpNorm (fun x => η.μ_fn false x - S.μ_val false x) 2 PX).toReal *
(eLpNorm (fun x => η.e_fn x - S.e_val x) 2 PX).toReal) :=
add_le_add (mul_le_mul_of_nonneg_left (hCS true) hBε_nonneg)
(mul_le_mul_of_nonneg_left (hCS false) hBε_nonneg)
_ = (B / ε) *
∑ a : Bool,
(eLpNorm (fun x => η.μ_fn a x - S.μ_val a x) 2 PX).toReal *
(eLpNorm (fun x => η.e_fn x - S.e_val x) 2 PX).toReal := by
rw [Fintype.sum_bool]; ring
1 supporting declaration (lemmas, instances)
-
integral_phiDiff_mul_eq_condBiastheorem — Conditioning identity for the weighted pseudo-outcome bias.hypothesesS :hA :S.toPOBackdoorSystem.Assumptionsη :ε :ℝhε_pos :0 < εh_overlap_η :η ∈ BackdoorEstimationSystem.H_ε (γ := γ) εh_overlap_η₀ :S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) εh_μ_η_int :∀ a : Bool, Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μw :γ → ℝhw_meas :h_phi_int :Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μh_phiw_int :Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) * w (S.toBackdoorEstimationSystem.factualX ω)) P.μProof (Lean source)
theorem integral_phiDiff_mul_eq_condBias (S : CATEEstimationSystem P γ) (hA : S.toPOBackdoorSystem.Assumptions) (η : NuisanceVec γ) {ε : ℝ} (hε_pos : 0 < ε) (h_overlap_η : η ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (h_overlap_η₀ : S.toBackdoorEstimationSystem.η₀ ∈ BackdoorEstimationSystem.H_ε (γ := γ) ε) (h_μ_η_int : ∀ a : Bool, Integrable (fun ω => η.μ_fn a (S.toBackdoorEstimationSystem.factualX ω)) P.μ) (w : γ → ℝ) (hw_meas : Measurable w) (h_phi_int : Integrable (fun ω => phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) P.μ) (h_phiw_int : Integrable (fun ω => (phi_eta (S.toBackdoorEstimationSystem.factualZ ω) η - phi₀ S (S.toBackdoorEstimationSystem.factualZ ω)) * w (S.toBackdoorEstimationSystem.factualX ω)) P.μ) : ∫ z, (phi_eta z η - phi₀ S z) * w z.1 ∂S.toBackdoorEstimationSystem.P_Z = ∫ x, condBias η S.toBackdoorEstimationSystem.η₀ x * w x ∂S.toBackdoorEstimationSystem.P_X := by set X := S.toPOBackdoorSystem.factualX with hX set Z := S.toBackdoorEstimationSystem.factualZ with hZ -- The conditional-bias identity (σ(X)-form). have hcond := phi_eta_minus_phi₀_cond_exp S hA η h_overlap_η h_overlap_η₀ hε_pos h_μ_η_int -- σ(X)-strong measurability of `w ∘ X`. have hw_sm : StronglyMeasurable[S.toPOBackdoorSystem.sigmaX] (fun ω => w (X ω)) := by change StronglyMeasurable[ comap S.toPOBackdoorSystem.factualX inferInstance] (fun ω => w (S.toPOBackdoorSystem.factualX ω)) exact (hw_meas.comp (comap_measurable S.toPOBackdoorSystem.factualX)).stronglyMeasurable -- Pull `w ∘ X` out of the conditional expectation of `(phi_eta − phi₀) ∘ Z`. have hpull := MeasureTheory.condExp_mul_of_stronglyMeasurable_right (μ := P.μ) (m := S.toPOBackdoorSystem.sigmaX) hw_sm h_phiw_int h_phi_int -- Hence `E[(phi_eta − phi₀)·(w∘X) | σX] =ᵐ (w∘X)·(condBias ∘ X)`. have hcond_mul : P.μ[fun ω => (phi_eta (Z ω) η - phi₀ S (Z ω)) * w (X ω) | S.toPOBackdoorSystem.sigmaX] =ᵐ[P.μ] (fun ω => w (X ω) * condBias η S.toBackdoorEstimationSystem.η₀ (X ω)) := by refine hpull.trans ?_ filter_upwards [hcond] with ω hω rw [Pi.mul_apply, hω]; simp only [hX]; ring calc ∫ z, (phi_eta z η - phi₀ S z) * w z.1 ∂S.toBackdoorEstimationSystem.P_Z = ∫ ω, (phi_eta (Z ω) η - phi₀ S (Z ω)) * w (X ω) ∂P.μ := by rw [BackdoorEstimationSystem.P_Z, MeasureTheory.integral_map S.toBackdoorEstimationSystem.measurable_factualZ.aemeasurable (by refine ((measurable_phi_eta η).sub (measurable_phi₀ S)).mul (hw_meas.comp measurable_fst) |>.aestronglyMeasurable)] rfl _ = ∫ ω, P.μ[fun ω => (phi_eta (Z ω) η - phi₀ S (Z ω)) * w (X ω) | S.toPOBackdoorSystem.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.toPOBackdoorSystem.sigmaX_le] _ = ∫ ω, w (X ω) * condBias η S.toBackdoorEstimationSystem.η₀ (X ω) ∂P.μ := MeasureTheory.integral_congr_ae hcond_mul _ = ∫ x, condBias η S.toBackdoorEstimationSystem.η₀ x * w x ∂S.toBackdoorEstimationSystem.P_X := by rw [BackdoorEstimationSystem.P_X, MeasureTheory.integral_map S.toPOBackdoorSystem.measurable_factualX.aemeasurable (by refine (((measurable_condBias η S.toBackdoorEstimationSystem.η₀).mul hw_meas)).aestronglyMeasurable)] refine MeasureTheory.integral_congr_ae (Filter.Eventually.of_forall fun ω => ?_) simp only [hX]; ring