Estimation.DTR.RemainderIdentity
Algebraic helpers for the exact second-order remainder identity of the dynamic-treatment-regime moment.
RemainderIdentity 1 core · 0 supporting Proves the stagewise cross-product remainder identity for sequential doubly robust DTR scores. ★ seqDR_remainder_identity
Proves the stagewise cross-product remainder identity for sequential doubly robust DTR scores. The identity decomposes the population moment error into nuisance-error products for the dynamic treatment rule.
lemma seqDR_remainder_identity reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Sequential DR (DTR, n = 2) remainder identity. Consider a two-stage dynamic treatment-regime estimation system satisfying the sequential causal assumptions (consistency and sequential ignorability), for which the stage-0 and stage-1 propensity scores are bounded within a margin ε of 0 and 1 (strict overlap), and where the factual outcome and the potential outcome under every fixed treatment regime each have finite second moment. For any candidate nuisance vector η whose stage-0 and stage-1 propensities likewise lie in this strict-overlap band, and whose stage-0 outcome-regression error, stage-1 outcome-regression error, stage-0 propensity error, and stage-1 propensity error are each square-integrable against the corresponding stage's history law, the population sequential doubly robust moment at η and the true target θ₀ equals the sum of two stagewise cross-product integrals — propensity error times inverse-propensity weight times outcome-regression error, at stage 0 against the stage-0 history law and at stage 1 against the stage-1 history law.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPODTRSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
_h_yd2 :
∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ
η :
DTRNuisanceVec₂ δ γ
hη :
η ∈ DTREstimationSystem.H_ε ε
hΔμ₀_memLp :
MemLp (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀
hΔμ₁_memLp :
MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁
hΔe₀_memLp :
MemLp (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀
hΔe₁_memLp :
MemLp (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁
conclusion
∫ z, S.seqDRMomentFunctional η z S.θ₀ ∂(S.P_Z)
= (∫ s₀, (η.e₀_fn s₀ - S.e₀_val s₀) * (1 / η.e₀_fn s₀) * (η.μ₀_fn s₀ - S.μ₀_val s₀) ∂(S.P_H₀))
+ (∫ h, indEq h.2.1 (S.dbar 0) * (η.e₁_fn h - S.e₁_val h) * (1 / (η.e₀_fn h.2.2 * η.e₁_fn h)) * (η.μ₁_fn h - S.μ₁_val h) ∂(S.P_H₁))
Proof (Lean source)
lemma seqDR_remainder_identity
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(hA : S.toPODTRSystem.Assumptions)
(h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ)
(_h_yd2 : ∀ dbar : Fin 2 → δ, Integrable
(fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ)
(η : DTRNuisanceVec₂ δ γ) (hη : η ∈ DTREstimationSystem.H_ε ε)
(hΔμ₀_memLp : MemLp (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀)
(hΔμ₁_memLp : MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁)
(hΔe₀_memLp : MemLp (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀)
(hΔe₁_memLp : MemLp (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁) :
∫ z, S.seqDRMomentFunctional η z S.θ₀ ∂(S.P_Z)
=
(∫ s₀, (η.e₀_fn s₀ - S.e₀_val s₀)
* (1 / η.e₀_fn s₀)
* (η.μ₀_fn s₀ - S.μ₀_val s₀) ∂(S.P_H₀))
+
(∫ h, indEq h.2.1 (S.dbar 0)
* (η.e₁_fn h - S.e₁_val h)
* (1 / (η.e₀_fn h.2.2 * η.e₁_fn h))
* (η.μ₁_fn h - S.μ₁_val h) ∂(S.P_H₁)) := by
let S0 : P.Ω → γ 0 := S.toPODTRSystem.factualS ⟨0, by decide⟩
let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω =>
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)
let Y : P.Ω → ℝ := S.toPODTRSystem.factualY
let I0 : P.Ω → ℝ :=
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩)
let I1 : P.Ω → ℝ :=
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩)
let M0 : P.Ω → ℝ := fun ω => S.μ₀_val (S0 ω)
let M1 : P.Ω → ℝ := fun ω => S.μ₁_val (H1 ω)
let dμ0 : P.Ω → ℝ := fun ω => η.μ₀_fn (S0 ω) - S.μ₀_val (S0 ω)
let dμ1 : P.Ω → ℝ := fun ω => η.μ₁_fn (H1 ω) - S.μ₁_val (H1 ω)
let G0 : P.Ω → ℝ := fun ω => 1 / η.e₀_fn (S0 ω)
let G1 : P.Ω → ℝ := fun ω => 1 / (η.e₀_fn (S0 ω) * η.e₁_fn (H1 ω))
let base : P.Ω → ℝ := fun ω => M0 ω - S.θ₀
let R0 : P.Ω → ℝ := fun ω => I0 ω * (M1 ω - M0 ω)
let R1 : P.Ω → ℝ := fun ω => I0 ω * (I1 ω * (Y ω - M1 ω))
let r0 : P.Ω → ℝ := fun ω => G0 ω * R0 ω
let r1 : P.Ω → ℝ := fun ω => G1 ω * R1 ω
let i0 : P.Ω → ℝ := fun ω => I0 ω * G0 ω * dμ0 ω
let i10 : P.Ω → ℝ := fun ω => I0 ω * G0 ω * dμ1 ω
let i11 : P.Ω → ℝ := fun ω => I0 ω * I1 ω * G1 ω * dμ1 ω
let p0 : P.Ω → ℝ := fun ω =>
(dμ0 ω / η.e₀_fn (S0 ω)) * S.e₀_val (S0 ω)
let p1 : P.Ω → ℝ := fun ω =>
indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) (S.dbar ⟨0, by decide⟩) *
(dμ1 ω / (η.e₀_fn (S0 ω) * η.e₁_fn (H1 ω))) * S.e₁_val (H1 ω)
let crossInd : P.Ω → ℝ := fun ω => dμ0 ω + i10 ω - i0 ω - i11 ω
let crossProp : P.Ω → ℝ := fun ω => dμ0 ω + i10 ω - p0 ω - p1 ω
let rem0 : γ 0 → ℝ := fun s₀ =>
(η.e₀_fn s₀ - S.e₀_val s₀) * (1 / η.e₀_fn s₀) *
(η.μ₀_fn s₀ - S.μ₀_val s₀)
let rem1 : γ 1 × δ × γ 0 → ℝ := fun h =>
indEq h.2.1 (S.dbar 0) *
(η.e₁_fn h - S.e₁_val h) *
(1 / (η.e₀_fn h.2.2 * η.e₁_fn h)) *
(η.μ₁_fn h - S.μ₁_val h)
let remΩ : P.Ω → ℝ := fun ω => rem0 (S0 ω) + rem1 (H1 ω)
have hS0_meas : Measurable S0 := by
dsimp [S0]
exact S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩
have hH1_meas : Measurable H1 := by
dsimp [H1]
exact (S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩))
have hM0_int : Integrable M0 P.μ := by
let B0 := S.toPODTRSystem.historyBundle 0 (by decide)
exact (B0.integrable_condExpGiven (S.toPODTRSystem.Y_of S.dbar)).congr
(by simpa [B0, M0, S0] using S.μ₀_compat hA)
have hM1_int : Integrable M1 P.μ := by
let B1 := S.toPODTRSystem.historyBundle 1 (by decide)
have hM1_L2 : MemLp M1 2 P.μ := by
simpa [M1, H1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq
(S.μ₁_val_comp_eq_stageOneReg).symm
exact hM1_L2.integrable (by norm_num)
have hM0_meas : Measurable M0 := by
dsimp [M0]
exact S.μ₀_meas.comp hS0_meas
have hM1_meas : Measurable M1 := by
dsimp [M1]
exact S.μ₁_meas.comp hH1_meas
have hI0M0_int : Integrable (fun ω => I0 ω * M0 ω) P.μ := by
have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator
(S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hM0_int
exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, M0, mul_comm]))
have hI0M1_int : Integrable (fun ω => I0 ω * M1 ω) P.μ := by
have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator
(S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hM1_int
exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, M1, mul_comm]))
have hR0_int : Integrable R0 P.μ := by
have hsub := hI0M1_int.sub hI0M0_int
refine hsub.congr ?_
exact Filter.Eventually.of_forall (fun ω => by
simp [R0]
ring)
have hI1Y_int : Integrable (fun ω => I1 ω * Y ω) P.μ := by
have h := (S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_mul_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _) hA.integrable_factualY
exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I1, Y, mul_comm]))
have hI1M1_int : Integrable (fun ω => I1 ω * M1 ω) P.μ := by
have h := (S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_mul_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _) hM1_int
exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I1, M1, mul_comm]))
have hI1_res_int :
Integrable (fun ω => I1 ω * (Y ω - M1 ω)) P.μ := by
have hsub := hI1Y_int.sub hI1M1_int
refine hsub.congr ?_
exact Filter.Eventually.of_forall (fun ω => by
rw [Pi.sub_apply]
ring)
have hI1_res_meas : Measurable (fun ω => I1 ω * (Y ω - M1 ω)) := by
exact ((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)).mul
(S.toPODTRSystem.measurable_factualY.sub hM1_meas)
have hR1_int : Integrable R1 P.μ := by
have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator
(S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hI1_res_int
exact h.congr (Filter.Eventually.of_forall (fun ω => by
change (I1 ω * (Y ω - M1 ω)) * I0 ω = R1 ω
simp [R1]
ring))
have hη0_lower : ∀ s₀, ε ≤ η.e₀_fn s₀ := fun s₀ => (hη.1 s₀).1
have hη1_lower : ∀ h, ε ≤ η.e₁_fn h := fun h => (hη.2 h).1
have hη0_pos : ∀ s₀, 0 < η.e₀_fn s₀ :=
fun s₀ => lt_of_lt_of_le h_overlap.1 (hη0_lower s₀)
have hη1_pos : ∀ h, 0 < η.e₁_fn h :=
fun h => lt_of_lt_of_le h_overlap.1 (hη1_lower h)
have hG0_meas : Measurable G0 := by
dsimp [G0]
exact measurable_const.div (η.e₀_meas.comp hS0_meas)
have hG1_meas : Measurable G1 := by
dsimp [G1]
exact measurable_const.div ((η.e₀_meas.comp hS0_meas).mul
(η.e₁_meas.comp hH1_meas))
have hG0_bound : ∀ᵐ ω ∂P.μ, ‖G0 ω‖ ≤ ε⁻¹ := by
refine Filter.Eventually.of_forall ?_
intro ω
have hle : (η.e₀_fn (S0 ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ (hη0_pos (S0 ω)) h_overlap.1).2 (hη0_lower (S0 ω))
change ‖1 / η.e₀_fn (S0 ω)‖ ≤ ε⁻¹
rw [norm_div, norm_one, Real.norm_eq_abs, abs_of_pos (hη0_pos (S0 ω))]
simpa [one_div] using hle
have hG1_bound : ∀ᵐ ω ∂P.μ, ‖G1 ω‖ ≤ (ε * ε)⁻¹ := by
refine Filter.Eventually.of_forall ?_
intro ω
have hpos0 : 0 < η.e₀_fn (S0 ω) := hη0_pos (S0 ω)
have hpos1 : 0 < η.e₁_fn (H1 ω) := hη1_pos (H1 ω)
have hprod_le : ε * ε ≤ η.e₀_fn (S0 ω) * η.e₁_fn (H1 ω) :=
mul_le_mul (hη0_lower (S0 ω)) (hη1_lower (H1 ω))
h_overlap.1.le hpos0.le
have hle : (η.e₀_fn (S0 ω) * η.e₁_fn (H1 ω))⁻¹ ≤ (ε * ε)⁻¹ :=
(inv_le_inv₀ (mul_pos hpos0 hpos1)
(mul_pos h_overlap.1 h_overlap.1)).2 hprod_le
change ‖1 / (η.e₀_fn (S0 ω) * η.e₁_fn (H1 ω))‖ ≤ (ε * ε)⁻¹
rw [norm_div, norm_one, Real.norm_eq_abs, abs_of_pos (mul_pos hpos0 hpos1)]
simpa [one_div] using hle
have hr0_int : Integrable r0 P.μ := by
exact hR0_int.bdd_mul hG0_meas.aestronglyMeasurable hG0_bound
have hr1_int : Integrable r1 P.μ := by
exact hR1_int.bdd_mul hG1_meas.aestronglyMeasurable hG1_bound
have hi0_int : Integrable i0 P.μ := by
simpa [i0, I0, G0, dμ0, S0, mul_assoc] using
indicator_weighted_delta_mu0_integrable S h_overlap.1 η hη hΔμ₀_memLp
have hi10_int : Integrable i10 P.μ := by
simpa [i10, I0, G0, dμ1, H1, S0, mul_assoc] using
indicator_weighted_delta_mu1_stage0_integrable S h_overlap.1 η hη hΔμ₁_memLp
have hi11_int : Integrable i11 P.μ := by
simpa [i11, I0, I1, G1, dμ1, H1, S0, mul_assoc] using
indicator_weighted_delta_mu1_stage1_integrable S h_overlap.1 η hη hΔμ₁_memLp
have hdμ0_L2 : MemLp dμ0 2 P.μ := by
have hd := MemLp.comp_of_map (f := S0) hΔμ₀_memLp hS0_meas.aemeasurable
simpa [dμ0, S0, DTREstimationSystem.P_H₀, Function.comp_def] using hd
have hdμ1_L2 : MemLp dμ1 2 P.μ := by
have hd := MemLp.comp_of_map (f := H1) hΔμ₁_memLp hH1_meas.aemeasurable
simpa [dμ1, H1, DTREstimationSystem.P_H₁, Function.comp_def] using hd
have hdμ0_int : Integrable dμ0 P.μ := hdμ0_L2.integrable (by norm_num)
have hdμ1_int : Integrable dμ1 P.μ := hdμ1_L2.integrable (by norm_num)
have hbase_int : Integrable base P.μ := by
have h : Integrable (fun ω => M0 ω - S.θ₀) P.μ := hM0_int.sub (integrable_const S.θ₀)
simpa [base] using h
have hcrossInd_int : Integrable crossInd P.μ := by
have h : Integrable (fun ω => dμ0 ω + i10 ω - i0 ω - i11 ω) P.μ :=
((hdμ0_int.add hi10_int).sub hi0_int).sub hi11_int
simpa [crossInd, sub_eq_add_neg, add_assoc] using h
have hbase_zero : ∫ ω, base ω ∂P.μ = 0 := by
have hθ : S.θ₀ = ∫ ω, M0 ω ∂P.μ := by
simpa [M0, S0] using theta_zero_factualS₀_integral S hA
have hconst : (∫ _ : P.Ω, S.θ₀ ∂P.μ) = S.θ₀ := by
haveI : IsProbabilityMeasure P.μ := inferInstance
simp
calc
∫ ω, base ω ∂P.μ
= (∫ ω, M0 ω ∂P.μ) - ∫ _ : P.Ω, S.θ₀ ∂P.μ := by
rw [show base = (fun ω => M0 ω - S.θ₀) from rfl]
exact integral_sub hM0_int (integrable_const S.θ₀)
_ = S.θ₀ - S.θ₀ := by rw [← hθ, hconst]
_ = 0 := by ring
have hr0_zero : ∫ ω, r0 ω ∂P.μ = 0 := by
have hg_meas : Measurable (fun s₀ => 1 / η.e₀_fn s₀) :=
measurable_const.div η.e₀_meas
have h_int : Integrable
(fun ω => (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) *
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω *
(S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) -
S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) P.μ := by
simpa [S0, H1, G0, R0, r0, I0, M0, M1, mul_assoc] using hr0_int
calc
∫ ω, r0 ω ∂P.μ
= ∫ ω, (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) *
-- … truncated; follow the source link for the rest …
Helpers 1 core · 7 supporting This file provides the helper lemmas used to expand the two-stage sequential doubly robust DTR remainder identity. ★ split_stage_history_integral
Sequential DR Remainder Helpers
This file provides the helper lemmas used to expand the two-stage sequential
doubly robust DTR remainder identity. It relates factual treatment equality
checks to the target-regime indicators (indEq_factualD0_eq_indicator,
indEq_factualD1_eq_indicator), extracts positivity from the overlap-bounded
nuisance set (eta_e0_pos_of_mem_Hε, eta_e1_pos_of_mem_Hε), proves the
indicator-weighted outcome-regression error terms are integrable, and supplies
split_stage_history_integral to split integrals over the full observed DTR
law into the stage-history marginals P_H₀ and P_H₁.
lemma split_stage_history_integral reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Additivity of stage-history integrals under the joint DTR data law. Consider a real-valued function f₀ of the stage-0 state that is measurable and integrable against the stage-0 history marginal law and a real-valued function f₁ of the stage-1 history (current state, previous treatment, previous state) that is measurable and integrable against the stage-1 history marginal law. Then the integral, against the joint law of the observed two-stage data tuple, of the sum of f₀ and f₁ each pulled back through its respective projection out of the data tuple equals the sum of the separate integrals of f₀ against the stage-0 marginal law and f₁ against the stage-1 marginal law.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
f₀ :
γ 0 → ℝ
f₁ :
γ 1 × δ × γ 0 → ℝ
hf₀_meas :
Measurable f₀
hf₁_meas :
Measurable f₁
hf₀_int :
Integrable f₀ S.P_H₀
hf₁_int :
Integrable f₁ S.P_H₁
Proof (Lean source)
lemma split_stage_history_integral
(S : DTREstimationSystem P δ γ)
(f₀ : γ 0 → ℝ) (f₁ : γ 1 × δ × γ 0 → ℝ)
(hf₀_meas : Measurable f₀) (hf₁_meas : Measurable f₁)
(hf₀_int : Integrable f₀ S.P_H₀)
(hf₁_int : Integrable f₁ S.P_H₁) :
∫ z, f₀ (projS₀ z) + f₁ (histH₁ z) ∂(S.P_Z)
= ∫ s₀, f₀ s₀ ∂(S.P_H₀) + ∫ h, f₁ h ∂(S.P_H₁) := by
have hcomp₀_int :
Integrable (fun z : γ 0 × δ × γ 1 × δ × ℝ => f₀ (projS₀ z)) S.P_Z := by
rw [← P_Z_map_projS₀_eq_P_H₀ S] at hf₀_int
exact (MeasureTheory.integrable_map_measure
hf₀_meas.aestronglyMeasurable measurable_projS₀.aemeasurable).1 hf₀_int
have hcomp₁_int :
Integrable (fun z : γ 0 × δ × γ 1 × δ × ℝ => f₁ (histH₁ z)) S.P_Z := by
rw [← P_Z_map_histH₁_eq_P_H₁ S] at hf₁_int
exact (MeasureTheory.integrable_map_measure
hf₁_meas.aestronglyMeasurable measurable_histH₁.aemeasurable).1 hf₁_int
calc
∫ z, f₀ (projS₀ z) + f₁ (histH₁ z) ∂(S.P_Z)
= ∫ z, f₀ (projS₀ z) ∂(S.P_Z) +
∫ z, f₁ (histH₁ z) ∂(S.P_Z) := by
exact MeasureTheory.integral_add hcomp₀_int hcomp₁_int
_ = ∫ s₀, f₀ s₀ ∂(S.P_H₀) +
∫ h, f₁ h ∂(S.P_H₁) := by
have hmap₀ :
∫ z, f₀ (projS₀ z) ∂(S.P_Z) = ∫ s₀, f₀ s₀ ∂(S.P_H₀) := by
rw [← MeasureTheory.integral_map measurable_projS₀.aemeasurable
hf₀_meas.aestronglyMeasurable]
rw [P_Z_map_projS₀_eq_P_H₀ S]
have hmap₁ :
∫ z, f₁ (histH₁ z) ∂(S.P_Z) = ∫ h, f₁ h ∂(S.P_H₁) := by
rw [← MeasureTheory.integral_map measurable_histH₁.aemeasurable
hf₁_meas.aestronglyMeasurable]
rw [P_Z_map_histH₁_eq_P_H₁ S]
rw [hmap₀, hmap₁]
7 supporting declarations (lemmas, instances)
-
indEq_factualD0_eq_indicatorlemma — The stage-zero equality indicator agrees with the stage-zero treatment indicator for the target regime.hypothesesS :DTREstimationSystem P δ γω :P.ΩProof (Lean source)
lemma indEq_factualD0_eq_indicator (S : DTREstimationSystem P δ γ) (ω : P.Ω) : indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) (S.dbar ⟨0, by decide⟩) = (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω := by by_cases hD : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · have hI : (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω = 1 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one hD have hDn : S.toPODTRSystem.factualD 0 ω = S.dbar 0 := by simpa using hD have hIn : (S.toPODTRSystem.dVar 0).indicator (S.dbar 0) ω = 1 := by simpa using hI simp [indEq, hDn, hIn] · have hI : (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω = 0 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero hD have hDn : ¬ S.toPODTRSystem.factualD 0 ω = S.dbar 0 := by simpa using hD have hIn : (S.toPODTRSystem.dVar 0).indicator (S.dbar 0) ω = 0 := by simpa using hI simp [indEq, hDn, hIn] -
indEq_factualD1_eq_indicatorlemma — The stage-one equality indicator agrees with the stage-one treatment indicator for the target regime.hypothesesS :DTREstimationSystem P δ γω :P.ΩProof (Lean source)
lemma indEq_factualD1_eq_indicator (S : DTREstimationSystem P δ γ) (ω : P.Ω) : indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) (S.dbar ⟨1, by decide⟩) = (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω := by by_cases hD : S.toPODTRSystem.factualD ⟨1, by decide⟩ ω = S.dbar ⟨1, by decide⟩ · have hI : (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω = 1 := (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_one hD have hDn : S.toPODTRSystem.factualD 1 ω = S.dbar 1 := by simpa using hD have hIn : (S.toPODTRSystem.dVar 1).indicator (S.dbar 1) ω = 1 := by simpa using hI simp [indEq, hDn, hIn] · have hI : (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω = 0 := (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_zero hD have hDn : ¬ S.toPODTRSystem.factualD 1 ω = S.dbar 1 := by simpa using hD have hIn : (S.toPODTRSystem.dVar 1).indicator (S.dbar 1) ω = 0 := by simpa using hI simp [indEq, hDn, hIn] -
eta_e0_pos_of_mem_Hεlemma — Any nuisance vector in the overlap-bounded set has a positive stage-zero propensity.hypothesesη :DTRNuisanceVec₂ δ γε :ℝhε :0 < εhη :η ∈ DTREstimationSystem.H_ε (δ := δ) (γ := γ) εs₀ :γ 0conclusion0 < η.e₀_fn s₀Proof (Lean source)
lemma eta_e0_pos_of_mem_Hε {η : DTRNuisanceVec₂ δ γ} {ε : ℝ} (hε : 0 < ε) (hη : η ∈ DTREstimationSystem.H_ε (δ := δ) (γ := γ) ε) (s₀ : γ 0) : 0 < η.e₀_fn s₀ := lt_of_lt_of_le hε (hη.1 s₀).1 -
eta_e1_pos_of_mem_Hεlemma — Any nuisance vector in the overlap-bounded set has a positive stage-one propensity.hypothesesη :DTRNuisanceVec₂ δ γε :ℝhε :0 < εhη :η ∈ DTREstimationSystem.H_ε (δ := δ) (γ := γ) εh :γ 1 × δ × γ 0conclusion0 < η.e₁_fn hProof (Lean source)
lemma eta_e1_pos_of_mem_Hε {η : DTRNuisanceVec₂ δ γ} {ε : ℝ} (hε : 0 < ε) (hη : η ∈ DTREstimationSystem.H_ε (δ := δ) (γ := γ) ε) (h : γ 1 × δ × γ 0) : 0 < η.e₁_fn h := lt_of_lt_of_le hε (hη.2 h).1 -
indicator_weighted_delta_mu0_integrablelemma — The stage-zero indicator-weighted stage-zero outcome-regression error is integrable.hypothesesS :DTREstimationSystem P δ γε :ℝhε :0 < εη :DTRNuisanceVec₂ δ γhη :η ∈ DTREstimationSystem.H_ε εhΔμ₀_memLp :MemLp (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀conclusionIntegrable (fun ω => (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) * (η.μ₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μProof (Lean source)
lemma indicator_weighted_delta_mu0_integrable (S : DTREstimationSystem P δ γ) {ε : ℝ} (hε : 0 < ε) (η : DTRNuisanceVec₂ δ γ) (hη : η ∈ DTREstimationSystem.H_ε ε) (hΔμ₀_memLp : MemLp (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀) : Integrable (fun ω => (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) * (η.μ₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μ := by let I0 : P.Ω → ℝ := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let W0 : P.Ω → ℝ := fun ω => I0 ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) let dμ0 : P.Ω → ℝ := fun ω => η.μ₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hdμ0_L2 : MemLp dμ0 2 P.μ := by have hd := MemLp.comp_of_map (f := S.toPODTRSystem.factualS ⟨0, by decide⟩) hΔμ₀_memLp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable exact hd have hW0_meas : Measurable W0 := by dsimp [W0, I0] exact ((S.toPODTRSystem.dVar ⟨0, by decide⟩).measurable_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _)).mul (measurable_const.div (η.e₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩))) have hW0_bound : ∀ᵐ ω ∂P.μ, ‖W0 ω‖ ≤ ε⁻¹ := by refine Filter.Eventually.of_forall ?_ intro ω by_cases hD : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · have hI : I0 ω = 1 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one hD have hpos := eta_e0_pos_of_mem_Hε hε hη (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hle : (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos hε).2 (hη.1 (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)).1 have hle_abs : |η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)|⁻¹ ≤ ε⁻¹ := by rw [abs_of_pos hpos] exact hle simpa [W0, hI, one_div, Real.norm_eq_abs] using hle_abs · have hI : I0 ω = 0 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero hD have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr hε.le simpa [W0, hI] using hεinv_nonneg have hW0_Linf : MemLp W0 ⊤ P.μ := MemLp.of_bound hW0_meas.aestronglyMeasurable ε⁻¹ hW0_bound have hL2 : MemLp (fun ω => W0 ω * dμ0 ω) 2 P.μ := hdμ0_L2.mul hW0_Linf exact (hL2.integrable (by norm_num)).congr (Filter.Eventually.of_forall (fun ω => by simp [W0, I0, dμ0])) -
indicator_weighted_delta_mu1_stage0_integrablelemma — The stage-zero indicator-weighted stage-one outcome-regression error is integrable.hypothesesS :DTREstimationSystem P δ γε :ℝhε :0 < εη :DTRNuisanceVec₂ δ γhη :η ∈ DTREstimationSystem.H_ε εhΔμ₁_memLp :MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁conclusionIntegrable (fun ω => (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) * (η.μ₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μProof (Lean source)
lemma indicator_weighted_delta_mu1_stage0_integrable (S : DTREstimationSystem P δ γ) {ε : ℝ} (hε : 0 < ε) (η : DTRNuisanceVec₂ δ γ) (hη : η ∈ DTREstimationSystem.H_ε ε) (hΔμ₁_memLp : MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁) : Integrable (fun ω => (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) * (η.μ₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μ := by let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω => (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) let I0 : P.Ω → ℝ := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let W0 : P.Ω → ℝ := fun ω => I0 ω * (1 / η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) let dμ1 : P.Ω → ℝ := fun ω => η.μ₁_fn (H1 ω) - S.μ₁_val (H1 ω) have hH1_meas : Measurable H1 := by dsimp [H1] exact (S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod ((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)) have hdμ1_L2 : MemLp dμ1 2 P.μ := by have hd := MemLp.comp_of_map (f := H1) hΔμ₁_memLp hH1_meas.aemeasurable exact hd have hW0_meas : Measurable W0 := by dsimp [W0, I0] exact ((S.toPODTRSystem.dVar ⟨0, by decide⟩).measurable_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _)).mul (measurable_const.div (η.e₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩))) have hW0_bound : ∀ᵐ ω ∂P.μ, ‖W0 ω‖ ≤ ε⁻¹ := by refine Filter.Eventually.of_forall ?_ intro ω by_cases hD : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · have hI : I0 ω = 1 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one hD have hpos := eta_e0_pos_of_mem_Hε hε hη (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hle : (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ := (inv_le_inv₀ hpos hε).2 (hη.1 (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)).1 have hle_abs : |η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)|⁻¹ ≤ ε⁻¹ := by rw [abs_of_pos hpos] exact hle simpa [W0, hI, one_div, Real.norm_eq_abs] using hle_abs · have hI : I0 ω = 0 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero hD have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr hε.le simpa [W0, hI] using hεinv_nonneg have hW0_Linf : MemLp W0 ⊤ P.μ := MemLp.of_bound hW0_meas.aestronglyMeasurable ε⁻¹ hW0_bound have hL2 : MemLp (fun ω => W0 ω * dμ1 ω) 2 P.μ := hdμ1_L2.mul hW0_Linf exact (hL2.integrable (by norm_num)).congr (Filter.Eventually.of_forall (fun ω => by simp [W0, I0, dμ1, H1])) -
indicator_weighted_delta_mu1_stage1_integrablelemma — The double-indicator-weighted stage-one outcome-regression error is integrable.hypothesesS :DTREstimationSystem P δ γε :ℝhε :0 < εη :DTRNuisanceVec₂ δ γhη :η ∈ DTREstimationSystem.H_ε εhΔμ₁_memLp :MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁conclusionIntegrable (fun ω => ((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω * (1 / (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) * (η.μ₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μProof (Lean source)
lemma indicator_weighted_delta_mu1_stage1_integrable (S : DTREstimationSystem P δ γ) {ε : ℝ} (hε : 0 < ε) (η : DTRNuisanceVec₂ δ γ) (hη : η ∈ DTREstimationSystem.H_ε ε) (hΔμ₁_memLp : MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁) : Integrable (fun ω => ((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω * (1 / (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) * (η.μ₁_fn (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) P.μ := by let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω => (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) let I0 : P.Ω → ℝ := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let I1 : P.Ω → ℝ := (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) let W1 : P.Ω → ℝ := fun ω => I0 ω * I1 ω * (1 / (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (H1 ω))) let dμ1 : P.Ω → ℝ := fun ω => η.μ₁_fn (H1 ω) - S.μ₁_val (H1 ω) have hH1_meas : Measurable H1 := by dsimp [H1] exact (S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod ((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)) have hdμ1_L2 : MemLp dμ1 2 P.μ := by have hd := MemLp.comp_of_map (f := H1) hΔμ₁_memLp hH1_meas.aemeasurable exact hd have hW1_meas : Measurable W1 := by dsimp [W1, I0, I1, H1] exact (((S.toPODTRSystem.dVar ⟨0, by decide⟩).measurable_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _)).mul ((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator (S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _))).mul (measurable_const.div ((η.e₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)).mul (η.e₁_meas.comp hH1_meas))) have hW1_bound : ∀ᵐ ω ∂P.μ, ‖W1 ω‖ ≤ (ε * ε)⁻¹ := by refine Filter.Eventually.of_forall ?_ intro ω by_cases hD0 : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · by_cases hD1 : S.toPODTRSystem.factualD ⟨1, by decide⟩ ω = S.dbar ⟨1, by decide⟩ · have hI0 : I0 ω = 1 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one hD0 have hI1 : I1 ω = 1 := (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_one hD1 have hpos0 := eta_e0_pos_of_mem_Hε hε hη (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hpos1 := eta_e1_pos_of_mem_Hε hε hη (H1 ω) have hprod_le : ε * ε ≤ η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (H1 ω) := mul_le_mul (hη.1 (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)).1 (hη.2 (H1 ω)).1 hε.le hpos0.le have hle : (η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (H1 ω))⁻¹ ≤ (ε * ε)⁻¹ := (inv_le_inv₀ (mul_pos hpos0 hpos1) (mul_pos hε hε)).2 hprod_le have hle_abs : |η.e₀_fn (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * η.e₁_fn (H1 ω)|⁻¹ ≤ (ε * ε)⁻¹ := by rw [abs_of_pos (mul_pos hpos0 hpos1)] exact hle simpa [W1, hI0, hI1, one_div, Real.norm_eq_abs] using hle_abs · have hI1 : I1 ω = 0 := (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_zero hD1 have hnonneg : 0 ≤ (ε * ε)⁻¹ := inv_nonneg.mpr (mul_nonneg hε.le hε.le) simpa [W1, hI1] using hnonneg · have hI0 : I0 ω = 0 := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero hD0 have hnonneg : 0 ≤ (ε * ε)⁻¹ := inv_nonneg.mpr (mul_nonneg hε.le hε.le) simpa [W1, hI0] using hnonneg have hW1_Linf : MemLp W1 ⊤ P.μ := MemLp.of_bound hW1_meas.aestronglyMeasurable (ε * ε)⁻¹ hW1_bound have hL2 : MemLp (fun ω => W1 ω * dμ1 ω) 2 P.μ := hdμ1_L2.mul hW1_Linf exact (hL2.integrable (by norm_num)).congr (Filter.Eventually.of_forall (fun ω => by simp [W1, I0, I1, dμ1, H1]))