Estimation.DTR
DML estimation for dynamic treatment regimes: the two-period AIPW moment, remainder identities and bounds, and the asymptotic-linearity theorem.
RemainderIdentity 2 core · 7 supporting · 1 submodule Proves the stagewise cross-product remainder identity for sequential doubly robust DTR scores. ScoreL2 4 core · 14 supporting · 1 submodule This module proves the L² continuity statement for the two-stage sequential doubly robust DTR score.
Setup 9 core · 7 supporting This file defines the data layer for two-stage dynamic treatment regime estimation: the estimation-system structure, observable regression targets, stagewise overlap, history marginals, the observed data law, and the val ★ θ₀_eq_dtrEffect
Two-Stage DTR Estimation Setup
This file defines the data layer for two-stage dynamic treatment regime estimation: the estimation-system structure, observable regression targets, stagewise overlap, history marginals, the observed data law, and the value-space target estimand. The target is the fixed-regime mean, and the observable compatibility fields are the value-space representatives used by the sequential AIPW score.
This module is specialized to horizon two, with a discrete treatment space so that target-regime equality indicators are measurable.
structure DTREstimationSystem reviewed
⚑ flagged
Causalean.Estimation.DTR
This structure extends a two-stage potential-outcome dynamic-treatment-regime system with, at a fixed target regime, measurable value-space representatives of the stage-0 and stage-1 outcome regressions and of the propensities at both stages, bounded away from zero and one, each required to agree almost surely with the corresponding observable conditional regression or propensity built from the factual treatment and covariate history.
Definition (Lean source)
parameters
P :
δ :
Type
γ :
Fin 2 → Type
∀ k, MeasurableSpace (γ k)
IsFiniteMeasure P.μ
extends :
PODTRSystem P 2 δ γ
fields
Target regime stored at the system level (mirrors the design rationale
in the brief: regime is multi-stage, so we fix it).
dbar :
Fin 2 → δ
Value-space stage-0 outcome regression `μ₀ : γ 0 → ℝ`.
μ₀_val :
γ 0 → ℝ
μ₀_meas :
Measurable μ₀_val
Value-space stage-0 propensity `e₀ : γ 0 → ℝ`, in `(0, 1)`.
e₀_val :
γ 0 → ℝ
e₀_meas :
Measurable e₀_val
e₀_pos :
∀ s, 0 < e₀_val s
e₀_lt_one :
∀ s, e₀_val s < 1
Value-space stage-1 outcome regression `μ₁ : γ 1 × δ × γ 0 → ℝ`.
μ₁_val :
γ 1 × δ × γ 0 → ℝ
μ₁_meas :
Measurable μ₁_val
Value-space stage-1 propensity `e₁ : γ 1 × δ × γ 0 → ℝ`, in `(0, 1)`.
e₁_val :
γ 1 × δ × γ 0 → ℝ
e₁_meas :
Measurable e₁_val
e₁_pos :
∀ h, 0 < e₁_val h
e₁_lt_one :
∀ h, e₁_val h < 1
The stage-0 (outermost) regression `μ₀_val` represents the **observable**
nested regression `innerReg dbar (n-1)` (the iterated g-computation regression on
the factual data), with NO counterfactual: `μ₀_val (factualS 0 ·) =ᵐ innerReg dbar 1`.
The counterfactual reading `μ[Y(dbar)|σ(historyBundle 0)] =ᵐ μ₀_val ∘ factualS 0` is
NOT assumed here — it is the *derived* lemma `μ₀_compat` below, which requires
`Assumptions` via the sequential back-door identity `cdtr_backdoor`.
μ₀_reg_compat :
(fun ω => μ₀_val (toPODTRSystem.factualS ⟨0, by decide⟩ ω))
=ᵐ[P.μ] toPODTRSystem.innerReg dbar 1
Stage-0 propensity factors through `factualS 0`:
`μ[1_{D₀ = dbar 0} | σ(historyBundle 0)] =ᵐ e₀_val (factualS 0 ·)`.
e₀_compat :
The stage-1 regression `μ₁_val` represents the **observable** last-stage
regression `f₂ = E[Y | hist₁, D₁=dbar₁]`, written as the ratio
`condExpRatio_{hist₁}(Y·1_{D₁=dbar₁}, 1_{D₁=dbar₁})` (the paper's nested-regression
base case), with NO counterfactual:
`μ₁_val (factualS 1, factualD 0, factualS 0) =ᵐ f₂`. This is the ML/regression
target. The counterfactual reading `μ[Y(dbar) | σ(hist₁)] =ᵐ μ₁_val ∘ …` holds only
on the regime path `{D₀=dbar₀}` (the `·indD` form `stageOneReg_indD_eq`), NOT
globally — which is exactly why `μ₁` is the regression `f₂`, not the full-regime
intermediate counterfactual.
μ₁_reg_compat :
(fun ω => μ₁_val (toPODTRSystem.factualS ⟨1, by decide⟩ ω, toPODTRSystem.factualD ⟨0, by decide⟩ ω, toPODTRSystem.factualS ⟨0, by decide⟩ ω))
Stage-1 propensity factors through `(factualS 1, factualD 0, factualS 0)`:
`μ[1_{D₁ = dbar 1} | σ(historyBundle 1)] =ᵐ e₁_val (factualS 1, factualD 0, factualS 0)`.
def stageOneReg reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the observable stage-1 regression of the outcome within the target final treatment arm.
Definition (Lean source)
noncomputable def stageOneReg (S : DTREstimationSystem P δ γ) : P.Ω → ℝ :=
(S.toPODTRSystem.historyBundle 1 (by decide)).condExpRatio
(fun ω => S.toPODTRSystem.factualY ω *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω)
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩)) P.μ
def StrictOverlap reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This predicate requires both stagewise target-regime propensities to stay uniformly away from zero and one.
Definition (Lean source)
def StrictOverlap (S : DTREstimationSystem P δ γ) (ε : ℝ) : Prop :=
0 < ε ∧ ε ≤ 1 / 2 ∧
(∀ᵐ ω ∂P.μ,
(ε ≤ (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩)) P.μ ω
∧ (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩)) P.μ ω
≤ 1 - ε)
∧ (ε ≤ (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩)) P.μ ω
∧ (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩)) P.μ ω
≤ 1 - ε))
def P_H₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the marginal law of the stage-0 history.
Definition (Lean source)
noncomputable def P_H₀ (S : DTREstimationSystem P δ γ) : Measure (γ 0) :=
P.μ.map (S.toPODTRSystem.factualS ⟨0, by decide⟩)
def P_H₁ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the marginal law of the stage-1 history in the DTR history ordering.
Definition (Lean source)
noncomputable def P_H₁ (S : DTREstimationSystem P δ γ) :
Measure (γ 1 × δ × γ 0) :=
P.μ.map (fun ω =>
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))
def factualZ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This map collects the full observed two-stage data tuple from the underlying outcome system.
Definition (Lean source)
noncomputable def factualZ (S : DTREstimationSystem P δ γ) :
P.Ω → γ 0 × δ × γ 1 × δ × ℝ :=
fun ω =>
(S.toPODTRSystem.factualS ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualY ω)
def P_Z reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the joint law of the full observed two-stage data tuple.
Definition (Lean source)
noncomputable def P_Z (S : DTREstimationSystem P δ γ) :
Measure (γ 0 × δ × γ 1 × δ × ℝ) :=
P.μ.map S.factualZ
def θ₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the fixed-regime mean outcome targeted by the two-stage DTR estimation system.
Definition (Lean source)
noncomputable def θ₀ (S : DTREstimationSystem P δ γ) : ℝ :=
S.toPODTRSystem.dtrEffect S.dbar
theorem θ₀_eq_dtrEffect reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a two-stage dynamic treatment regime estimation system, its value-space DTR estimand θ₀ equals the potential-outcome DTR effect evaluated at the chosen regime dbar.
Formal statement
Proof (Lean source)
theorem θ₀_eq_dtrEffect (S : DTREstimationSystem P δ γ) :
S.θ₀ = S.toPODTRSystem.dtrEffect S.dbar := rfl
7 supporting declarations (lemmas, instances)
-
μ₀_compatlemma — The stage-0 value-space regression equals the counterfactual stage-0 regression under identification.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.Assumptionsconclusion(S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ=ᵐ[P.μ] (fun ω => S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))Proof (Lean source)
lemma μ₀_compat (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ =ᵐ[P.μ] (fun ω => S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := (S.toPODTRSystem.cdtr_backdoor hA S.dbar (by decide)).trans S.μ₀_reg_compat.symm -
μ₁_val_comp_eq_stageOneReglemma — The stage-1 value-space regression agrees almost everywhere with the observable stage-1 regression.hypothesesS :DTREstimationSystem P δ γconclusion(fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))=ᵐ[P.μ] S.stageOneRegProof (Lean source)
lemma μ₁_val_comp_eq_stageOneReg (S : DTREstimationSystem P δ γ) : (fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) =ᵐ[P.μ] S.stageOneReg := S.μ₁_reg_compat -
stageOneReg_indD_eqlemma — On the regime-consistent path, the observable stage-1 regression agrees with the counterfactual stage-1 regression.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.Assumptionsconclusion(fun ω => S.stageOneReg ω * S.toPODTRSystem.indD S.dbar 1 ω)=ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω)Proof (Lean source)
lemma stageOneReg_indD_eq (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : (fun ω => S.stageOneReg ω * S.toPODTRSystem.indD S.dbar 1 ω) =ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω) := by let T := S.toPODTRSystem let kLast : Fin 2 := ⟨1, by decide⟩ let I1 : P.Ω → ℝ := (T.dVar kLast).indicator (S.dbar kLast) let B := T.historyBundle 1 (by decide) have hFactor : T.indD S.dbar 2 = fun ω => T.indD S.dbar 1 ω * I1 ω := by simpa [T, I1, kLast] using T.indD_factor_split S.dbar 1 (by decide) have hYI_int : Integrable (fun ω => T.factualY ω * I1 ω) P.μ := by simpa [T, I1, kLast] using (T.dVar kLast).integrable_mul_indicator (S.dbar kLast) (measurableSet_singleton (S.dbar kLast)) hA.integrable_factualY have hYindD2_int : Integrable (fun ω => T.factualY ω * T.indD S.dbar 2 ω) P.μ := by refine hA.integrable_factualY.mono (T.measurable_factualY.mul (T.measurable_indD S.dbar 2)).aestronglyMeasurable ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rcases T.indD_eq_zero_or_one S.dbar 2 ω with h0 | h1 · simp [T, h0] · simp [T, h1] have hprodY_int : Integrable (T.indD S.dbar 1 * fun ω => T.factualY ω * I1 ω) P.μ := by have hfun : (T.indD S.dbar 1 * fun ω => T.factualY ω * I1 ω) = fun ω => T.factualY ω * T.indD S.dbar 2 ω := by funext ω change T.indD S.dbar 1 ω * (T.factualY ω * I1 ω) = T.factualY ω * T.indD S.dbar 2 ω rw [hFactor] ring rw [hfun] exact hYindD2_int have hI1_int : Integrable I1 P.μ := by simpa [T, I1, kLast] using (T.dVar kLast).integrable_indicator (S.dbar kLast) have hindD2_int : Integrable (T.indD S.dbar 2) P.μ := T.indD_integrable S.dbar 2 have hprodI_int : Integrable (T.indD S.dbar 1 * I1) P.μ := by have hfun : (T.indD S.dbar 1 * I1) = T.indD S.dbar 2 := by funext ω change T.indD S.dbar 1 ω * I1 ω = T.indD S.dbar 2 ω rw [hFactor] rw [hfun] exact hindD2_int have hindD1_sm : StronglyMeasurable[B.sigma] (T.indD S.dbar 1) := by simpa [T, B] using T.stronglyMeasurable_indD_sigma_history 1 (by decide) S.dbar 1 (le_refl 1) have hNum_pull : B.condExpGiven (fun ω => T.factualY ω * T.indD S.dbar 2 ω) P.μ =ᵐ[P.μ] (fun ω => T.indD S.dbar 1 ω * B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω) := by have hpull := B.condExpGiven_mul_of_stronglyMeasurable_left (f := T.indD S.dbar 1) (g := fun ω => T.factualY ω * I1 ω) hindD1_sm hprodY_int hYI_int have harg : (fun ω => T.factualY ω * T.indD S.dbar 2 ω) = fun ω => T.indD S.dbar 1 ω * (T.factualY ω * I1 ω) := by funext ω rw [hFactor] ring rw [harg] filter_upwards [hpull] with ω hω exact hω have hDen_pull : B.condExpGiven (T.indD S.dbar 2) P.μ =ᵐ[P.μ] (fun ω => T.indD S.dbar 1 ω * B.condExpGiven I1 P.μ ω) := by have hpull := B.condExpGiven_mul_of_stronglyMeasurable_left (f := T.indD S.dbar 1) (g := I1) hindD1_sm hprodI_int hI1_int have harg : T.indD S.dbar 2 = T.indD S.dbar 1 * I1 := by funext ω rw [hFactor] rfl rw [harg] filter_upwards [hpull] with ω hω simpa [Pi.mul_apply] using hω have hbridge : (fun ω => S.stageOneReg ω * T.indD S.dbar 1 ω) =ᵐ[P.μ] (fun ω => T.innerReg S.dbar 0 ω * T.indD S.dbar 1 ω) := by have hover := hA.overlap S.dbar kLast filter_upwards [hNum_pull, hDen_pull, hover] with ω hN hD hov have hstage : S.stageOneReg ω = B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω / B.condExpGiven I1 P.μ ω := by rfl have hinner : T.innerReg S.dbar 0 ω = B.condExpGiven (fun ω => T.factualY ω * T.indD S.dbar 2 ω) P.μ ω / B.condExpGiven (T.indD S.dbar 2) P.μ ω := by unfold PODTRSystem.innerReg simp only [Nat.ofNat_pos, ↓reduceDIte] rfl rw [hstage, hinner, hN, hD] rcases T.indD_eq_zero_or_one S.dbar 1 ω with h0 | h1 · simp [h0] · have hne : B.condExpGiven I1 P.μ ω ≠ 0 := by intro hzero rw [hzero] at hov linarith rw [h1] field_simp [hne] have hbase := T.cdtr_base hA S.dbar (by decide : 0 < 2) exact hbridge.trans (by simpa [T, B] using hbase) -
μ₁_val_comp_mul_indD_eqlemma — Composed observable μ₁_val, multiplied by the partial regime indicator indD dbar 1, agrees with the corresponding counterfactual conditional expectation. This is the consumer-facing form of stageOneReg_indD_eq.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.Assumptionsconclusion(fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.toPODTRSystem.indD S.dbar 1 ω)=ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω)Proof (Lean source)
lemma μ₁_val_comp_mul_indD_eq (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : (fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.toPODTRSystem.indD S.dbar 1 ω) =ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω) := by filter_upwards [S.μ₁_val_comp_eq_stageOneReg, S.stageOneReg_indD_eq hA] with ω hμ hstage rw [hμ] exact hstage -
indD_mul_μ₁_val_comp_eqlemma — Same as μ₁_val_comp_mul_indD_eq, with the partial regime indicator written on the left.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.Assumptionsconclusion(fun ω => S.toPODTRSystem.indD S.dbar 1 ω * S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))=ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω)Proof (Lean source)
lemma indD_mul_μ₁_val_comp_eq (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) =ᵐ[P.μ] (fun ω => S.toPODTRSystem.indD S.dbar 1 ω * (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω) := by filter_upwards [S.μ₁_val_comp_mul_indD_eq hA] with ω hω simpa [mul_comm] using hω -
stageOneReg_memLplemma — The observable stage-1 regression is square-integrable under strict overlap and a factual second moment.hypothesesS :DTREstimationSystem P δ γε :ℝhov :S.StrictOverlap εh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μconclusionMemLp S.stageOneReg 2 P.μProof (Lean source)
lemma stageOneReg_memLp (S : DTREstimationSystem P δ γ) {ε : ℝ} (hov : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) : MemLp S.stageOneReg 2 P.μ := by let T := S.toPODTRSystem let kLast : Fin 2 := ⟨1, by decide⟩ let I1 : P.Ω → ℝ := (T.dVar kLast).indicator (S.dbar kLast) let B := T.historyBundle 1 (by decide) have hε_pos : 0 < ε := hov.1 have hY_L2 : MemLp T.factualY 2 P.μ := (memLp_two_iff_integrable_sq T.measurable_factualY.aestronglyMeasurable).2 h_y2 have hI1_meas : Measurable I1 := by simpa [T, I1, kLast] using (T.dVar kLast).measurable_indicator (S.dbar kLast) have hYI_L2 : MemLp (fun ω => T.factualY ω * I1 ω) 2 P.μ := by refine hY_L2.norm.mono' ((T.measurable_factualY.mul hI1_meas).aestronglyMeasurable) ?_ refine Filter.Eventually.of_forall (fun ω => ?_) rcases (T.dVar kLast).indicator_eq_one_or_zero (S.dbar kLast) ω with h0 | h1 · simp [I1, h0] · simp [I1, h1] have hNum_L2 : MemLp (B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ) 2 P.μ := by simpa [POCFBundle.condExpGiven] using hYI_L2.condExp have hbound : ∀ᵐ ω ∂P.μ, ‖S.stageOneReg ω‖ ≤ ε⁻¹ * ‖B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω‖ := by filter_upwards [hov.2.2] with ω hover have hden_ge : ε ≤ B.condExpGiven I1 P.μ ω := by simpa [T, B, I1, kLast] using hover.2.1 have hden_pos : 0 < B.condExpGiven I1 P.μ ω := lt_of_lt_of_le hε_pos hden_ge have hinv : (B.condExpGiven I1 P.μ ω)⁻¹ ≤ ε⁻¹ := by rw [inv_le_inv₀ hden_pos hε_pos] exact hden_ge unfold stageOneReg POCFBundle.condExpRatio simp only [T, B, I1, kLast] rw [Real.norm_eq_abs, abs_div, abs_of_pos hden_pos] calc |B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω| / B.condExpGiven I1 P.μ ω = (B.condExpGiven I1 P.μ ω)⁻¹ * |B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω| := by ring _ ≤ ε⁻¹ * |B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω| := by exact mul_le_mul_of_nonneg_right hinv (abs_nonneg _) _ = ε⁻¹ * ‖B.condExpGiven (fun ω => T.factualY ω * I1 ω) P.μ ω‖ := by rw [Real.norm_eq_abs] refine (hNum_L2.norm.const_mul ε⁻¹).mono' (B.stronglyMeasurable_condExpRatio (fun ω => T.factualY ω * I1 ω) I1).aestronglyMeasurable ?_ simpa [DTREstimationSystem.stageOneReg, T, B, I1, kLast] using hbound -
measurable_factualZlemma — The full observed two-stage data tuple is measurable.Proof (Lean source)
lemma measurable_factualZ (S : DTREstimationSystem P δ γ) : Measurable S.factualZ := by refine (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩).prodMk ?_ refine (S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prodMk ?_ refine (S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prodMk ?_ exact (S.toPODTRSystem.measurable_factualD ⟨1, by decide⟩).prodMk S.toPODTRSystem.measurable_factualY
SeqDRMoment 16 core · 12 supporting This file defines the explicit two-stage sequential AIPW moment for dynamic treatment regimes, its truth-level influence function, and the overlap-bounded nuisance space used by the abstract DML layer. ★ P_Z_map_projS₀_eq_P_H₀★ P_Z_map_histH₁_eq_P_H₁
Sequential DR Moment for Two-Stage Regimes
This file defines the explicit two-stage sequential AIPW moment for dynamic treatment regimes, its truth-level influence function, and the overlap-bounded nuisance space used by the abstract DML layer. The target is the fixed-regime mean for a two-period regime, and the score uses stagewise inverse-propensity weights centered by the target estimand.
The development is intentionally specialized to horizon two; the treatment space is discrete enough to support equality indicators. The stage-1 history is stored in cons order as the current state, previous treatment, and previous state.
def projS₀ reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the initial state from the observed two-stage data tuple.
Definition (Lean source)
def projS₀ : γ 0 × δ × γ 1 × δ × ℝ → γ 0 := fun z => z.1
def projD₀ reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the first treatment from the observed two-stage data tuple.
Definition (Lean source)
def projD₀ : γ 0 × δ × γ 1 × δ × ℝ → δ := fun z => z.2.1
def projS₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the second state from the observed two-stage data tuple.
Definition (Lean source)
def projS₁ : γ 0 × δ × γ 1 × δ × ℝ → γ 1 := fun z => z.2.2.1
def projD₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the second treatment from the observed two-stage data tuple.
Definition (Lean source)
def projD₁ : γ 0 × δ × γ 1 × δ × ℝ → δ := fun z => z.2.2.2.1
def projY reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the outcome from the observed two-stage data tuple.
Definition (Lean source)
def projY : γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun z => z.2.2.2.2
def histH₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
This projection returns the stage-1 history in the order used by the DTR history bundle.
def indEq reviewed
⚑ flagged
Causalean.Estimation.DTR
This function is the real-valued indicator that two discrete treatments are equal.
structure DTRNuisanceVec₂ reviewed
⚑ flagged
Causalean.Estimation.DTR
A stagewise nuisance vector for two-period dynamic-treatment-regime estimation: the baseline outcome regression and treatment propensity at the first stage, the second-stage outcome regression and treatment propensity given the second-period history, together with the measurability of all four nuisance functions.
Definition (Lean source)
parameters
fields
μ₀_fn :
γ 0 → ℝ
e₀_fn :
γ 0 → ℝ
μ₁_fn :
γ 1 × δ × γ 0 → ℝ
e₁_fn :
γ 1 × δ × γ 0 → ℝ
μ₀_meas :
Measurable μ₀_fn
e₀_meas :
Measurable e₀_fn
μ₁_meas :
Measurable μ₁_fn
e₁_meas :
Measurable e₁_fn
def seqDRMoment reviewed
⚑ flagged
Causalean.Estimation.DTR
This is the explicit two-stage sequential doubly robust moment for a fixed treatment regime.
Definition (Lean source)
noncomputable def seqDRMoment
(dbar : Fin 2 → δ) (z : γ 0 × δ × γ 1 × δ × ℝ)
(η : DTRNuisanceVec₂ δ γ) (θ : ℝ) : ℝ :=
η.μ₀_fn (projS₀ z)
+ (indEq (projD₀ z) (dbar 0) / η.e₀_fn (projS₀ z))
* (η.μ₁_fn (histH₁ z) - η.μ₀_fn (projS₀ z))
+ (indEq (projD₀ z) (dbar 0) * indEq (projD₁ z) (dbar 1) /
(η.e₀_fn (projS₀ z) * η.e₁_fn (histH₁ z)))
* (projY z - η.μ₁_fn (histH₁ z))
- θ
def η₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the true nuisance vector extracted from a two-stage DTR estimation system.
Definition (Lean source)
noncomputable def η₀ (S : DTREstimationSystem P δ γ) :
DTRNuisanceVec₂ δ γ :=
⟨S.μ₀_val, S.e₀_val, S.μ₁_val, S.e₁_val,
S.μ₀_meas, S.e₀_meas, S.μ₁_meas, S.e₁_meas⟩
def seqDRMoment reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the sequential doubly robust moment specialized to the system's target regime.
Definition (Lean source)
noncomputable def seqDRMoment (S : DTREstimationSystem P δ γ)
(z : γ 0 × δ × γ 1 × δ × ℝ) (η : DTRNuisanceVec₂ δ γ) (θ : ℝ) : ℝ :=
seqDRMoment S.dbar z η θ
def ψ_seqDR reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the sequential doubly robust influence function evaluated at the true nuisances and target.
Definition (Lean source)
noncomputable def ψ_seqDR (S : DTREstimationSystem P δ γ)
(z : γ 0 × δ × γ 1 × δ × ℝ) : ℝ :=
S.seqDRMoment z S.η₀ S.θ₀
def H_ε reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This set contains nuisance candidates whose two propensity components are uniformly overlap-bounded.
Definition (Lean source)
def H_ε (ε : ℝ) : Set (DTRNuisanceVec₂ δ γ) :=
{ η | (∀ s, ε ≤ η.e₀_fn s ∧ η.e₀_fn s ≤ 1 - ε)
∧ (∀ h, ε ≤ η.e₁_fn h ∧ η.e₁_fn h ≤ 1 - ε) }
def seqDRMomentFunctional reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
This is the sequential doubly robust moment packaged as a functional of nuisance, data, and target value.
Definition (Lean source)
noncomputable def seqDRMomentFunctional (S : DTREstimationSystem P δ γ) :
DTRNuisanceVec₂ δ γ → (γ 0 × δ × γ 1 × δ × ℝ) → ℝ → ℝ :=
fun η z θ => seqDRMoment S.dbar z η θ
lemma P_Z_map_projS₀_eq_P_H₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a dynamic-treatment-regime estimation system, pushing the full observed-data law forward through the initial-state projection yields exactly the stage-0 history marginal law.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
conclusion
S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z) = S.P_H₀
Proof (Lean source)
lemma P_Z_map_projS₀_eq_P_H₀ (S : DTREstimationSystem P δ γ) :
S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z) = S.P_H₀ := by
unfold DTREstimationSystem.P_Z DTREstimationSystem.P_H₀
rw [Measure.map_map measurable_projS₀ S.measurable_factualZ]; rfl
lemma P_Z_map_histH₁_eq_P_H₁ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a dynamic-treatment-regime estimation system, pushing the full observed-data law forward through the stage-1 history projection yields exactly the stage-1 history marginal law.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
conclusion
S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z) = S.P_H₁
Proof (Lean source)
lemma P_Z_map_histH₁_eq_P_H₁ (S : DTREstimationSystem P δ γ) :
S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z) = S.P_H₁ := by
unfold DTREstimationSystem.P_Z DTREstimationSystem.P_H₁
rw [Measure.map_map measurable_histH₁ S.measurable_factualZ]; rfl
12 supporting declarations (lemmas, instances)
-
instZeroinstance — The zero nuisance vector sets every stagewise regression and propensity component to zero.instance : Zero (DTRNuisanceVec₂ δ γ) where zero := ⟨fun _ => 0, fun _ => 0, fun _ => 0, fun _ => 0, measurable_const, measurable_const, measurable_const, measurable_const⟩ -
instAddinstance — Addition of nuisance vectors is performed component by component.instance : Add (DTRNuisanceVec₂ δ γ) where add η η' := ⟨fun s => η.μ₀_fn s + η'.μ₀_fn s, fun s => η.e₀_fn s + η'.e₀_fn s, fun h => η.μ₁_fn h + η'.μ₁_fn h, fun h => η.e₁_fn h + η'.e₁_fn h, η.μ₀_meas.add η'.μ₀_meas, η.e₀_meas.add η'.e₀_meas, η.μ₁_meas.add η'.μ₁_meas, η.e₁_meas.add η'.e₁_meas⟩ -
instNeginstance — Negation of a nuisance vector is performed component by component.instance : Neg (DTRNuisanceVec₂ δ γ) where neg η := ⟨fun s => -η.μ₀_fn s, fun s => -η.e₀_fn s, fun h => -η.μ₁_fn h, fun h => -η.e₁_fn h, η.μ₀_meas.neg, η.e₀_meas.neg, η.μ₁_meas.neg, η.e₁_meas.neg⟩ -
instSubinstance — Subtraction of nuisance vectors is performed component by component.instance : Sub (DTRNuisanceVec₂ δ γ) where sub η η' := ⟨fun s => η.μ₀_fn s - η'.μ₀_fn s, fun s => η.e₀_fn s - η'.e₀_fn s, fun h => η.μ₁_fn h - η'.μ₁_fn h, fun h => η.e₁_fn h - η'.e₁_fn h, η.μ₀_meas.sub η'.μ₀_meas, η.e₀_meas.sub η'.e₀_meas, η.μ₁_meas.sub η'.μ₁_meas, η.e₁_meas.sub η'.e₁_meas⟩ -
instSMulRealinstance — Real scalar multiplication of a nuisance vector is performed component by component.instance : SMul ℝ (DTRNuisanceVec₂ δ γ) where smul t η := ⟨fun s => t * η.μ₀_fn s, fun s => t * η.e₀_fn s, fun h => t * η.μ₁_fn h, fun h => t * η.e₁_fn h, measurable_const.mul η.μ₀_meas, measurable_const.mul η.e₀_meas, measurable_const.mul η.μ₁_meas, measurable_const.mul η.e₁_meas⟩ -
exttheorem — Two nuisance vectors are equal when all four stagewise components agree pointwise.hypothesesη η' :DTRNuisanceVec₂ δ γh0μ :∀ s, η.μ₀_fn s = η'.μ₀_fn sh0e :∀ s, η.e₀_fn s = η'.e₀_fn sh1μ :∀ h, η.μ₁_fn h = η'.μ₁_fn hh1e :∀ h, η.e₁_fn h = η'.e₁_fn hconclusionη = η'Proof (Lean source)
@[ext] theorem ext {η η' : DTRNuisanceVec₂ δ γ} (h0μ : ∀ s, η.μ₀_fn s = η'.μ₀_fn s) (h0e : ∀ s, η.e₀_fn s = η'.e₀_fn s) (h1μ : ∀ h, η.μ₁_fn h = η'.μ₁_fn h) (h1e : ∀ h, η.e₁_fn h = η'.e₁_fn h) : η = η' := by cases η cases η' simp only at h0μ h0e h1μ h1e congr · funext s; exact h0μ s · funext s; exact h0e s · funext h; exact h1μ h · funext h; exact h1e h -
ext_ifftheorem∀ {δ : Type} [inst : MeasurableSpace δ] [inst_1 : MeasurableSingletonClass δ] {γ : Fin 2 → Type} [inst_2 : (k : Fin 2) → MeasurableSpace (γ k)] {η η' : DTRNuisanceVec₂ δ γ}, η = η' ↔ (∀ (s : γ 0), η.μ₀_fn s = η'.μ₀_fn s) ∧ (∀ (s : γ 0), η.e₀_fn s = η'.e₀_fn s) ∧ (∀ (h : γ 1 × δ × γ 0), η.μ₁_fn h = η'.μ₁_fn h) ∧ ∀ (h : γ 1 × δ × γ 0), η.e₁_fn h = η'.e₁_fn hProof (Lean source)
@[ext] -
instAddCommGroupinstance — The nuisance vectors form an additive commutative group under componentwise operations.instance : AddCommGroup (DTRNuisanceVec₂ δ γ) where zero := 0 add := (· + ·) neg := neg sub := Sub.sub nsmul := nsmulRec zsmul := zsmulRec nsmul_zero η := by rfl nsmul_succ n η := by rfl zsmul_zero' η := by rfl zsmul_succ' n η := by rfl zsmul_neg' n η := by rfl sub_eq_add_neg η η' := by apply ext · intro s; exact sub_eq_add_neg (η.μ₀_fn s) (η'.μ₀_fn s) · intro s; exact sub_eq_add_neg (η.e₀_fn s) (η'.e₀_fn s) · intro h; exact sub_eq_add_neg (η.μ₁_fn h) (η'.μ₁_fn h) · intro h; exact sub_eq_add_neg (η.e₁_fn h) (η'.e₁_fn h) add_assoc η η' η'' := by apply ext · intro s; exact add_assoc (η.μ₀_fn s) (η'.μ₀_fn s) (η''.μ₀_fn s) · intro s; exact add_assoc (η.e₀_fn s) (η'.e₀_fn s) (η''.e₀_fn s) · intro h; exact add_assoc (η.μ₁_fn h) (η'.μ₁_fn h) (η''.μ₁_fn h) · intro h; exact add_assoc (η.e₁_fn h) (η'.e₁_fn h) (η''.e₁_fn h) zero_add η := by apply ext · intro s; exact zero_add (η.μ₀_fn s) · intro s; exact zero_add (η.e₀_fn s) · intro h; exact zero_add (η.μ₁_fn h) · intro h; exact zero_add (η.e₁_fn h) add_zero η := by apply ext · intro s; exact add_zero (η.μ₀_fn s) · intro s; exact add_zero (η.e₀_fn s) · intro h; exact add_zero (η.μ₁_fn h) · intro h; exact add_zero (η.e₁_fn h) neg_add_cancel η := by apply ext · intro s; exact neg_add_cancel (η.μ₀_fn s) · intro s; exact neg_add_cancel (η.e₀_fn s) · intro h; exact neg_add_cancel (η.μ₁_fn h) · intro h; exact neg_add_cancel (η.e₁_fn h) add_comm η η' := by apply ext · intro s; exact add_comm (η.μ₀_fn s) (η'.μ₀_fn s) · intro s; exact add_comm (η.e₀_fn s) (η'.e₀_fn s) · intro h; exact add_comm (η.μ₁_fn h) (η'.μ₁_fn h) · intro h; exact add_comm (η.e₁_fn h) (η'.e₁_fn h) -
instModuleRealinstance — The nuisance vectors form a real module under componentwise scalar multiplication.instance : Module ℝ (DTRNuisanceVec₂ δ γ) where smul := (· • ·) one_smul η := by apply ext · intro s; change (1 : ℝ) * η.μ₀_fn s = η.μ₀_fn s; exact one_mul _ · intro s; change (1 : ℝ) * η.e₀_fn s = η.e₀_fn s; exact one_mul _ · intro h; change (1 : ℝ) * η.μ₁_fn h = η.μ₁_fn h; exact one_mul _ · intro h; change (1 : ℝ) * η.e₁_fn h = η.e₁_fn h; exact one_mul _ mul_smul t u η := by apply ext · intro s; change (t * u) * η.μ₀_fn s = t * (u * η.μ₀_fn s); ring · intro s; change (t * u) * η.e₀_fn s = t * (u * η.e₀_fn s); ring · intro h; change (t * u) * η.μ₁_fn h = t * (u * η.μ₁_fn h); ring · intro h; change (t * u) * η.e₁_fn h = t * (u * η.e₁_fn h); ring smul_zero t := by apply ext · intro s; change t * (0 : ℝ) = 0; exact mul_zero t · intro s; change t * (0 : ℝ) = 0; exact mul_zero t · intro h; change t * (0 : ℝ) = 0; exact mul_zero t · intro h; change t * (0 : ℝ) = 0; exact mul_zero t smul_add t η η' := by apply ext · intro s change t * (η.μ₀_fn s + η'.μ₀_fn s) = t * η.μ₀_fn s + t * η'.μ₀_fn s ring · intro s change t * (η.e₀_fn s + η'.e₀_fn s) = t * η.e₀_fn s + t * η'.e₀_fn s ring · intro h change t * (η.μ₁_fn h + η'.μ₁_fn h) = t * η.μ₁_fn h + t * η'.μ₁_fn h ring · intro h change t * (η.e₁_fn h + η'.e₁_fn h) = t * η.e₁_fn h + t * η'.e₁_fn h ring add_smul t u η := by apply ext · intro s change (t + u) * η.μ₀_fn s = t * η.μ₀_fn s + u * η.μ₀_fn s ring · intro s change (t + u) * η.e₀_fn s = t * η.e₀_fn s + u * η.e₀_fn s ring · intro h change (t + u) * η.μ₁_fn h = t * η.μ₁_fn h + u * η.μ₁_fn h ring · intro h change (t + u) * η.e₁_fn h = t * η.e₁_fn h + u * η.e₁_fn h ring zero_smul η := by apply ext · intro s; change (0 : ℝ) * η.μ₀_fn s = 0; exact zero_mul _ · intro s; change (0 : ℝ) * η.e₀_fn s = 0; exact zero_mul _ · intro h; change (0 : ℝ) * η.μ₁_fn h = 0; exact zero_mul _ · intro h; change (0 : ℝ) * η.e₁_fn h = 0; exact zero_mul _ -
measurable_seqDRMomentFunctionallemma — The sequential doubly robust moment functional is measurable as a function of the observed data tuple.hypothesesconclusionMeasurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => S.seqDRMomentFunctional η z θ)Proof (Lean source)
lemma measurable_seqDRMomentFunctional (S : DTREstimationSystem P δ γ) (η : DTRNuisanceVec₂ δ γ) (θ : ℝ) : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => S.seqDRMomentFunctional η z θ) := by unfold DTREstimationSystem.seqDRMomentFunctional unfold Causalean.Estimation.DTR.seqDRMoment have hs0 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z) := by unfold projS₀ exact measurable_fst have hd0 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projD₀ z) := by unfold projD₀ measurability have hd1 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projD₁ z) := by unfold projD₁ measurability have hy : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projY z) := by unfold projY measurability have hh1 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z) := by unfold histH₁ projS₁ projD₀ projS₀ measurability have hμ0 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => η.μ₀_fn (projS₀ z)) := η.μ₀_meas.comp hs0 have he0 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => η.e₀_fn (projS₀ z)) := η.e₀_meas.comp hs0 have hμ1 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => η.μ₁_fn (histH₁ z)) := η.μ₁_meas.comp hh1 have he1 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => η.e₁_fn (histH₁ z)) := η.e₁_meas.comp hh1 have hind0 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => indEq (projD₀ z) (S.dbar 0)) := by have hset : MeasurableSet {z : γ 0 × δ × γ 1 × δ × ℝ | projD₀ z = S.dbar 0} := (MeasurableSet.singleton (S.dbar 0)).preimage hd0 have hfun : (fun z : γ 0 × δ × γ 1 × δ × ℝ => indEq (projD₀ z) (S.dbar 0)) = indicator {z : γ 0 × δ × γ 1 × δ × ℝ | projD₀ z = S.dbar 0} (fun _ => (1 : ℝ)) := by funext z by_cases hz : projD₀ z = S.dbar 0 <;> simp [indEq, hz] rw [hfun] exact measurable_const.indicator hset have hind1 : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => indEq (projD₁ z) (S.dbar 1)) := by have hset : MeasurableSet {z : γ 0 × δ × γ 1 × δ × ℝ | projD₁ z = S.dbar 1} := (MeasurableSet.singleton (S.dbar 1)).preimage hd1 have hfun : (fun z : γ 0 × δ × γ 1 × δ × ℝ => indEq (projD₁ z) (S.dbar 1)) = indicator {z : γ 0 × δ × γ 1 × δ × ℝ | projD₁ z = S.dbar 1} (fun _ => (1 : ℝ)) := by funext z by_cases hz : projD₁ z = S.dbar 1 <;> simp [indEq, hz] rw [hfun] exact measurable_const.indicator hset exact ((hμ0.add ((hind0.div he0).mul (hμ1.sub hμ0))).add (((hind0.mul hind1).div (he0.mul he1)).mul (hy.sub hμ1))).sub measurable_const -
measurable_projS₀lemma — The initial-state projection is measurable.conclusionMeasurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z)Proof (Lean source)
lemma measurable_projS₀ : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z) := by unfold projS₀; exact measurable_fst -
measurable_histH₁lemma — The cons-ordered stage-1 history projection is measurable.conclusionMeasurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z)
Constructor 3 core · 0 supporting Constructs value-space lifts for explicit two-stage dynamic-treatment-regime histories. ★ exists_stage0_lift★ exists_stage1_lift
Constructs value-space lifts for explicit two-stage dynamic-treatment-regime histories. The module turns stagewise histories, actions, and outcome regressions into the representatives consumed by sequential doubly robust scores.
lemma exists_stage0_lift reviewed
⚑ flagged
Causalean.Estimation.DTR
Doob–Dynkin factorization through the stage-0 state. Consider a two-stage dynamic-treatment-regime potential-outcome system and a real-valued function g on the sample space. If g is measurable with respect to the σ-algebra generated by the stage-0 history — here just the initial state S₀, then g factors through the stage-0 state: there is a measurable function f on the stage-0 state space such that g equals f composed with the stage-0 state map.
Formal statement
hypotheses
conclusion
∃ f : γ 0 → ℝ, Measurable f ∧ g = fun ω => f (S.factualS ⟨0, by decide⟩ ω)
Proof (Lean source)
lemma exists_stage0_lift (S : PODTRSystem P 2 δ γ) (g : P.Ω → ℝ)
(hg : Measurable[(S.historyBundle 0 (by decide)).sigma] g) :
∃ f : γ 0 → ℝ, Measurable f ∧
g = fun ω => f (S.factualS ⟨0, by decide⟩ ω) := by
let t : P.Ω → γ 0 := S.factualS ⟨0, by decide⟩
let B := S.historyBundle 0 (by decide)
let mT : MeasurableSpace P.Ω := MeasurableSpace.comap t inferInstance
have ht : @Measurable P.Ω (γ 0) mT inferInstance t :=
Measurable.of_comap_le (le_refl _)
have hBmeas :
@Measurable P.Ω (∀ i : Fin B.n, B.type i) mT inferInstance B.jointValue := by
apply measurable_pi_lambda
intro i
dsimp [B, t, PODTRSystem.historyBundle, POCFBundle.jointValue, POCFBundle.cons,
POCFBundle.nil, RegimedVar.ofFactual, RegimedVar.value, PODTRSystem.factualS]
fin_cases i
exact ht
have hsub : B.sigma ≤ mT := hBmeas.comap_le
have hmeas : @Measurable P.Ω ℝ mT inferInstance g := hg.mono hsub (le_refl _)
obtain ⟨f, hf, hfg⟩ :=
Measurable.exists_eq_measurable_comp (f := t) (g := g) hmeas
exact ⟨f, hf, by funext ω; exact congrFun hfg ω⟩
lemma exists_stage1_lift reviewed
⚑ flagged
Causalean.Estimation.DTR
Doob–Dynkin factorization through the stage-1 history. Consider a two-stage dynamic-treatment-regime potential-outcome system and a real-valued function g on the sample space. If g is measurable with respect to the σ-algebra generated by the stage-1 history — the current state, the previous treatment, and the previous state, then g factors through that history tuple: there is a measurable function f on the stage-1 history space such that g equals f composed with the map recording the current state, the previous treatment, and the previous state.
Formal statement
hypotheses
conclusion
∃ f : γ 1 × δ × γ 0 → ℝ,
Measurable f ∧
g
= fun ω => f (S.factualS ⟨1, by decide⟩ ω, S.factualD ⟨0, by decide⟩ ω, S.factualS ⟨0, by decide⟩ ω)
Proof (Lean source)
lemma exists_stage1_lift (S : PODTRSystem P 2 δ γ) (g : P.Ω → ℝ)
(hg : Measurable[(S.historyBundle 1 (by decide)).sigma] g) :
∃ f : γ 1 × δ × γ 0 → ℝ, Measurable f ∧
g = fun ω => f
(S.factualS ⟨1, by decide⟩ ω,
S.factualD ⟨0, by decide⟩ ω,
S.factualS ⟨0, by decide⟩ ω) := by
let t : P.Ω → γ 1 × δ × γ 0 := fun ω =>
(S.factualS ⟨1, by decide⟩ ω,
S.factualD ⟨0, by decide⟩ ω,
S.factualS ⟨0, by decide⟩ ω)
let B := S.historyBundle 1 (by decide)
let mT : MeasurableSpace P.Ω := MeasurableSpace.comap t inferInstance
have ht : @Measurable P.Ω (γ 1 × δ × γ 0) mT inferInstance t :=
Measurable.of_comap_le (le_refl _)
have hS1 : @Measurable P.Ω (γ 1) mT inferInstance
(S.factualS ⟨1, by decide⟩) := by
change @Measurable P.Ω (γ 1) mT inferInstance (fun ω => (t ω).1)
exact measurable_fst.comp ht
have hD0 : @Measurable P.Ω δ mT inferInstance
(S.factualD ⟨0, by decide⟩) := by
change @Measurable P.Ω δ mT inferInstance (fun ω => (t ω).2.1)
exact measurable_fst.comp (measurable_snd.comp ht)
have hS0 : @Measurable P.Ω (γ 0) mT inferInstance
(S.factualS ⟨0, by decide⟩) := by
change @Measurable P.Ω (γ 0) mT inferInstance (fun ω => (t ω).2.2)
exact measurable_snd.comp (measurable_snd.comp ht)
have hBmeas :
@Measurable P.Ω (∀ i : Fin B.n, B.type i) mT inferInstance B.jointValue := by
apply measurable_pi_lambda
intro i
dsimp [B, t, PODTRSystem.historyBundle, POCFBundle.jointValue, POCFBundle.cons,
POCFBundle.nil, RegimedVar.ofFactual, RegimedVar.value, PODTRSystem.factualS,
PODTRSystem.factualD, PODTRSystem.dVar]
fin_cases i
· exact hS1
· exact hD0
· exact hS0
have hsub : B.sigma ≤ mT := hBmeas.comap_le
have hmeas : @Measurable P.Ω ℝ mT inferInstance g := hg.mono hsub (le_refl _)
obtain ⟨f, hf, hfg⟩ :=
Measurable.exists_eq_measurable_comp (f := t) (g := g) hmeas
exact ⟨f, hf, by funext ω; exact congrFun hfg ω⟩
def toDTREstimationSystem reviewed
⚑ flagged
Causalean.PO.PODTRSystem
The DTR estimation-system fields are free given two-stage overlap. From a bare PODTRSystem P 2 δ γ, a fixed target regime dbar, and a.e. overlap at stages 0 and 1, construct a DTREstimationSystem. The regression fields are Doob--Dynkin lifts of the observable nested regressions, and the propensity fields are the corresponding lifts clamped into (0, 1) off support.
Definition (Lean source)
noncomputable def _root_.Causalean.PO.PODTRSystem.toDTREstimationSystem
(S : PODTRSystem P 2 δ γ) (dbar : Fin 2 → δ)
(hov0 : ∀ᵐ ω ∂P.μ,
0 < (S.historyBundle 0 (by decide)).condExpGiven
((S.dVar ⟨0, by decide⟩).indicator (dbar ⟨0, by decide⟩)) P.μ ω ∧
(S.historyBundle 0 (by decide)).condExpGiven
((S.dVar ⟨0, by decide⟩).indicator (dbar ⟨0, by decide⟩)) P.μ ω < 1)
(hov1 : ∀ᵐ ω ∂P.μ,
0 < (S.historyBundle 1 (by decide)).condExpGiven
((S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩)) P.μ ω ∧
(S.historyBundle 1 (by decide)).condExpGiven
((S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩)) P.μ ω < 1) :
DTREstimationSystem P δ γ := by
let e0prop : P.Ω → ℝ :=
(S.historyBundle 0 (by decide)).condExpGiven
((S.dVar ⟨0, by decide⟩).indicator (dbar ⟨0, by decide⟩)) P.μ
let e1prop : P.Ω → ℝ :=
(S.historyBundle 1 (by decide)).condExpGiven
((S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩)) P.μ
let f₂ : P.Ω → ℝ :=
(S.historyBundle 1 (by decide)).condExpRatio
(fun ω => S.factualY ω *
(S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩) ω)
((S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩)) P.μ
let innerReg : P.Ω → ℝ := S.innerReg dbar 1
let B0 := S.historyBundle 0 (by decide)
let B1 := S.historyBundle 1 (by decide)
have hinner_meas : Measurable[B0.sigma] innerReg := by
unfold innerReg
unfold PODTRSystem.innerReg
simp only [Nat.reduceAdd, Nat.reduceLT, ↓reduceDIte, Nat.reduceSub]
let stage : Fin 2 := ⟨0, by decide⟩
let ind_k : P.Ω → ℝ := (S.dVar stage).indicator (dbar stage)
have hN : Measurable[B0.sigma]
(B0.condExpGiven (fun ω' => S.innerReg dbar 0 ω' * ind_k ω') P.μ) :=
(B0.stronglyMeasurable_condExpGiven_comap
(fun ω' => S.innerReg dbar 0 ω' * ind_k ω')).measurable
have hD : Measurable[B0.sigma] (B0.condExpGiven ind_k P.μ) :=
(B0.stronglyMeasurable_condExpGiven_comap ind_k).measurable
exact hN.div hD
have he0_meas : Measurable[B0.sigma] e0prop :=
(B0.stronglyMeasurable_condExpGiven_comap
((S.dVar ⟨0, by decide⟩).indicator (dbar ⟨0, by decide⟩))).measurable
have hf₂_meas : Measurable[B1.sigma] f₂ := by
let yInd : P.Ω → ℝ := fun ω => S.factualY ω *
(S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩) ω
let ind : P.Ω → ℝ :=
(S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩)
have hN : Measurable[B1.sigma] (B1.condExpGiven yInd P.μ) :=
(B1.stronglyMeasurable_condExpGiven_comap yInd).measurable
have hD : Measurable[B1.sigma] (B1.condExpGiven ind P.μ) :=
(B1.stronglyMeasurable_condExpGiven_comap ind).measurable
unfold f₂ POCFBundle.condExpRatio
exact hN.div hD
have he1_meas : Measurable[B1.sigma] e1prop :=
(B1.stronglyMeasurable_condExpGiven_comap
((S.dVar ⟨1, by decide⟩).indicator (dbar ⟨1, by decide⟩))).measurable
let μ0Lift := exists_stage0_lift S innerReg hinner_meas
let e0Lift := exists_stage0_lift S e0prop he0_meas
let μ1Lift := exists_stage1_lift S f₂ hf₂_meas
let e1Lift := exists_stage1_lift S e1prop he1_meas
exact
{ toPODTRSystem := S
dbar := dbar
μ₀_val := μ0Lift.choose
μ₀_meas := μ0Lift.choose_spec.1
e₀_val :=
Set.piecewise {x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1}
e0Lift.choose (fun _ => 1 / 2)
e₀_meas := by
refine Measurable.piecewise ?_ e0Lift.choose_spec.1 measurable_const
exact (measurableSet_lt measurable_const e0Lift.choose_spec.1).inter
(measurableSet_lt e0Lift.choose_spec.1 measurable_const)
e₀_pos := by
intro x
by_cases hx : x ∈ {x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.1
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
e₀_lt_one := by
intro x
by_cases hx : x ∈ {x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.2
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
μ₁_val := μ1Lift.choose
μ₁_meas := μ1Lift.choose_spec.1
e₁_val :=
Set.piecewise {x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1}
e1Lift.choose (fun _ => 1 / 2)
e₁_meas := by
refine Measurable.piecewise ?_ e1Lift.choose_spec.1 measurable_const
exact (measurableSet_lt measurable_const e1Lift.choose_spec.1).inter
(measurableSet_lt e1Lift.choose_spec.1 measurable_const)
e₁_pos := by
intro x
by_cases hx : x ∈
{x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.1
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
e₁_lt_one := by
intro x
by_cases hx : x ∈
{x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1}
· rw [Set.piecewise_eq_of_mem _ _ _ hx]; exact hx.2
· rw [Set.piecewise_eq_of_notMem _ _ _ hx]; norm_num
μ₀_reg_compat := Filter.EventuallyEq.of_eq μ0Lift.choose_spec.2.symm
e₀_compat := by
filter_upwards [hov0] with ω hω
have heq : e0prop ω = e0Lift.choose (S.factualS (0 : Fin 2) ω) := by
simpa using congrFun e0Lift.choose_spec.2 ω
have hmem :
S.factualS (0 : Fin 2) ω ∈
{x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1} := by
have hω' : 0 < e0prop ω ∧ e0prop ω < 1 := by
simpa [e0prop] using hω
change 0 < e0Lift.choose (S.factualS (0 : Fin 2) ω) ∧
e0Lift.choose (S.factualS (0 : Fin 2) ω) < 1
rw [← heq]
exact hω'
change e0prop ω =
Set.piecewise {x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1}
e0Lift.choose (fun _ => 1 / 2) (S.factualS (0 : Fin 2) ω)
rw [heq]
exact (Set.piecewise_eq_of_mem
{x : γ 0 | 0 < e0Lift.choose x ∧ e0Lift.choose x < 1}
e0Lift.choose (fun _ => 1 / 2) hmem).symm
μ₁_reg_compat := Filter.EventuallyEq.of_eq μ1Lift.choose_spec.2.symm
e₁_compat := by
filter_upwards [hov1] with ω hω
have heq : e1prop ω = e1Lift.choose
(S.factualS (1 : Fin 2) ω,
S.factualD (0 : Fin 2) ω,
S.factualS (0 : Fin 2) ω) := by
simpa using congrFun e1Lift.choose_spec.2 ω
have hmem :
(S.factualS (1 : Fin 2) ω,
S.factualD (0 : Fin 2) ω,
S.factualS (0 : Fin 2) ω) ∈
{x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1} := by
have hω' : 0 < e1prop ω ∧ e1prop ω < 1 := by
simpa [e1prop] using hω
change 0 < e1Lift.choose
(S.factualS (1 : Fin 2) ω,
S.factualD (0 : Fin 2) ω,
S.factualS (0 : Fin 2) ω) ∧
e1Lift.choose
(S.factualS (1 : Fin 2) ω,
S.factualD (0 : Fin 2) ω,
S.factualS (0 : Fin 2) ω) < 1
rw [← heq]
exact hω'
change e1prop ω =
Set.piecewise
{x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1}
e1Lift.choose (fun _ => 1 / 2)
(S.factualS (1 : Fin 2) ω,
S.factualD (0 : Fin 2) ω,
S.factualS (0 : Fin 2) ω)
rw [heq]
exact (Set.piecewise_eq_of_mem
{x : γ 1 × δ × γ 0 | 0 < e1Lift.choose x ∧ e1Lift.choose x < 1}
e1Lift.choose (fun _ => 1 / 2) hmem).symm }
DML 2 core · 0 supporting This file defines the one-shot double machine learning estimator for the two-period dynamic-treatment-regime effect. ★ dml_DTR_isAsymLinear
Dynamic-Treatment-Regime DML Estimator
This file defines the one-shot double machine learning estimator for the
two-period dynamic-treatment-regime effect. The main declarations are
dml_DTR_estimator, the fold-B empirical mean of the sequential doubly robust
pseudo-outcome, and dml_DTR_isAsymLinear, which proves asymptotic linearity
from stagewise nuisance overlap, measurability, L2 integrability, individual
o_p(1) rates, and the four cross-product o_p(n^{-1/2}) rates.
def dml_DTR_estimator reviewed
⚑ flagged
Causalean.Estimation.DTR
One-shot DML / sequential DR estimator of the DTR effect (def:est-dml-dtr).
Definition (Lean source)
noncomputable def dml_DTR_estimator
(S : DTREstimationSystem P δ γ)
(sample : IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
(η_hat : ℕ → P.Ω → DTRNuisanceVec₂ δ γ)
(n : ℕ) : P.Ω → ℝ :=
fun ω =>
((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n,
seqDRMoment S.dbar (sample.Z i ω) (η_hat n ω) 0
theorem dml_DTR_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.DTR
Asymptotic linearity of the one-shot DML DTR (n = 2) estimator — thm:est-dml-dtr-al. Assuming the DTR backdoor identification conditions hold, the theorem shows that the one-shot double/debiased-machine-learning estimator of the two-period dynamic-treatment-regime effect is asymptotically linear, with influence function ψ_seqDR, around the true effect θ₀. The population-truth propensities obey strict overlap — some ε ∈ (0, 1/2] sandwiches them a.s. at both stages, restated pointwise on the value-space propensity functions e₀_val, e₁_val; the factual outcome and every counterfactual outcome under a fixed regime are square-integrable; and the one-shot sample split's auxiliary-fold fraction |B(n)|/n converges to some c ∈ (0, 1). For every horizon n, the stage-0 nuisance learners μ̂₀, ê₀ and the stage-1 learners μ̂₁, ê₁ are each jointly measurable in the sample outcome and the covariate history at stage 0 and likewise at stage 1; the fitted propensities satisfy the same strict-overlap bound ε pointwise at both stages; each learner lies in L² of the covariate-history distribution at stage 0 and likewise at stage 1; and, viewed as a function of the sample outcome alone, each learner is measurable with respect to the auxiliary training fold's σ-algebra at stage 0 and likewise at stage 1, and jointly with the covariate in uncurried form at stage 0 and at stage 1. Finally, each stagewise estimation error converges to zero in L² at rate o_p(1), and every cross-stage product of an outcome-regression error with a propensity error vanishes at the doubly-robust rate o_p(n^{-1/2}).
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
hA :
S.toPODTRSystem.Assumptions
h_overlap :
S.StrictOverlap ε
h_e_val_pointwise :
(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ
sample :
IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
hc_lt :
c < 1
Stagewise nuisance hats.
μ₀_hat :
ℕ → P.Ω → (γ 0 → ℝ)
e₀_hat :
ℕ → P.Ω → (γ 0 → ℝ)
μ₁_hat :
ℕ → P.Ω → (γ 1 × δ × γ 0 → ℝ)
e₁_hat :
ℕ → P.Ω → (γ 1 × δ × γ 0 → ℝ)
Joint measurability (`(ω, x) ↦ hat(n, ω, x)`) for each stage.
h_mu0_meas :
∀ n, Measurable (fun (p : P.Ω × γ 0) => μ₀_hat n p.1 p.2)
h_e0_meas :
∀ n, Measurable (fun (p : P.Ω × γ 0) => e₀_hat n p.1 p.2)
h_mu1_meas :
∀ n, Measurable (fun (p : P.Ω × (γ 1 × δ × γ 0)) => μ₁_hat n p.1 p.2)
h_e1_meas :
∀ n, Measurable (fun (p : P.Ω × (γ 1 × δ × γ 0)) => e₁_hat n p.1 p.2)
Pointwise overlap of the estimator on `H_ε` at both stages.
h_e_overlap_hat :
∀ n ω,
(∀ s₀, ε ≤ e₀_hat n ω s₀ ∧ e₀_hat n ω s₀ ≤ 1 - ε) ∧
(∀ h, ε ≤ e₁_hat n ω h ∧ e₁_hat n ω h ≤ 1 - ε)
Per-`(n, ω)` `MemLp` hypotheses on each hat.
h_mu0_memLp :
∀ n ω, MemLp (fun s₀ => μ₀_hat n ω s₀) 2 S.P_H₀
h_e0_memLp :
∀ n ω, MemLp (fun s₀ => e₀_hat n ω s₀) 2 S.P_H₀
h_mu1_memLp :
∀ n ω, MemLp (fun h => μ₁_hat n ω h) 2 S.P_H₁
h_e1_memLp :
∀ n ω, MemLp (fun h => e₁_hat n ω h) 2 S.P_H₁
Fold-A measurability witnesses (per stage).
h_mu0_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ₀_hat n)
h_e0_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (e₀_hat n)
h_mu1_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (μ₁_hat n)
h_e1_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (e₁_hat n)
Joint fold-A measurability on the uncurried form (per stage).
h_mu0_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ 0))] (fun (p : P.Ω × γ 0) => μ₀_hat n p.1 p.2)
h_e0_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ 0))] (fun (p : P.Ω × γ 0) => e₀_hat n p.1 p.2)
h_mu1_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ 1 × δ × γ 0))] (fun (p : P.Ω × (γ 1 × δ × γ 0)) => μ₁_hat n p.1 p.2)
h_e1_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ 1 × δ × γ 0))] (fun (p : P.Ω × (γ 1 × δ × γ 0)) => e₁_hat n p.1 p.2)
Stagewise individual `o_p(1)` rates on `‖Δ·‖_{L²(P_H_k)}`.
h_mu0_rate :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal) (fun _ => (1 : ℝ)) P.μ
h_mu1_rate :
IsLittleOp (fun n ω => (eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal) (fun _ => (1 : ℝ)) P.μ
h_e0_rate :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) (fun _ => (1 : ℝ)) P.μ
h_e1_rate :
IsLittleOp (fun n ω => (eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal) (fun _ => (1 : ℝ)) P.μ
Cross-stage product rates: every `(μ_a, e_b)` pair is `o_p(n^{-1/2})`.
h_product_rate_00 :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal * (eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_11 :
IsLittleOp (fun n ω => (eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal * (eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_01 :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal * (eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_10 :
IsLittleOp (fun n ω => (eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal * (eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
conclusion
IsAsymLinear (dml_DTR_estimator S sample split (fun n ω => { μ₀_fn := μ₀_hat n ω e₀_fn := e₀_hat n ω μ₁_fn := μ₁_hat n ω e₁_fn := e₁_hat n ω μ₀_meas := (h_mu0_meas n).comp (prodMk measurable_const measurable_id) e₀_meas := (h_e0_meas n).comp (prodMk measurable_const measurable_id) μ₁_meas := (h_mu1_meas n).comp (prodMk measurable_const measurable_id) e₁_meas := (h_e1_meas n).comp (prodMk measurable_const measurable_id) })) S.θ₀ S.ψ_seqDR sample split.foldB
Proof (Lean source)
theorem dml_DTR_isAsymLinear
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(hA : S.toPODTRSystem.Assumptions)
(h_overlap : S.StrictOverlap ε)
(h_e_val_pointwise :
(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε)
∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε))
(h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ)
(h_yd2 : ∀ dbar : Fin 2 → δ,
Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ)
(sample : IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
{c : ℝ} (hc_pos : 0 < c) (hc_lt : c < 1)
(h_split_rate :
Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c))
-- Stagewise nuisance hats.
(μ₀_hat : ℕ → P.Ω → (γ 0 → ℝ))
(e₀_hat : ℕ → P.Ω → (γ 0 → ℝ))
(μ₁_hat : ℕ → P.Ω → (γ 1 × δ × γ 0 → ℝ))
(e₁_hat : ℕ → P.Ω → (γ 1 × δ × γ 0 → ℝ))
-- Joint measurability (`(ω, x) ↦ hat(n, ω, x)`) for each stage.
(h_mu0_meas :
∀ n, Measurable (fun (p : P.Ω × γ 0) => μ₀_hat n p.1 p.2))
(h_e0_meas :
∀ n, Measurable (fun (p : P.Ω × γ 0) => e₀_hat n p.1 p.2))
(h_mu1_meas :
∀ n, Measurable (fun (p : P.Ω × (γ 1 × δ × γ 0)) => μ₁_hat n p.1 p.2))
(h_e1_meas :
∀ n, Measurable (fun (p : P.Ω × (γ 1 × δ × γ 0)) => e₁_hat n p.1 p.2))
-- Pointwise overlap of the estimator on `H_ε` at both stages.
(h_e_overlap_hat :
∀ n ω,
(∀ s₀, ε ≤ e₀_hat n ω s₀ ∧ e₀_hat n ω s₀ ≤ 1 - ε)
∧ (∀ h, ε ≤ e₁_hat n ω h ∧ e₁_hat n ω h ≤ 1 - ε))
-- Per-`(n, ω)` `MemLp` hypotheses on each hat.
(h_mu0_memLp : ∀ n ω, MemLp (fun s₀ => μ₀_hat n ω s₀) 2 S.P_H₀)
(h_e0_memLp : ∀ n ω, MemLp (fun s₀ => e₀_hat n ω s₀) 2 S.P_H₀)
(h_mu1_memLp : ∀ n ω, MemLp (fun h => μ₁_hat n ω h) 2 S.P_H₁)
(h_e1_memLp : ∀ n ω, MemLp (fun h => e₁_hat n ω h) 2 S.P_H₁)
-- Fold-A measurability witnesses (per stage).
(h_mu0_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(μ₀_hat n))
(h_e0_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(e₀_hat n))
(h_mu1_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(μ₁_hat n))
(h_e1_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(e₁_hat n))
-- Joint fold-A measurability on the uncurried form (per stage).
(h_mu0_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ 0))]
(fun (p : P.Ω × γ 0) => μ₀_hat n p.1 p.2))
(h_e0_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ 0))]
(fun (p : P.Ω × γ 0) => e₀_hat n p.1 p.2))
(h_mu1_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ 1 × δ × γ 0))]
(fun (p : P.Ω × (γ 1 × δ × γ 0)) => μ₁_hat n p.1 p.2))
(h_e1_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ 1 × δ × γ 0))]
(fun (p : P.Ω × (γ 1 × δ × γ 0)) => e₁_hat n p.1 p.2))
-- Stagewise individual `o_p(1)` rates on `‖Δ·‖_{L²(P_H_k)}`.
(h_mu0_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_mu1_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_e0_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_e1_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun _ => (1 : ℝ)) P.μ)
-- Cross-stage product rates: every `(μ_a, e_b)` pair is `o_p(n^{-1/2})`.
(h_product_rate_00 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_11 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_01 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ => μ₀_hat n ω s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun h => e₁_hat n ω h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_10 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h => μ₁_hat n ω h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun s₀ => e₀_hat n ω s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) :
IsAsymLinear
(dml_DTR_estimator S sample split
(fun n ω =>
{ μ₀_fn := μ₀_hat n ω
e₀_fn := e₀_hat n ω
μ₁_fn := μ₁_hat n ω
e₁_fn := e₁_hat n ω
μ₀_meas :=
(h_mu0_meas n).comp
(prodMk measurable_const measurable_id)
e₀_meas :=
(h_e0_meas n).comp
(prodMk measurable_const measurable_id)
μ₁_meas :=
(h_mu1_meas n).comp
(prodMk measurable_const measurable_id)
e₁_meas :=
(h_e1_meas n).comp
(prodMk measurable_const measurable_id) }))
S.θ₀
S.ψ_seqDR
sample
split.foldB := by
let η_hat : ℕ → P.Ω → DTRNuisanceVec₂ δ γ := fun n ω =>
{ μ₀_fn := μ₀_hat n ω
e₀_fn := e₀_hat n ω
μ₁_fn := μ₁_hat n ω
e₁_fn := e₁_hat n ω
μ₀_meas :=
(h_mu0_meas n).comp
(prodMk measurable_const measurable_id)
e₀_meas :=
(h_e0_meas n).comp
(prodMk measurable_const measurable_id)
μ₁_meas :=
(h_mu1_meas n).comp
(prodMk measurable_const measurable_id)
e₁_meas :=
(h_e1_meas n).comp
(prodMk measurable_const measurable_id) }
have h_in_Hε : ∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε := by
intro n ω
exact h_e_overlap_hat n ω
haveI : IsProbabilityMeasure S.P_H₀ := by
unfold DTREstimationSystem.P_H₀
exact Measure.isProbabilityMeasure_map
(S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable
haveI : IsProbabilityMeasure S.P_H₁ := by
unfold DTREstimationSystem.P_H₁
exact Measure.isProbabilityMeasure_map
((S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩))).aemeasurable
haveI : IsProbabilityMeasure S.P_Z := by
unfold DTREstimationSystem.P_Z
exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable
have hμ0_val_memLp : MemLp S.μ₀_val 2 S.P_H₀ := by
have hYd_L2 : MemLp (S.toPODTRSystem.Y_of S.dbar) 2 P.μ :=
(memLp_two_iff_integrable_sq
(S.toPODTRSystem.measurable_Y_of S.dbar).aestronglyMeasurable).2
(h_yd2 S.dbar)
-- … truncated; follow the source link for the rest …
DTRInstance 2 core · 2 supporting This file instantiates the abstract orthogonal-moment framework with the two-period sequential doubly robust moment for a dynamic treatment regime. ★ seqDR_dml_isAsymLinear
Sequential Doubly Robust Moment Instance
This file instantiates the abstract orthogonal-moment framework with the two-period sequential doubly robust moment for a dynamic treatment regime. It records the mean-zero, bilinear-remainder, and asymptotic-linearity ingredients needed to reuse the general DML theorem.
def seqDRGeneralMoment reviewed
⚑ flagged
Causalean.Estimation.DTR
Sequential DR (DTR, n = 2) instance of the abstract GeneralMoment.
Definition (Lean source)
noncomputable def seqDRGeneralMoment
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_e_pointwise :
(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε)
∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)) :
GeneralMoment P.Ω P.μ (γ 0 × δ × γ 1 × δ × ℝ) S.P_Z
(DTRNuisanceVec₂ δ γ) where
m := fun η z θ => S.seqDRMomentFunctional η z θ
η₀ := S.η₀
θ₀ := S.θ₀
H_ε := DTREstimationSystem.H_ε ε
ρ₁ := fun η η' =>
⟨(eLpNorm (fun s₀ => η.μ₀_fn s₀ - η'.μ₀_fn s₀) 2 S.P_H₀).toReal +
(eLpNorm (fun h => η.μ₁_fn h - η'.μ₁_fn h) 2 S.P_H₁).toReal,
by positivity⟩
ρ₂ := fun η η' =>
⟨(eLpNorm (fun s₀ => η.e₀_fn s₀ - η'.e₀_fn s₀) 2 S.P_H₀).toReal +
(eLpNorm (fun h => η.e₁_fn h - η'.e₁_fn h) 2 S.P_H₁).toReal,
by positivity⟩
m_meas := fun η θ => S.measurable_seqDRMomentFunctional η θ
η₀_mem := h_e_pointwise
-- Sequential DR is a linear score `m_seqDR(η, z, θ) = ψ_seqDR(η, z) − θ`,
-- so the population Jacobian
-- `J₀ = ∂_θ ∫ m(η₀, z, θ) dP_Z |_{θ=θ₀} = −1`.
J₀ := -1
J₀_ne_zero := by norm_num
theorem seqDR_dml_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.DTR
Headline sequential DR (DTR) DML asymptotic-linearity theorem, derived from the abstract dml_chernozhukov_asymptoticLinear in Estimation/OrthogonalMoments/DMLChernozhukov.lean. Fix a dynamic-treatment-regime estimation system with strict two-stage propensity overlap and satisfying the DTR identification assumptions, and suppose the factual outcome and every counterfactual outcome under a fixed treatment history have finite second moment. Given an i.i.d. sample together with a one-shot cross-fitting split whose estimation-fold share converges to some constant strictly between and , and a sequence of nuisance estimators η_hat that remain in the -overlap ball, with stagewise outcome-regression and propensity errors that are square-integrable, such that the resulting moment function is measurable against the sample and each cross-fitting fold, and is both integrable and square-integrable, and such that the individual L² nuisance-error rates vanish while their product is , then the resulting Chernozhukov one-step DML estimator is asymptotically linear at the true sequential-DR parameter, with influence function the sequential doubly-robust score evaluated at the truth.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_e_pointwise :
(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)
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.μ
sample :
IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
_hc_lt :
c < 1
η_hat :
ℕ → P.Ω → DTRNuisanceVec₂ δ γ
h_in_Hε :
∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε
h_mu0_diff_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀
h_mu1_diff_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁
h_e0_diff_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀
h_e1_diff_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁
h_m_meas :
∀ n,
Measurable (fun (p : P.Ω × (γ 0 × δ × γ 1 × δ × ℝ)) => S.seqDRMomentFunctional (η_hat n p.1) p.2 S.θ₀)
h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.seqDRMomentFunctional (η_hat n ω) z S.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ 0 × δ × γ 1 × δ × ℝ))] (fun (p : P.Ω × (γ 0 × δ × γ 1 × δ × ℝ)) => S.seqDRMomentFunctional (η_hat n p.1) p.2 S.θ₀)
h_m_int :
∀ n ω, Integrable (fun z => S.seqDRMomentFunctional (η_hat n ω) z S.θ₀) S.P_Z
h_m_sq_int :
∀ n ω, Integrable (fun z => (S.seqDRMomentFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z
h_indiv_rate_ρ₁ :
IsLittleOp (fun n ω => (((seqDRGeneralMoment S h_e_pointwise).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ
h_indiv_rate_ρ₂ :
IsLittleOp (fun n ω => (((seqDRGeneralMoment S h_e_pointwise).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
IsLittleOp (fun n ω => (((seqDRGeneralMoment S h_e_pointwise).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((seqDRGeneralMoment S h_e_pointwise).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
conclusion
IsAsymLinear (dmlChernozhukovEstimator (seqDRGeneralMoment S h_e_pointwise) sample split η_hat) S.θ₀ (fun z => -(seqDRGeneralMoment S h_e_pointwise).J₀_inv * S.seqDRMomentFunctional S.η₀ z S.θ₀) sample split.foldB
Proof (Lean source)
theorem seqDR_dml_isAsymLinear
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_e_pointwise :
(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε)
∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε))
(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.μ)
(sample : IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
{c : ℝ} (hc_pos : 0 < c) (_hc_lt : c < 1)
(h_split_rate :
Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c))
(η_hat : ℕ → P.Ω → DTRNuisanceVec₂ δ γ)
(h_in_Hε : ∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε)
(h_mu0_diff_memLp : ∀ n ω,
MemLp (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀)
(h_mu1_diff_memLp : ∀ n ω,
MemLp (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁)
(h_e0_diff_memLp : ∀ n ω,
MemLp (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀)
(h_e1_diff_memLp : ∀ n ω,
MemLp (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁)
(h_m_meas :
∀ n, Measurable (fun (p : P.Ω × (γ 0 × δ × γ 1 × δ × ℝ)) =>
S.seqDRMomentFunctional (η_hat n p.1) p.2 S.θ₀))
(h_m_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω z => S.seqDRMomentFunctional (η_hat n ω) z S.θ₀))
(h_m_foldA_uncurry :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ 0 × δ × γ 1 × δ × ℝ))]
(fun (p : P.Ω × (γ 0 × δ × γ 1 × δ × ℝ)) =>
S.seqDRMomentFunctional (η_hat n p.1) p.2 S.θ₀))
(h_m_int : ∀ n ω,
Integrable (fun z => S.seqDRMomentFunctional (η_hat n ω) z S.θ₀) S.P_Z)
(h_m_sq_int : ∀ n ω,
Integrable
(fun z => (S.seqDRMomentFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z)
(h_indiv_rate_ρ₁ :
IsLittleOp
(fun n ω =>
(((seqDRGeneralMoment S h_e_pointwise).ρ₁
(η_hat n ω) S.η₀ : NNReal) : ℝ))
(fun _ => (1 : ℝ)) P.μ)
(h_indiv_rate_ρ₂ :
IsLittleOp
(fun n ω =>
(((seqDRGeneralMoment S h_e_pointwise).ρ₂
(η_hat n ω) S.η₀ : NNReal) : ℝ))
(fun _ => (1 : ℝ)) P.μ)
(h_product_rate :
IsLittleOp
(fun n ω =>
(((seqDRGeneralMoment S h_e_pointwise).ρ₁
(η_hat n ω) S.η₀ : NNReal) : ℝ) *
(((seqDRGeneralMoment S h_e_pointwise).ρ₂
(η_hat n ω) S.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) :
IsAsymLinear
(dmlChernozhukovEstimator
(seqDRGeneralMoment S h_e_pointwise) sample split η_hat)
S.θ₀
(fun z => -(seqDRGeneralMoment S h_e_pointwise).J₀_inv *
S.seqDRMomentFunctional S.η₀ z S.θ₀)
sample
split.foldB := by
have hMZ := seqDR_meanZero S h_e_pointwise h_overlap hA h_y2
have hFV :
Integrable (fun z =>
((seqDRGeneralMoment S h_e_pointwise).m
(seqDRGeneralMoment S h_e_pointwise).η₀ z
(seqDRGeneralMoment S h_e_pointwise).θ₀) ^ 2) S.P_Z := by
simpa [seqDRGeneralMoment, DTREstimationSystem.ψ_seqDR,
DTREstimationSystem.η₀, DTREstimationSystem.seqDRMomentFunctional,
DTREstimationSystem.seqDRMoment] using
seqDR_finite_var S h_overlap hA h_y2 h_yd2
have hBR_at :
∀ n ω,
|∫ z, (seqDRGeneralMoment S h_e_pointwise).m (η_hat n ω) z
(seqDRGeneralMoment S h_e_pointwise).θ₀ ∂S.P_Z| ≤
seqDR_rem_const ε *
(((seqDRGeneralMoment S h_e_pointwise).ρ₁
(η_hat n ω) (seqDRGeneralMoment S h_e_pointwise).η₀ : NNReal) : ℝ) *
(((seqDRGeneralMoment S h_e_pointwise).ρ₂
(η_hat n ω) (seqDRGeneralMoment S h_e_pointwise).η₀ : NNReal) : ℝ) := by
intro n ω
have h := seqDR_remainder_bound S h_overlap hA h_y2 h_yd2
(η_hat n ω) (h_in_Hε n ω)
(h_mu0_diff_memLp n ω) (h_mu1_diff_memLp n ω)
(h_e0_diff_memLp n ω) (h_e1_diff_memLp n ω)
change |∫ z, S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)| ≤
seqDR_rem_const ε *
((eLpNorm (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal +
(eLpNorm (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) *
((eLpNorm (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal +
(eLpNorm (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
exact h
have h_mu0_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal)
(fun _ => (1 : ℝ)) P.μ := by
intro δ hδ
rw [ENNReal.tendsto_nhds_zero]
intro κ hκ
have hsum_event :=
(ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₁ δ hδ)) κ hκ
filter_upwards [hsum_event] with n hn
refine (measure_mono ?_).trans hn
intro ω hω
have hcoord_le :
|(eLpNorm
(fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal| ≤
|(((seqDRGeneralMoment S h_e_pointwise).ρ₁
(η_hat n ω) S.η₀ : NNReal) : ℝ)| := by
simp only [seqDRGeneralMoment, DTREstimationSystem.η₀]
rw [abs_of_nonneg ENNReal.toReal_nonneg]
exact (le_add_of_nonneg_right ENNReal.toReal_nonneg).trans (le_abs_self _)
exact lt_of_lt_of_le hω hcoord_le
have h_mu1_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal)
(fun _ => (1 : ℝ)) P.μ := by
intro δ hδ
rw [ENNReal.tendsto_nhds_zero]
intro κ hκ
have hsum_event :=
(ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₁ δ hδ)) κ hκ
filter_upwards [hsum_event] with n hn
refine (measure_mono ?_).trans hn
intro ω hω
have hcoord_le :
|(eLpNorm
(fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal| ≤
|(((seqDRGeneralMoment S h_e_pointwise).ρ₁
(η_hat n ω) S.η₀ : NNReal) : ℝ)| := by
simp only [seqDRGeneralMoment, DTREstimationSystem.η₀]
rw [abs_of_nonneg ENNReal.toReal_nonneg]
exact (le_add_of_nonneg_left ENNReal.toReal_nonneg).trans (le_abs_self _)
exact lt_of_lt_of_le hω hcoord_le
have h_e0_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun _ => (1 : ℝ)) P.μ := by
intro δ hδ
rw [ENNReal.tendsto_nhds_zero]
intro κ hκ
have hsum_event :=
(ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₂ δ hδ)) κ hκ
filter_upwards [hsum_event] with n hn
refine (measure_mono ?_).trans hn
intro ω hω
have hcoord_le :
|(eLpNorm
(fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal| ≤
|(((seqDRGeneralMoment S h_e_pointwise).ρ₂
(η_hat n ω) S.η₀ : NNReal) : ℝ)| := by
simp only [seqDRGeneralMoment, DTREstimationSystem.η₀]
rw [abs_of_nonneg ENNReal.toReal_nonneg]
exact (le_add_of_nonneg_right ENNReal.toReal_nonneg).trans (le_abs_self _)
exact lt_of_lt_of_le hω hcoord_le
have h_e1_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun _ => (1 : ℝ)) P.μ := by
intro δ hδ
rw [ENNReal.tendsto_nhds_zero]
intro κ hκ
have hsum_event :=
(ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₂ δ hδ)) κ hκ
filter_upwards [hsum_event] with n hn
refine (measure_mono ?_).trans hn
intro ω hω
have hcoord_le :
|(eLpNorm
(fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal| ≤
|(((seqDRGeneralMoment S h_e_pointwise).ρ₂
(η_hat n ω) S.η₀ : NNReal) : ℝ)| := by
simp only [seqDRGeneralMoment, DTREstimationSystem.η₀]
rw [abs_of_nonneg ENNReal.toReal_nonneg]
exact (le_add_of_nonneg_left ENNReal.toReal_nonneg).trans (le_abs_self _)
exact lt_of_lt_of_le hω hcoord_le
have h_score_diff_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun z =>
(seqDRGeneralMoment S h_e_pointwise).m (η_hat n ω) z
(seqDRGeneralMoment S h_e_pointwise).θ₀ -
(seqDRGeneralMoment S h_e_pointwise).m
(seqDRGeneralMoment S h_e_pointwise).η₀ z
(seqDRGeneralMoment S h_e_pointwise).θ₀)
2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
simpa [seqDRGeneralMoment] using
seqDR_score_diff_isLittleOp_one
S h_overlap hA h_y2 h_yd2 η_hat h_in_Hε
h_mu0_diff_memLp h_mu1_diff_memLp h_e0_diff_memLp h_e1_diff_memLp
h_mu0_rate h_mu1_rate h_e0_rate h_e1_rate
-- … truncated; follow the source link for the rest …
2 supporting declarations (lemmas, instances)
-
seqDR_meanZerotheorem — Sequential DR (DTR) satisfies MeanZero.hypothesesS :DTREstimationSystem P δ γε :ℝh_e_pointwise :(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)h_overlap :S.StrictOverlap εhA :S.toPODTRSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μconclusionMeanZero (seqDRGeneralMoment S h_e_pointwise)Proof (Lean source)
theorem seqDR_meanZero (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_e_pointwise : (∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)) (h_overlap : S.StrictOverlap ε) (hA : S.toPODTRSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) : MeanZero (seqDRGeneralMoment S h_e_pointwise) := by unfold MeanZero seqDRGeneralMoment exact seqDR_mean_zero S h_overlap hA h_y2 -
seqDR_bilinearRemtheorem — Sequential DR (DTR) satisfies BilinearRemainder with constant seqDR_rem_const ε.hypothesesS :DTREstimationSystem P δ γε :ℝh_e_pointwise :(∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)h_overlap :S.StrictOverlap εhA :S.toPODTRSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μh_yd2 :∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μconclusion∃ C, BilinearRemainder (seqDRGeneralMoment S h_e_pointwise) CProof (Lean source)
theorem seqDR_bilinearRem (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_e_pointwise : (∀ s₀, ε ≤ S.e₀_val s₀ ∧ S.e₀_val s₀ ≤ 1 - ε) ∧ (∀ h, ε ≤ S.e₁_val h ∧ S.e₁_val h ≤ 1 - ε)) (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.μ) (h_L2 : ∀ η ∈ DTREstimationSystem.H_ε (δ := δ) (γ := γ) ε, MemLp (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀ ∧ MemLp (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁ ∧ MemLp (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀ ∧ MemLp (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁) : ∃ C, BilinearRemainder (seqDRGeneralMoment S h_e_pointwise) C := by refine ⟨seqDR_rem_const ε, ?_⟩ intro η hη obtain ⟨hΔμ₀, hΔμ₁, hΔe₀, hΔe₁⟩ := h_L2 η hη have h := seqDR_remainder_bound S h_overlap hA h_y2 h_yd2 η hη hΔμ₀ hΔμ₁ hΔe₀ hΔe₁ change |∫ z, S.seqDRMomentFunctional η z S.θ₀ ∂(S.P_Z)| ≤ seqDR_rem_const ε * ((eLpNorm (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal + (eLpNorm (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) * ((eLpNorm (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal + (eLpNorm (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) exact h
FiniteVar 1 core · 1 supporting This file proves square integrability of the sequential doubly robust influence function for a two-stage dynamic treatment regime. ★ seqDR_finite_var
Finite Variance for Sequential DR
This file proves square integrability of the sequential doubly robust influence function for a two-stage dynamic treatment regime. The proof extends the average-treatment-effect finite-variance argument to stagewise histories, propensity weights, and counterfactual outcome regressions under strict overlap.
theorem seqDR_finite_var reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Finite variance of the sequential doubly robust score — sequential DR (DTR) analogue of aipw_finite_var. Under the two-stage DTR backdoor assumptions — sequential exchangeability, consistency, stagewise positivity, and integrability of every counterfactual outcome, uniform two-stage strict overlap: the target-regime propensity at each stage lies almost surely in [ε, 1-ε] for some ε in (0, 1/2], a finite second moment for the observed factual outcome, and a finite second moment for every counterfactual outcome under a treatment sequence, the sequential doubly robust influence function ψ_seqDR is square-integrable against the joint law of the observed two-stage data tuple.
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.μ
conclusion
Integrable (fun z => (S.ψ_seqDR z) ^ 2) (S.P_Z)
Proof (Lean source)
theorem seqDR_finite_var (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.μ) :
Integrable (fun z => (S.ψ_seqDR z) ^ 2) (S.P_Z) := by
have hψ_meas : Measurable S.ψ_seqDR := by
exact S.measurable_seqDRMomentFunctional S.η₀ S.θ₀
have hY_L2 : MemLp S.toPODTRSystem.factualY 2 P.μ :=
(memLp_two_iff_integrable_sq
S.toPODTRSystem.measurable_factualY.aestronglyMeasurable).2 h_y2
have hYd_L2 : MemLp (S.toPODTRSystem.Y_of S.dbar) 2 P.μ :=
(memLp_two_iff_integrable_sq
(S.toPODTRSystem.measurable_Y_of S.dbar).aestronglyMeasurable).2
(h_yd2 S.dbar)
have hμ0_L2 :
MemLp
(fun ω => S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))
2 P.μ := by
have hcond_L2 :
MemLp ((S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven
(S.toPODTRSystem.Y_of S.dbar) P.μ) 2 P.μ := by
simpa [POCFBundle.condExpGiven] using hYd_L2.condExp
exact hcond_L2.ae_eq (S.μ₀_compat hA)
have hμ1_L2 :
MemLp
(fun ω => S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) 2 P.μ := by
exact (S.stageOneReg_memLp h_overlap h_y2).ae_eq
(S.μ₁_val_comp_eq_stageOneReg).symm
have he0_lower :
∀ᵐ ω ∂P.μ,
ε ≤ S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) := by
filter_upwards [h_overlap.2.2, S.e₀_compat] with ω hover hcomp
rw [← hcomp]
exact hover.1.1
have he1_lower :
∀ᵐ ω ∂P.μ,
ε ≤ S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) := by
filter_upwards [h_overlap.2.2, S.e₁_compat] with ω hover hcomp
rw [← hcomp]
exact hover.2.1
have hw0_bound :
∀ᵐ ω ∂P.μ,
‖indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)‖ ≤ ε⁻¹ := by
filter_upwards [he0_lower] with ω he
by_cases hD : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω =
S.dbar ⟨0, by decide⟩
· have hpos : 0 < S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) :=
S.e₀_pos _
have hle : (S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos h_overlap.1).2 he
rw [indEq, if_pos hD, norm_div, norm_one, Real.norm_eq_abs, abs_of_pos hpos]
simpa [one_div] using hle
· have hεinv_nonneg : 0 ≤ ε⁻¹ := inv_nonneg.mpr h_overlap.1.le
rw [indEq, if_neg hD, zero_div, norm_zero]
exact hεinv_nonneg
have hw1_bound :
∀ᵐ ω ∂P.μ,
‖(indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))‖ ≤ (ε * ε)⁻¹ := by
filter_upwards [he0_lower, he1_lower] with ω he0 he1
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 hpos0 : 0 < S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) :=
S.e₀_pos _
have hpos1 : 0 < S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) :=
S.e₁_pos _
have hle0 : (S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹
≤ ε⁻¹ :=
(inv_le_inv₀ hpos0 h_overlap.1).2 he0
have hle1 :
(S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos1 h_overlap.1).2 he1
have hle :
(S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹ *
(S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))⁻¹
≤ ε⁻¹ * ε⁻¹ :=
mul_le_mul hle1 hle0 (inv_nonneg.mpr hpos0.le)
(inv_nonneg.mpr h_overlap.1.le)
have hD0n : S.toPODTRSystem.factualD 0 ω = S.dbar 0 := by
simpa using hD0
have hD1n : S.toPODTRSystem.factualD 1 ω = S.dbar 1 := by
simpa using hD1
have hind0eq : indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) = 1 := by
simpa using (show indEq (S.toPODTRSystem.factualD 0 ω) (S.dbar 0) = 1 by
simp [indEq, hD0n])
have hind1eq : indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩) = 1 := by
simpa using (show indEq (S.toPODTRSystem.factualD 1 ω) (S.dbar 1) = 1 by
simp [indEq, hD1n])
rw [hind0eq, hind1eq, one_mul, norm_div, norm_one, norm_mul]
rw [show ‖S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)‖ =
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) from
Real.norm_of_nonneg hpos0.le]
rw [show ‖S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)‖ =
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) from
Real.norm_of_nonneg hpos1.le]
simpa [one_div, mul_comm, mul_left_comm, mul_assoc] using hle
· have hεεinv_nonneg : 0 ≤ (ε * ε)⁻¹ :=
inv_nonneg.mpr (mul_nonneg h_overlap.1.le h_overlap.1.le)
have hD1n : ¬S.toPODTRSystem.factualD 1 ω = S.dbar 1 := by
simpa using hD1
have hind1eq : indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩) = 0 := by
simpa using (show indEq (S.toPODTRSystem.factualD 1 ω) (S.dbar 1) = 0 by
simp [indEq, hD1n])
rw [hind1eq, mul_zero, zero_div, norm_zero]
exact hεεinv_nonneg
· have hεεinv_nonneg : 0 ≤ (ε * ε)⁻¹ :=
inv_nonneg.mpr (mul_nonneg h_overlap.1.le h_overlap.1.le)
rw [indEq, if_neg hD0, zero_mul, zero_div, norm_zero]
exact hεεinv_nonneg
have hw0_Linf :
MemLp
(fun ω => indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) ⊤ P.μ := by
refine MemLp.of_bound ?_ ε⁻¹ hw0_bound
apply Measurable.aestronglyMeasurable
exact ((measurable_indEq_left (S.dbar ⟨0, by decide⟩)).comp
(S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩)).div
(S.e₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩))
have hw1_Linf :
MemLp
(fun ω =>
(indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) ⊤ P.μ := by
refine MemLp.of_bound ?_ (ε * ε)⁻¹ hw1_bound
apply Measurable.aestronglyMeasurable
have hind0 : Measurable (fun ω => indEq
(S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩)) :=
(measurable_indEq_left (S.dbar ⟨0, by decide⟩)).comp
(S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩)
have hind1 : Measurable (fun ω => indEq
(S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) :=
(measurable_indEq_left (S.dbar ⟨1, by decide⟩)).comp
(S.toPODTRSystem.measurable_factualD ⟨1, by decide⟩)
have he0 : Measurable (fun ω =>
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) :=
S.e₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)
have he1 : Measurable (fun ω =>
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) :=
S.e₁_meas.comp
((S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)))
exact (hind0.mul hind1).div (he0.mul he1)
have hterm0_L2 :
MemLp
(fun ω =>
(indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
S.e₀_val (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⟩ ω) -
S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) 2 P.μ := by
exact (hμ1_L2.sub hμ0_L2).mul hw0_Linf
have hterm1_L2 :
MemLp
(fun ω =>
((indEq (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) *
(S.toPODTRSystem.factualY ω -
S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))) 2 P.μ := by
exact (hY_L2.sub hμ1_L2).mul hw1_Linf
have hψ_comp_L2 : MemLp (fun ω => S.ψ_seqDR (S.factualZ ω)) 2 P.μ := by
have hconst_L2 : MemLp (fun _ : P.Ω => S.θ₀) 2 P.μ := memLp_const _
have hsum_L2 :=
((hμ0_L2.add hterm0_L2).add hterm1_L2).sub hconst_L2
simp only [DTREstimationSystem.ψ_seqDR, DTREstimationSystem.seqDRMoment,
seqDRMoment, DTREstimationSystem.factualZ,
projS₀, projD₀, projS₁, projD₁, projY, histH₁,
DTREstimationSystem.η₀]
exact hsum_L2
have hψ_L2 : MemLp S.ψ_seqDR 2 (S.P_Z) := by
rw [DTREstimationSystem.P_Z]
exact (memLp_map_measure_iff hψ_meas.aestronglyMeasurable
S.measurable_factualZ.aemeasurable).2 hψ_comp_L2
-- … truncated; follow the source link for the rest …
1 supporting declaration (lemmas, instances)
-
measurable_ψ_seqDR_squaredlemma — Measurability helper: the squared sequential DR influence function on the data tuple is measurable. Used in the L² bookkeeping for seqDR_finite_var.hypothesesS :DTREstimationSystem P δ γconclusionMeasurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => (S.ψ_seqDR z) ^ 2)Proof (Lean source)
lemma measurable_ψ_seqDR_squared (S : DTREstimationSystem P δ γ) : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => (S.ψ_seqDR z) ^ 2) := by exact (S.measurable_seqDRMomentFunctional S.η₀ S.θ₀).pow_const 2
MeanZero 1 core · 6 supporting Proves mean-zero properties for the sequential doubly robust score. ★ seqDR_mean_zero
Proves mean-zero properties for the sequential doubly robust score. The module handles measurability, conditioning, and stagewise cancellation needed for the DTR influence-function argument.
theorem seqDR_mean_zero reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Mean zero of the sequential doubly robust score. Under the two-stage DTR backdoor assumptions — sequential exchangeability, consistency, stagewise positivity, and integrability of every counterfactual outcome, uniform two-stage strict overlap: the target-regime propensity at each stage lies almost surely in [ε, 1-ε] for some ε in (0, 1/2], and a finite second moment for the observed factual outcome, then the sequential doubly robust influence function ψ_seqDR has expectation zero under the observed two-stage data law.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPODTRSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
conclusion
(∫ z, S.ψ_seqDR z ∂(S.P_Z)) = 0
Proof (Lean source)
theorem seqDR_mean_zero (S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(hA : S.toPODTRSystem.Assumptions)
(h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) :
(∫ z, S.ψ_seqDR z ∂(S.P_Z)) = 0 := by
rw [DTREstimationSystem.P_Z]
rw [MeasureTheory.integral_map S.measurable_factualZ.aemeasurable
(S.measurable_ψ_seqDR).aestronglyMeasurable]
exact seqDR_factualZ_integral_zero S h_overlap hA h_y2
6 supporting declarations (lemmas, instances)
-
measurable_ψ_seqDRlemma — Measurability of the sequential DR influence function on the data tuple (s₀, d₀, s₁, d₁, y) : γ 0 × δ × γ 1 × δ × ℝ. Decomposes into Measurable.add/Measurable.mul/Measurable.div chained against the projections, the indicator functions indEq, and the value-space nuisance functions stored in S.η₀.Proof (Lean source)
lemma measurable_ψ_seqDR (S : DTREstimationSystem P δ γ) : Measurable S.ψ_seqDR := by exact S.measurable_seqDRMomentFunctional S.η₀ S.θ₀ -
propScore_ne_zero_stage0lemma — Stage-0 propensity is a.e. nonzero under the DTR backdoor assumptions. The conditional indicator μ[1{D₀ = dbar 0} | σ(historyBundle 0)] is identified via e₀_compat with e₀_val ∘ factualS 0, and e₀_val > 0 pointwise on γ 0.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.AssumptionsProof (Lean source)
lemma propScore_ne_zero_stage0 (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : ∀ᵐ ω ∂P.μ, (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven ((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩)) P.μ ω ≠ 0 := by filter_upwards [hA.overlap S.dbar ⟨0, by decide⟩] with ω hω exact ne_of_gt hω -
propScore_ne_zero_stage1lemma — Stage-1 propensity is a.e. nonzero under the DTR backdoor assumptions. Analogous to propScore_ne_zero_stage0 via e₁_compat and e₁_pos.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.AssumptionsProof (Lean source)
lemma propScore_ne_zero_stage1 (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : ∀ᵐ ω ∂P.μ, (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven ((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩)) P.μ ω ≠ 0 := by filter_upwards [hA.overlap S.dbar ⟨1, by decide⟩] with ω hω exact ne_of_gt hω -
cond_exp_residual_zero_stage0lemma — Stage-0 residual conditional expectation is zero a.s.: under DTR assumptions, μ[1{D₀=dbar 0}·(μ₁_val(history₁) − μ₀_val(S₀)) | σ(historyBundle 0)] =ᵐ 0.hypothesesS :DTREstimationSystem P δ γε :ℝh_overlap :S.StrictOverlap εhA :S.toPODTRSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μconclusion(S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven (fun ω => (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.μ=ᵐ[P.μ] (fun _ => (0 : ℝ))Proof (Lean source)
lemma cond_exp_residual_zero_stage0 (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPODTRSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) : (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven (fun ω => (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.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by let B0 := S.toPODTRSystem.historyBundle 0 (by decide) let B1 := S.toPODTRSystem.historyBundle 1 (by decide) let I0 : P.Ω → ℝ := (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) let Y : P.Ω → ℝ := S.toPODTRSystem.Y_of S.dbar let M0 : P.Ω → ℝ := fun ω => S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) let M1 : P.Ω → ℝ := fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hY_int : Integrable Y P.μ := by simpa [Y] using hA.integrable_Y S.dbar have hI0_int : Integrable I0 P.μ := by simpa [I0] using (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_indicator (S.dbar ⟨0, by decide⟩) have hI0Y_int : Integrable (fun ω => I0 ω * Y ω) P.μ := by have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hY_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, Y, mul_comm])) have hM0_int : Integrable M0 P.μ := by exact (B0.integrable_condExpGiven (S.toPODTRSystem.Y_of S.dbar)).congr (by simpa [B0, M0] using S.μ₀_compat hA) have hM1_int : Integrable M1 P.μ := by have hM1_L2 : MemLp M1 2 P.μ := by simpa [M1] 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 exact S.μ₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩) have hM1_meas : Measurable M1 := by have hs1 := S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩ have hd0 := S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩ have hs0 := S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩ exact S.μ₁_meas.comp (hs1.prod (hd0.prod hs0)) 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 hres_eq : (fun ω => I0 ω * (M1 ω - M0 ω)) = (fun ω => I0 ω * M1 ω - I0 ω * M0 ω) := by funext ω ring have hsub : B0.condExpGiven (fun ω => I0 ω * M1 ω - I0 ω * M0 ω) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ - B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ := by simp only [POCFBundle.condExpGiven] exact MeasureTheory.condExp_sub hI0M1_int hI0M0_int B0.sigma have hI0_sm_B1 : StronglyMeasurable[B1.sigma] I0 := by simpa [B1, I0] using S.toPODTRSystem.stronglyMeasurable_indicator_dVar_sigma_history 1 (by decide) ⟨0, by decide⟩ (by decide) (S.dbar ⟨0, by decide⟩) have hrev_B1 : (fun ω => I0 ω * M1 ω) =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by have hI0_eq_indD : I0 = S.toPODTRSystem.indD S.dbar 1 := by funext ω have hsplit := congr_fun (S.toPODTRSystem.indD_factor_split S.dbar 0 (by decide)) ω simp [I0, PODTRSystem.indD] at hsplit ⊢ have hpull := B1.condExpGiven_mul_of_stronglyMeasurable_left (f := I0) (g := Y) hI0_sm_B1 hI0Y_int hY_int filter_upwards [hpull, S.indD_mul_μ₁_val_comp_eq hA] with ω hp hμ1 have hp' : B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ ω = I0 ω * B1.condExpGiven Y P.μ ω := by exact hp have hμ1_local : I0 ω * M1 ω = I0 ω * B1.condExpGiven Y P.μ ω := by have hμ1' : S.toPODTRSystem.indD S.dbar 1 ω * M1 ω = S.toPODTRSystem.indD S.dbar 1 ω * B1.condExpGiven Y P.μ ω := hμ1 rw [hI0_eq_indD] exact hμ1' rw [hp'] exact hμ1_local haveI : IsFiniteMeasure (P.μ.trim B1.sigma_le) := isFiniteMeasure_trim _ have hB0_le_B1 : B0.sigma ≤ B1.sigma := by simpa [B0, B1] using S.toPODTRSystem.historyBundle_sigma_mono 0 1 (by decide) (by decide) have htower : B0.condExpGiven (B1.condExpGiven (fun ω => I0 ω * Y ω) P.μ) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by have h := B1.condExpGiven_tower_of_le (g := fun ω => I0 ω * Y ω) (μ := P.μ) (m := B0.sigma) hB0_le_B1 simpa [POCFBundle.condExpGiven] using h have hCE_I0M1_to_Y : B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ =ᵐ[P.μ] B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ := by exact (B0.condExpGiven_congr_ae hrev_B1).trans htower have hcfY_n : (S.toPODTRSystem.cfYBundle S.dbar).n = 1 := rfl let i0 : Fin (S.toPODTRSystem.cfYBundle S.dbar).n := ⟨0, by rw [hcfY_n]; exact Nat.one_pos⟩ let ψ : (∀ i : Fin (S.toPODTRSystem.cfYBundle S.dbar).n, (S.toPODTRSystem.cfYBundle S.dbar).type i) → ℝ := fun f => (f i0 : ℝ) have hψ_meas : Measurable ψ := by change Measurable (fun f : (∀ i, (S.toPODTRSystem.cfYBundle S.dbar).type i) => (f i0 : ℝ)) exact measurable_pi_apply i0 have hYof_eq_proj : S.toPODTRSystem.Y_of S.dbar = ψ ∘ (S.toPODTRSystem.cfYBundle S.dbar).jointValue := by funext ω rfl have hCI : CondIndepFun B0.sigma B0.sigma_le (S.toPODTRSystem.factualD ⟨0, by decide⟩) Y P.μ := by have hproj := (hA.exch S.dbar ⟨0, by decide⟩).project (ψ := ψ) hψ_meas change CondIndepFun B0.sigma B0.sigma_le (S.toPODTRSystem.factualD ⟨0, by decide⟩) (S.toPODTRSystem.Y_of S.dbar) P.μ rw [hYof_eq_proj] exact hproj let u : δ → ℝ := ({S.dbar ⟨0, by decide⟩} : Set δ).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := measurable_const.indicator (MeasurableSet.singleton _) have hu_eq : (fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω)) = I0 := by funext ω by_cases h : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω = S.dbar ⟨0, by decide⟩ · have h1 : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω ∈ ({S.dbar ⟨0, by decide⟩} : Set δ) := h have h2 : ω ∈ (S.toPODTRSystem.dVar ⟨0, by decide⟩).event (S.dbar ⟨0, by decide⟩) := h rw [show u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, show I0 ω = (1 : ℝ) from by simpa [I0] using (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_one h2] · have h1 : S.toPODTRSystem.factualD ⟨0, by decide⟩ ω ∉ ({S.dbar ⟨0, by decide⟩} : Set δ) := h have h2 : ω ∉ (S.toPODTRSystem.dVar ⟨0, by decide⟩).event (S.dbar ⟨0, by decide⟩) := h rw [show u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, show I0 ω = (0 : ℝ) from by simpa [I0] using (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator_apply_eq_zero h2] have hfact : P.μ[fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) * Y ω | B0.sigma] =ᵐ[P.μ] P.μ[fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) | B0.sigma] * P.μ[Y | B0.sigma] := condExp_mul_of_condIndep (μ := P.μ) (m := B0.sigma) B0.sigma_le (f := S.toPODTRSystem.factualD ⟨0, by decide⟩) (g := Y) (S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩) (by simpa [Y] using S.toPODTRSystem.measurable_Y_of S.dbar) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hI0_int) hY_int (by change Integrable (fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) * Y ω) P.μ have heq : (fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) * Y ω) = (fun ω => I0 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] rw [heq] exact hI0Y_int) have hExch : B0.condExpGiven (fun ω => I0 ω * Y ω) P.μ =ᵐ[P.μ] (fun ω => B0.condExpGiven I0 P.μ ω * B0.condExpGiven Y P.μ ω) := by unfold POCFBundle.condExpGiven have hprod_rw : (fun ω => u (S.toPODTRSystem.factualD ⟨0, by decide⟩ ω) * Y ω) = (fun ω => I0 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] rw [hprod_rw, hu_eq] at hfact filter_upwards [hfact] with ω hω simpa [Pi.mul_apply] using hω have hCE_I0M1 : B0.condExpGiven (fun ω => I0 ω * M1 ω) P.μ =ᵐ[P.μ] (fun ω => S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by refine hCE_I0M1_to_Y.trans ?_ filter_upwards [hExch, S.e₀_compat, S.μ₀_compat hA] with ω hE he hμ rw [hE, he, hμ] have hM0_sm_B0 : StronglyMeasurable[B0.sigma] M0 := by have hs0 : Measurable[B0.sigma] (S.toPODTRSystem.factualS ⟨0, by decide⟩) := S.toPODTRSystem.measurable_factualS_sigma_history 0 (by decide) ⟨0, by decide⟩ (by decide) exact (S.μ₀_meas.comp hs0).stronglyMeasurable have hpull_M0 := B0.condExpGiven_mul_of_stronglyMeasurable_right (f := I0) (g := M0) hM0_sm_B0 hI0M0_int hI0_int have hCE_I0M0 : B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ =ᵐ[P.μ] (fun ω => S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by filter_upwards [hpull_M0, S.e₀_compat] with ω hp he have hp' : B0.condExpGiven (fun ω => I0 ω * M0 ω) P.μ ω = B0.condExpGiven I0 P.μ ω * M0 ω := by exact hp rw [hp', he] rw [show (fun ω => (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⟩ ω))) = (fun ω => I0 ω * (M1 ω - M0 ω)) by rfl] rw [hres_eq] refine hsub.trans ?_ filter_upwards [hCE_I0M1, hCE_I0M0] with ω h1 h0 -- … truncated; follow the source link for the rest … -
cond_exp_residual_zero_stage1lemma — Stage-1 residual conditional expectation is zero a.s.: under DTR assumptions, the σ(historyBundle 1)-conditional expectation of 1{D₀ = dbar 0} · 1{D₁ = dbar 1} · (factualY − μ₁_val(S₁,D₀,S₀)) is zero a.s.hypothesesS :DTREstimationSystem P δ γε :ℝh_overlap :S.StrictOverlap εhA :S.toPODTRSystem.Assumptionsh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μconclusion(S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (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⟩) ω * (S.toPODTRSystem.factualY ω - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) P.μ=ᵐ[P.μ] (fun _ => (0 : ℝ))Proof (Lean source)
lemma cond_exp_residual_zero_stage1 (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (hA : S.toPODTRSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) : (S.toPODTRSystem.historyBundle 1 (by decide)).condExpGiven (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⟩) ω * (S.toPODTRSystem.factualY ω - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) P.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by let B1 := S.toPODTRSystem.historyBundle 1 (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 Y : P.Ω → ℝ := S.toPODTRSystem.Y_of S.dbar let Yf : P.Ω → ℝ := S.toPODTRSystem.factualY let M1 : P.Ω → ℝ := fun ω => S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hY_int : Integrable Y P.μ := by simpa [Y] using hA.integrable_Y S.dbar have hYf_int : Integrable Yf P.μ := by simpa [Yf] using hA.integrable_factualY have hI0_int : Integrable I0 P.μ := by simpa [I0] using (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_indicator (S.dbar ⟨0, by decide⟩) have hI1_int : Integrable I1 P.μ := by simpa [I1] using (S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_indicator (S.dbar ⟨1, by decide⟩) have hM1_int : Integrable M1 P.μ := by have hM1_L2 : MemLp M1 2 P.μ := by simpa [M1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq (S.μ₁_val_comp_eq_stageOneReg).symm exact hM1_L2.integrable (by norm_num) have hM1_meas : Measurable M1 := by have hs1 := S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩ have hd0 := S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩ have hs0 := S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩ exact S.μ₁_meas.comp (hs1.prod (hd0.prod hs0)) 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 _) hY_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I1, Y, mul_comm])) have hI1Yf_int : Integrable (fun ω => I1 ω * Yf ω) P.μ := by have h := (S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_mul_indicator (S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _) hYf_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I1, Yf, 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 hI0I1Y_int : Integrable (fun ω => I0 ω * (I1 ω * Y ω)) P.μ := by have hmeas : Measurable (fun ω => I1 ω * Y ω) := ((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator (S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)).mul (by simpa [Y] using S.toPODTRSystem.measurable_Y_of S.dbar) have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hI1Y_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, I1, Y, mul_comm, mul_left_comm])) have hI0I1Yf_int : Integrable (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ := by have hmeas : Measurable (fun ω => I1 ω * Yf ω) := ((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator (S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)).mul (by simpa [Yf] using S.toPODTRSystem.measurable_factualY) have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hI1Yf_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, I1, Yf, mul_comm, mul_left_comm])) have hI0I1M1_int : Integrable (fun ω => I0 ω * (I1 ω * M1 ω)) P.μ := by have hmeas : Measurable (fun ω => I1 ω * M1 ω) := ((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator (S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)).mul hM1_meas have h := (S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_mul_indicator (S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _) hI1M1_int exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I0, I1, M1, mul_comm])) have hres_eq : (fun ω => I0 ω * (I1 ω * (Yf ω - M1 ω))) = (fun ω => I0 ω * (I1 ω * Yf ω) - I0 ω * (I1 ω * M1 ω)) := by funext ω ring have hsub : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω) - I0 ω * (I1 ω * M1 ω)) P.μ =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ - B1.condExpGiven (fun ω => I0 ω * (I1 ω * M1 ω)) P.μ := by simp only [POCFBundle.condExpGiven] exact MeasureTheory.condExp_sub hI0I1Yf_int hI0I1M1_int B1.sigma have hConsistency : (fun ω => Yf ω * S.toPODTRSystem.indD S.dbar 2 ω) = (fun ω => Y ω * S.toPODTRSystem.indD S.dbar 2 ω) := by have h := POVar.factual_mul_indicator_eq_cf_mul_indicator hA.consistency S.toPODTRSystem.yVar (S.toPODTRSystem.regime S.dbar) (S.toPODTRSystem.yVar_notMem_regime S.dbar) {ω | ∀ i : Fin 2, S.toPODTRSystem.factualD i ω = S.dbar i} (S.toPODTRSystem.factualAgrees_regime S.dbar) have hrewrite : S.toPODTRSystem.indD S.dbar 2 = ({ω | ∀ i : Fin 2, S.toPODTRSystem.factualD i ω = S.dbar i}).indicator (fun _ => (1 : ℝ)) := by have h0 := S.toPODTRSystem.indD_eq_indicator_event S.dbar 2 (le_refl 2) have h_set_eq : ({ω | ∀ i : Fin 2, i.val < 2 → S.toPODTRSystem.factualD i ω = S.dbar i}) = {ω | ∀ i : Fin 2, S.toPODTRSystem.factualD i ω = S.dbar i} := by ext ω refine ⟨fun hω i => hω i i.isLt, fun hω i _ => hω i⟩ rw [h0, h_set_eq] change (fun ω => S.toPODTRSystem.factualY ω * S.toPODTRSystem.indD S.dbar 2 ω) = (fun ω => S.toPODTRSystem.Y_of S.dbar ω * S.toPODTRSystem.indD S.dbar 2 ω) rw [hrewrite] exact h have hIndD2_factor : S.toPODTRSystem.indD S.dbar 2 = fun ω => I0 ω * I1 ω := by funext ω have hsplit1 := congr_fun (S.toPODTRSystem.indD_factor_split S.dbar 1 (by decide)) ω have hsplit0 := congr_fun (S.toPODTRSystem.indD_factor_split S.dbar 0 (by decide)) ω rw [hsplit1, hsplit0] have hzero : S.toPODTRSystem.indD S.dbar 0 ω = 1 := rfl rw [hzero] ring have hFact_to_cf : (fun ω => I0 ω * (I1 ω * Yf ω)) =ᵐ[P.μ] (fun ω => I0 ω * (I1 ω * Y ω)) := by exact Filter.Eventually.of_forall (fun ω => by have hc := congr_fun hConsistency ω rw [hIndD2_factor] at hc change Yf ω * (I0 ω * I1 ω) = Y ω * (I0 ω * I1 ω) at hc nlinarith [hc]) have hCE_fact_to_cf : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ =ᵐ[P.μ] B1.condExpGiven (fun ω => I0 ω * (I1 ω * Y ω)) P.μ := B1.condExpGiven_congr_ae hFact_to_cf have hI0_sm_B1 : StronglyMeasurable[B1.sigma] I0 := by simpa [B1, I0] using S.toPODTRSystem.stronglyMeasurable_indicator_dVar_sigma_history 1 (by decide) ⟨0, by decide⟩ (by decide) (S.dbar ⟨0, by decide⟩) have hM1_sm_B1 : StronglyMeasurable[B1.sigma] M1 := by have hs1 : Measurable[B1.sigma] (S.toPODTRSystem.factualS ⟨1, by decide⟩) := S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide) ⟨1, by decide⟩ (by decide) have hd0 : Measurable[B1.sigma] (S.toPODTRSystem.factualD ⟨0, by decide⟩) := S.toPODTRSystem.measurable_factualD_sigma_history 1 (by decide) ⟨0, by decide⟩ (by decide) have hs0 : Measurable[B1.sigma] (S.toPODTRSystem.factualS ⟨0, by decide⟩) := S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide) ⟨0, by decide⟩ (by decide) exact (S.μ₁_meas.comp (hs1.prod (hd0.prod hs0))).stronglyMeasurable have hI0M1_sm_B1 : StronglyMeasurable[B1.sigma] (fun ω => I0 ω * M1 ω) := hI0_sm_B1.mul hM1_sm_B1 have hcfY_n : (S.toPODTRSystem.cfYBundle S.dbar).n = 1 := rfl let i0 : Fin (S.toPODTRSystem.cfYBundle S.dbar).n := ⟨0, by rw [hcfY_n]; exact Nat.one_pos⟩ let ψ : (∀ i : Fin (S.toPODTRSystem.cfYBundle S.dbar).n, (S.toPODTRSystem.cfYBundle S.dbar).type i) → ℝ := fun f => (f i0 : ℝ) have hψ_meas : Measurable ψ := by change Measurable (fun f : (∀ i, (S.toPODTRSystem.cfYBundle S.dbar).type i) => (f i0 : ℝ)) exact measurable_pi_apply i0 have hYof_eq_proj : S.toPODTRSystem.Y_of S.dbar = ψ ∘ (S.toPODTRSystem.cfYBundle S.dbar).jointValue := by funext ω rfl have hCI : CondIndepFun B1.sigma B1.sigma_le (S.toPODTRSystem.factualD ⟨1, by decide⟩) Y P.μ := by have hproj := (hA.exch S.dbar ⟨1, by decide⟩).project (ψ := ψ) hψ_meas change CondIndepFun B1.sigma B1.sigma_le (S.toPODTRSystem.factualD ⟨1, by decide⟩) (S.toPODTRSystem.Y_of S.dbar) P.μ rw [hYof_eq_proj] exact hproj let u : δ → ℝ := ({S.dbar ⟨1, by decide⟩} : Set δ).indicator (fun _ => (1 : ℝ)) have hu_meas : Measurable u := measurable_const.indicator (MeasurableSet.singleton _) have hu_eq : (fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω)) = I1 := by funext ω by_cases h : S.toPODTRSystem.factualD ⟨1, by decide⟩ ω = S.dbar ⟨1, by decide⟩ · have h1 : S.toPODTRSystem.factualD ⟨1, by decide⟩ ω ∈ ({S.dbar ⟨1, by decide⟩} : Set δ) := h have h2 : ω ∈ (S.toPODTRSystem.dVar ⟨1, by decide⟩).event (S.dbar ⟨1, by decide⟩) := h rw [show u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) = (1 : ℝ) from Set.indicator_of_mem h1 _, show I1 ω = (1 : ℝ) from by simpa [I1] using (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_one h2] · have h1 : S.toPODTRSystem.factualD ⟨1, by decide⟩ ω ∉ ({S.dbar ⟨1, by decide⟩} : Set δ) := h have h2 : ω ∉ (S.toPODTRSystem.dVar ⟨1, by decide⟩).event (S.dbar ⟨1, by decide⟩) := h rw [show u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) = (0 : ℝ) from Set.indicator_of_notMem h1 _, show I1 ω = (0 : ℝ) from by simpa [I1] using (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator_apply_eq_zero h2] have hfact : P.μ[fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) * Y ω | B1.sigma] =ᵐ[P.μ] P.μ[fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) | B1.sigma] * P.μ[Y | B1.sigma] := condExp_mul_of_condIndep (μ := P.μ) (m := B1.sigma) B1.sigma_le (f := S.toPODTRSystem.factualD ⟨1, by decide⟩) (g := Y) (S.toPODTRSystem.measurable_factualD ⟨1, by decide⟩) (by simpa [Y] using S.toPODTRSystem.measurable_Y_of S.dbar) hCI (u := u) (v := id) hu_meas measurable_id (by rw [hu_eq]; exact hI1_int) hY_int (by have heq : (fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) * Y ω) = (fun ω => I1 ω * Y ω) := by funext ω rw [congr_fun hu_eq ω] change Integrable -- … truncated; follow the source link for the rest … -
theta_zero_factualS₀_integrallemma — The DTR estimand θ₀ = E[Y(dbar)] lifts to an integral against P.μ: under DTR backdoor assumptions, θ₀ = ∫ ω, μ₀_val(factualS 0 ω) ∂P.μ, since μ₀_val ∘ factualS 0 is the σ(historyBundle 0)-conditional expectation of Y_of dbar and P.μ is a probability measure.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.AssumptionsconclusionS.θ₀ = ∫ ω, S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μProof (Lean source)
lemma theta_zero_factualS₀_integral (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) : S.θ₀ = ∫ ω, S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ := by unfold DTREstimationSystem.θ₀ dtrEffect calc ∫ ω, S.toPODTRSystem.Y_of S.dbar ω ∂P.μ = ∫ ω, (S.toPODTRSystem.historyBundle 0 (by decide)).condExpGiven (S.toPODTRSystem.Y_of S.dbar) P.μ ω ∂P.μ := by exact (MeasureTheory.integral_condExp (S.toPODTRSystem.historyBundle 0 (by decide)).sigma_le).symm _ = ∫ ω, S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ := MeasureTheory.integral_congr_ae (S.μ₀_compat hA)
RemainderBound 3 core · 0 supporting Bounds the sequential doubly robust second-order remainder for a two-stage dynamic-treatment-regime problem. ★ seqDR_remainder_bound★ seqDR_remainder_op
Bounds the sequential doubly robust second-order remainder for a two-stage
dynamic-treatment-regime problem. The constants track overlap and stagewise
nuisance errors in the DTR product-rate condition. The main declarations are
seqDR_rem_const, seqDR_remainder_bound, and the random-nuisance
stochastic-order corollary seqDR_remainder_op.
def seqDR_rem_const reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Sequential DR (DTR, n = 2) remainder constant for strict overlap ε.
Definition (Lean source)
noncomputable def seqDR_rem_const (ε : ℝ) : ℝ := 2 / (ε ^ 2 * (1 - ε))
theorem seqDR_remainder_bound reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Sequential DR (DTR, n = 2) remainder bound. Consider a two-stage dynamic treatment-regime estimation system satisfying the sequential causal assumptions, 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 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 absolute value of the population sequential doubly robust moment at η and the true target θ₀ is at most an explicit O(ε⁻²) constant times the sum of the two stagewise outcome-regression L² errors, times the sum of the two stagewise propensity L² errors.
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)|
≤ seqDR_rem_const ε * ((eLpNorm (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal + (eLpNorm (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) * ((eLpNorm (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal + (eLpNorm (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
Proof (Lean source)
theorem seqDR_remainder_bound
(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)|
≤ seqDR_rem_const ε *
((eLpNorm (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) *
((eLpNorm (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) := by
let dμ0 : γ 0 → ℝ := fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀
let de0 : γ 0 → ℝ := fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀
let dμ1 : γ 1 × δ × γ 0 → ℝ := fun h => η.μ₁_fn h - S.μ₁_val h
let de1 : γ 1 × δ × γ 0 → ℝ := fun h => η.e₁_fn h - S.e₁_val h
let rem0 : γ 0 → ℝ := fun s₀ => de0 s₀ * (1 / η.e₀_fn s₀) * dμ0 s₀
let rem1 : γ 1 × δ × γ 0 → ℝ := fun h =>
indEq h.2.1 (S.dbar 0) * de1 h * (1 / (η.e₀_fn h.2.2 * η.e₁_fn h)) * dμ1 h
have hC_ge_inv0 : ε⁻¹ ≤ seqDR_rem_const ε := by
unfold seqDR_rem_const
have hpos : 0 < ε := h_overlap.1
have hone : 0 < 1 - ε := by linarith [h_overlap.2.1]
have hden : 0 < ε ^ 2 * (1 - ε) := mul_pos (sq_pos_of_pos hpos) hone
rw [div_eq_mul_inv]
field_simp [hpos.ne', hden.ne']
nlinarith [h_overlap.2.1]
have hC_ge_inv1 : (ε * ε)⁻¹ ≤ seqDR_rem_const ε := by
unfold seqDR_rem_const
have hpos : 0 < ε := h_overlap.1
have hone : 0 < 1 - ε := by linarith [h_overlap.2.1]
have hεε : 0 < ε * ε := mul_pos hpos hpos
have hden : 0 < ε ^ 2 * (1 - ε) := mul_pos (sq_pos_of_pos hpos) hone
rw [div_eq_mul_inv]
field_simp [hpos.ne', hεε.ne', hden.ne']
nlinarith [h_overlap.2.1]
have hC_nonneg : 0 ≤ seqDR_rem_const ε :=
(inv_nonneg.mpr (mul_nonneg h_overlap.1.le h_overlap.1.le)).trans hC_ge_inv1
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 hpoint0 : ∀ s₀, |rem0 s₀| ≤ seqDR_rem_const ε * |dμ0 s₀ * de0 s₀| := by
intro s₀
have hinv : |(η.e₀_fn s₀)⁻¹| ≤ seqDR_rem_const ε := by
have hle : (η.e₀_fn s₀)⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ (hη0_pos s₀) h_overlap.1).2 (hη0_lower s₀)
rw [abs_of_pos (inv_pos.mpr (hη0_pos s₀))]
exact hle.trans hC_ge_inv0
calc
|rem0 s₀| = |dμ0 s₀ * de0 s₀| * |(η.e₀_fn s₀)⁻¹| := by
simp [rem0, div_eq_mul_inv, abs_mul, mul_left_comm, mul_comm]
_ ≤ |dμ0 s₀ * de0 s₀| * seqDR_rem_const ε :=
mul_le_mul_of_nonneg_left hinv (abs_nonneg _)
_ = seqDR_rem_const ε * |dμ0 s₀ * de0 s₀| := by ring
have hpoint1 : ∀ h, |rem1 h| ≤ seqDR_rem_const ε * |dμ1 h * de1 h| := by
intro h
have hpos0 : 0 < η.e₀_fn h.2.2 := hη0_pos h.2.2
have hpos1 : 0 < η.e₁_fn h := hη1_pos h
have hprod_pos : 0 < η.e₀_fn h.2.2 * η.e₁_fn h := mul_pos hpos0 hpos1
have hεprod : ε * ε ≤ η.e₀_fn h.2.2 * η.e₁_fn h :=
mul_le_mul (hη0_lower h.2.2) (hη1_lower h) h_overlap.1.le
(le_trans h_overlap.1.le (hη0_lower h.2.2))
have hinv : |(η.e₀_fn h.2.2 * η.e₁_fn h)⁻¹| ≤ seqDR_rem_const ε := by
have hle : (η.e₀_fn h.2.2 * η.e₁_fn h)⁻¹ ≤ (ε * ε)⁻¹ :=
(inv_le_inv₀ hprod_pos (mul_pos h_overlap.1 h_overlap.1)).2 hεprod
rw [abs_of_pos (inv_pos.mpr hprod_pos)]
exact hle.trans hC_ge_inv1
have hind : |indEq h.2.1 (S.dbar 0)| ≤ 1 := by
unfold indEq
split <;> simp
calc
|rem1 h| =
|indEq h.2.1 (S.dbar 0)| *
|dμ1 h * de1 h| * |(η.e₀_fn h.2.2 * η.e₁_fn h)⁻¹| := by
simp [rem1, div_eq_mul_inv, abs_mul, mul_assoc, mul_left_comm, mul_comm]
_ ≤ 1 * |dμ1 h * de1 h| * seqDR_rem_const ε := by
exact mul_le_mul
(mul_le_mul hind le_rfl (abs_nonneg _) zero_le_one)
hinv (abs_nonneg _) (mul_nonneg zero_le_one (abs_nonneg _))
_ = seqDR_rem_const ε * |dμ1 h * de1 h| := by ring
haveI : ENNReal.HolderTriple (2 : ENNReal) (2 : ENNReal) (1 : ENNReal) := by
constructor
simpa using ENNReal.inv_two_add_inv_two
haveI : IsFiniteMeasure S.P_H₀ := by
unfold DTREstimationSystem.P_H₀
infer_instance
haveI : IsFiniteMeasure S.P_H₁ := by
unfold DTREstimationSystem.P_H₁
infer_instance
have hprod0_int : Integrable (fun s₀ => dμ0 s₀ * de0 s₀) S.P_H₀ := by
have hmul : MemLp (fun s₀ => dμ0 s₀ * de0 s₀) 1 S.P_H₀ :=
hΔe₀_memLp.mul hΔμ₀_memLp
exact hmul.integrable (by norm_num)
have hprod1_int : Integrable (fun h => dμ1 h * de1 h) S.P_H₁ := by
have hmul : MemLp (fun h => dμ1 h * de1 h) 1 S.P_H₁ :=
hΔe₁_memLp.mul hΔμ₁_memLp
exact hmul.integrable (by norm_num)
have hbound0_int :
Integrable (fun s₀ => seqDR_rem_const ε * |dμ0 s₀ * de0 s₀|) S.P_H₀ :=
hprod0_int.norm.const_mul (seqDR_rem_const ε)
have hbound1_int :
Integrable (fun h => seqDR_rem_const ε * |dμ1 h * de1 h|) S.P_H₁ :=
hprod1_int.norm.const_mul (seqDR_rem_const ε)
have hrem0_meas : Measurable rem0 := by
dsimp [rem0, dμ0, de0]
exact (((η.e₀_meas.sub S.e₀_meas).mul
((measurable_const.div η.e₀_meas))).mul
((η.μ₀_meas.sub S.μ₀_meas)))
have hrem1_meas : Measurable rem1 := by
have hind : Measurable (fun h : γ 1 × δ × γ 0 => indEq h.2.1 (S.dbar 0)) := by
have hset : MeasurableSet {x : δ | x = S.dbar 0} := MeasurableSet.singleton _
have hbase : Measurable (indicator {x : δ | x = S.dbar 0} (fun _ => (1 : ℝ))) :=
measurable_const.indicator hset
have heq : (fun x : δ => indEq x (S.dbar 0)) =
indicator {x : δ | x = S.dbar 0} (fun _ => (1 : ℝ)) := by
funext x
unfold indEq
by_cases hx : x = S.dbar 0 <;> simp [hx]
exact (heq ▸ hbase).comp measurable_snd.fst
dsimp [rem1, dμ1, de1]
exact (((hind.mul (η.e₁_meas.sub S.e₁_meas)).mul
((measurable_const.div ((η.e₀_meas.comp measurable_snd.snd).mul η.e₁_meas)))).mul
(η.μ₁_meas.sub S.μ₁_meas))
have hrem0_abs_int : Integrable (fun s₀ => |rem0 s₀|) S.P_H₀ :=
hbound0_int.mono'
(continuous_abs.measurable.comp hrem0_meas).aestronglyMeasurable
(Filter.Eventually.of_forall fun s₀ => by
simpa [Real.norm_eq_abs] using hpoint0 s₀)
have hrem1_abs_int : Integrable (fun h => |rem1 h|) S.P_H₁ :=
hbound1_int.mono'
(continuous_abs.measurable.comp hrem1_meas).aestronglyMeasurable
(Filter.Eventually.of_forall fun h => by
simpa [Real.norm_eq_abs] using hpoint1 h)
have hCS0 :
∫ s₀, |dμ0 s₀ * de0 s₀| ∂(S.P_H₀)
≤ (eLpNorm dμ0 2 S.P_H₀).toReal * (eLpNorm de0 2 S.P_H₀).toReal := by
simpa [dμ0, de0] using
integral_abs_mul_le_eLpNorm_mul_eLpNorm
(ν := S.P_H₀) hΔμ₀_memLp hΔe₀_memLp
have hCS1 :
∫ h, |dμ1 h * de1 h| ∂(S.P_H₁)
≤ (eLpNorm dμ1 2 S.P_H₁).toReal * (eLpNorm de1 2 S.P_H₁).toReal := by
simpa [dμ1, de1] using
integral_abs_mul_le_eLpNorm_mul_eLpNorm
(ν := S.P_H₁) hΔμ₁_memLp hΔe₁_memLp
have hident := seqDR_remainder_identity S h_overlap hA h_y2 h_yd2 η hη
hΔμ₀_memLp hΔμ₁_memLp hΔe₀_memLp hΔe₁_memLp
calc
|∫ z, S.seqDRMomentFunctional η z S.θ₀ ∂(S.P_Z)|
= |∫ s₀, rem0 s₀ ∂(S.P_H₀) + ∫ h, rem1 h ∂(S.P_H₁)| := by
rw [hident]
_ ≤ |∫ s₀, rem0 s₀ ∂(S.P_H₀)| + |∫ h, rem1 h ∂(S.P_H₁)| :=
abs_add_le _ _
_ ≤ ∫ s₀, |rem0 s₀| ∂(S.P_H₀) + ∫ h, |rem1 h| ∂(S.P_H₁) :=
add_le_add MeasureTheory.abs_integral_le_integral_abs
MeasureTheory.abs_integral_le_integral_abs
_ ≤ ∫ s₀, seqDR_rem_const ε * |dμ0 s₀ * de0 s₀| ∂(S.P_H₀) +
∫ h, seqDR_rem_const ε * |dμ1 h * de1 h| ∂(S.P_H₁) := by
exact add_le_add
(integral_mono_ae hrem0_abs_int hbound0_int
(Filter.Eventually.of_forall hpoint0))
(integral_mono_ae hrem1_abs_int hbound1_int
(Filter.Eventually.of_forall hpoint1))
_ = seqDR_rem_const ε * (∫ s₀, |dμ0 s₀ * de0 s₀| ∂(S.P_H₀)) +
seqDR_rem_const ε * (∫ h, |dμ1 h * de1 h| ∂(S.P_H₁)) := by
rw [integral_const_mul, integral_const_mul]
_ ≤ seqDR_rem_const ε *
((eLpNorm dμ0 2 S.P_H₀).toReal * (eLpNorm de0 2 S.P_H₀).toReal) +
seqDR_rem_const ε *
((eLpNorm dμ1 2 S.P_H₁).toReal * (eLpNorm de1 2 S.P_H₁).toReal) := by
exact add_le_add
(mul_le_mul_of_nonneg_left hCS0 hC_nonneg)
(mul_le_mul_of_nonneg_left hCS1 hC_nonneg)
_ ≤ seqDR_rem_const ε *
((eLpNorm dμ0 2 S.P_H₀).toReal + (eLpNorm dμ1 2 S.P_H₁).toReal) *
((eLpNorm de0 2 S.P_H₀).toReal + (eLpNorm de1 2 S.P_H₁).toReal) := by
have hμ0 : 0 ≤ (eLpNorm dμ0 2 S.P_H₀).toReal := ENNReal.toReal_nonneg
have hμ1 : 0 ≤ (eLpNorm dμ1 2 S.P_H₁).toReal := ENNReal.toReal_nonneg
have he0 : 0 ≤ (eLpNorm de0 2 S.P_H₀).toReal := ENNReal.toReal_nonneg
have he1 : 0 ≤ (eLpNorm de1 2 S.P_H₁).toReal := ENNReal.toReal_nonneg
nlinarith [mul_nonneg hμ0 he1, mul_nonneg hμ1 he0]
_ = seqDR_rem_const ε *
((eLpNorm (fun s₀ => η.μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h => η.μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) *
((eLpNorm (fun s₀ => η.e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h => η.e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) := by
simp [dμ0, de0, dμ1, de1]
theorem seqDR_remainder_op reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Sequential DR remainder is o_p(n^{-1/2}) under the two-stage product rate. Consider a two-stage dynamic treatment-regime estimation system satisfying the sequential causal assumptions, 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. Let η̂ₙ be a sequence of sample-size-indexed, possibly random, candidate nuisance vectors that always land in the strict-overlap band, for every sample size and every outcome of the underlying randomness, with stage-0 outcome-regression error, stage-1 outcome-regression error, stage-0 propensity error, and stage-1 propensity error each square-integrable against the corresponding stage's history law at every sample size and outcome. If the four stagewise L² products of outcome-regression and propensity error — own-stage at stage 0, own-stage at stage 1, stage-0 outcome-regression with stage-1 propensity, and stage-1 outcome-regression with stage-0 propensity — are each o_p(n^{-1/2}), then the population sequential doubly robust moment evaluated at the random nuisance η̂ₙ is itself o_p(n^{-1/2}).
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.μ
η_hat :
ℕ → P.Ω → DTRNuisanceVec₂ δ γ
h_in_H :
∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε
hΔμ₀_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀
hΔμ₁_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁
hΔe₀_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀
hΔe₁_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁
h_product_rate_00 :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal * (eLpNorm (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_11 :
IsLittleOp (fun n ω => (eLpNorm (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal * (eLpNorm (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_01 :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal * (eLpNorm (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
h_product_rate_10 :
IsLittleOp (fun n ω => (eLpNorm (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal * (eLpNorm (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
conclusion
IsLittleOp (fun n ω => ∫ z, S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
Proof (Lean source)
theorem seqDR_remainder_op
(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.μ)
(η_hat : ℕ → P.Ω → DTRNuisanceVec₂ δ γ)
(h_in_H : ∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε)
(hΔμ₀_memLp :
∀ n ω, MemLp
(fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀)
(hΔμ₁_memLp :
∀ n ω, MemLp
(fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁)
(hΔe₀_memLp :
∀ n ω, MemLp
(fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀)
(hΔe₁_memLp :
∀ n ω, MemLp
(fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁)
(h_product_rate_00 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ =>
(η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun s₀ =>
(η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_11 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h =>
(η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun h =>
(η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_01 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ =>
(η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun h =>
(η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(h_product_rate_10 :
IsLittleOp
(fun n ω =>
(eLpNorm (fun h =>
(η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun s₀ =>
(η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal)
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) :
IsLittleOp
(fun n ω => ∫ z, S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ := by
let rn : ℕ → ℝ := fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))
let prod00 : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun s₀ =>
(η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun s₀ =>
(η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal
let prod11 : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun h =>
(η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun h =>
(η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal
let prod01 : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun s₀ =>
(η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal *
(eLpNorm (fun h =>
(η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal
let prod10 : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun h =>
(η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal *
(eLpNorm (fun s₀ =>
(η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal
let sumProd : ℕ → P.Ω → ℝ := fun n ω =>
prod00 n ω + prod11 n ω + prod01 n ω + prod10 n ω
have hrn_nonneg : ∀ᶠ n : ℕ in atTop, 0 ≤ rn n := by
filter_upwards with n
exact Real.rpow_nonneg (Nat.cast_nonneg n) _
have hsum_rate :
IsLittleOp sumProd rn P.μ := by
have h0011 :
IsLittleOp (fun n ω => prod00 n ω + prod11 n ω) rn P.μ := by
simpa [prod00, prod11, rn] using
IsLittleOp.add_eventually_nonneg_rate (μ := P.μ) hrn_nonneg
h_product_rate_00 h_product_rate_11
have h0110 :
IsLittleOp (fun n ω => prod01 n ω + prod10 n ω) rn P.μ := by
simpa [prod01, prod10, rn] using
IsLittleOp.add_eventually_nonneg_rate (μ := P.μ) hrn_nonneg
h_product_rate_01 h_product_rate_10
simpa [sumProd, add_assoc] using
IsLittleOp.add_eventually_nonneg_rate (μ := P.μ) hrn_nonneg h0011 h0110
have hCpos : 0 < seqDR_rem_const ε := by
unfold seqDR_rem_const
have h1 : 0 < 1 - ε := by linarith [h_overlap.2.1]
have hden_pos : 0 < ε ^ 2 * (1 - ε) := mul_pos (sq_pos_of_pos h_overlap.1) h1
positivity
refine IsLittleOp.of_abs_le_const_mul (μ := P.μ) hCpos hsum_rate ?_
intro n ω
have hsum_nonneg : 0 ≤ sumProd n ω := by
have h00 : 0 ≤ prod00 n ω := by
dsimp [prod00]
exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
have h11 : 0 ≤ prod11 n ω := by
dsimp [prod11]
exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
have h01 : 0 ≤ prod01 n ω := by
dsimp [prod01]
exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
have h10 : 0 ≤ prod10 n ω := by
dsimp [prod10]
exact mul_nonneg ENNReal.toReal_nonneg ENNReal.toReal_nonneg
dsimp [sumProd]
positivity
have hbound := seqDR_remainder_bound S h_overlap hA h_y2 h_yd2
(η_hat n ω) (h_in_H n ω) (hΔμ₀_memLp n ω) (hΔμ₁_memLp n ω)
(hΔe₀_memLp n ω) (hΔe₁_memLp n ω)
have habs_sum : |sumProd n ω| = sumProd n ω := abs_of_nonneg hsum_nonneg
calc
|∫ z, S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)|
≤ seqDR_rem_const ε * sumProd n ω := by
have hrhs :
seqDR_rem_const ε *
((eLpNorm (fun s₀ =>
(η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h =>
(η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) *
((eLpNorm (fun s₀ =>
(η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal
+ (eLpNorm (fun h =>
(η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal)
= seqDR_rem_const ε * sumProd n ω := by
dsimp [sumProd, prod00, prod11, prod01, prod10]
ring
exact hbound.trans_eq hrhs
_ = seqDR_rem_const ε * |sumProd n ω| :=
congrArg (fun x => seqDR_rem_const ε * x) habs_sum.symm
ScorePullout 4 core · 0 supporting This module proves the conditioning identities that collapse the weighted residual and treatment-indicator terms in the sequential doubly robust DTR score. ★ weighted_residual_integral_zero_stage0★ indicator_to_propScore_integral_stage0★ weighted_residual_integral_zero_stage1★ indicator_to_propScore_integral_stage1
Score pull-out identities for two-stage DTR scores
This module proves the conditioning identities that collapse the weighted
residual and treatment-indicator terms in the sequential doubly robust DTR
score. The stage-0 results
DTREstimationSystem.weighted_residual_integral_zero_stage0 and
DTREstimationSystem.indicator_to_propScore_integral_stage0 condition on the
initial history S₀; the stage-1 results
DTREstimationSystem.weighted_residual_integral_zero_stage1 and
DTREstimationSystem.indicator_to_propScore_integral_stage1 condition on the
history (S₁, D₀, S₀).
These lemmas move treatment indicators, history sigma-algebras, and regression residuals into forms suitable for the DTR mean-zero and remainder proofs.
theorem weighted_residual_integral_zero_stage0 reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Stage-0 weighted-residual integral vanishes. Let S be a two-stage dynamic-treatment-regime estimation system with strict overlap at level ε, satisfying the system's core identification assumptions (consistency, sequential exchangeability, positivity), and in which the observed outcome has finite second moment. For any weight function g on the stage-0 history that is measurable and for which the product g(S₀) · 1{D₀ = dbar 0} · (μ₁_val(S₁,D₀,S₀) − μ₀_val(S₀)) is integrable, then its expectation under P.μ is zero: the stage-0-weighted, treatment-indicator-gated gap between the stage-1 and stage-0 regression functions has zero mean.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPODTRSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
g :
γ 0 → ℝ
hg_meas :
h_int :
Integrable (fun ω => g (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.μ
conclusion
∫ ω, g (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.μ
= 0
Proof (Lean source)
theorem weighted_residual_integral_zero_stage0
(S : DTREstimationSystem P δ γ)
{ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(hA : S.toPODTRSystem.Assumptions)
(h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ)
(g : γ 0 → ℝ) (hg_meas : Measurable g)
(h_int : Integrable
(fun ω => g (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.μ) :
∫ ω, g (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.μ = 0 := by
let B0 := S.toPODTRSystem.historyBundle 0 (by decide)
let I0 : P.Ω → ℝ :=
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩)
let M0 : P.Ω → ℝ :=
fun ω => S.μ₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)
let M1 : P.Ω → ℝ :=
fun ω => S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)
let R : P.Ω → ℝ := fun ω => I0 ω * (M1 ω - M0 ω)
have hg_sm : StronglyMeasurable[B0.sigma]
(fun ω => g (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by
have hs0 : Measurable[B0.sigma]
(S.toPODTRSystem.factualS ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 0 (by decide)
⟨0, by decide⟩ (by decide)
exact (hg_meas.comp hs0).stronglyMeasurable
have hM0_int : Integrable M0 P.μ := by
exact (B0.integrable_condExpGiven (S.toPODTRSystem.Y_of S.dbar)).congr
(by simpa [B0, M0] 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] 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 :=
S.μ₀_meas.comp (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)
have hM1_meas : Measurable M1 := by
have hs1 := S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩
have hd0 := S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩
have hs0 := S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩
exact S.μ₁_meas.comp (hs1.prod (hd0.prod hs0))
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 hR_int : Integrable R P.μ := by
have hsub := hI0M1_int.sub hI0M0_int
refine hsub.congr ?_
exact Filter.Eventually.of_forall (fun ω => by
simp [R]
ring)
have hcondexp_pull :=
B0.condExpGiven_mul_of_stronglyMeasurable_left
(f := fun ω => g (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))
(g := R) hg_sm
(by
exact h_int.congr (Filter.Eventually.of_forall (fun ω => by
simp [R, I0, M0, M1])))
hR_int
have h_residual_ce_zero :
B0.condExpGiven R P.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
simpa [B0, R, I0, M0, M1] using
cond_exp_residual_zero_stage0 S h_overlap hA h_y2
have hgresid_ce_zero :
B0.condExpGiven
(fun ω => g (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * R ω) P.μ
=ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
refine hcondexp_pull.trans ?_
filter_upwards [h_residual_ce_zero] with ω hω
rw [Pi.mul_apply, hω, mul_zero]
calc
∫ ω, g (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.μ
= ∫ ω, g (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * R ω ∂P.μ := by
rfl
_ = ∫ ω, B0.condExpGiven
(fun ω => g (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * R ω) P.μ ω
∂P.μ := by
exact (MeasureTheory.integral_condExp B0.sigma_le).symm
_ = ∫ _, (0 : ℝ) ∂P.μ :=
MeasureTheory.integral_congr_ae hgresid_ce_zero
_ = 0 := MeasureTheory.integral_zero _ _
theorem indicator_to_propScore_integral_stage0 reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Stage-0 indicator-to-propensity rewrite. Let S be a two-stage dynamic-treatment-regime estimation system and let f be a real-valued function of the stage-0 history that is measurable and for which the product f(S₀) · 1{D₀ = dbar 0} is integrable. Then the expectation of f(S₀) times the indicator of following the target stage-0 treatment dbar 0 equals the expectation of f(S₀) times the true stage-0 propensity score e₀_val(S₀).
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
f :
γ 0 → ℝ
hf_meas :
hf_ind_int :
Integrable (fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω) P.μ
conclusion
∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * (S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω ∂P.μ
= ∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ
Proof (Lean source)
theorem indicator_to_propScore_integral_stage0
(S : DTREstimationSystem P δ γ)
(f : γ 0 → ℝ) (hf_meas : Measurable f)
(hf_ind_int : Integrable
(fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω) P.μ) :
∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω ∂P.μ
= ∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ := by
let B := S.toPODTRSystem.historyBundle 0 (by decide)
have hf_sm : StronglyMeasurable[B.sigma]
(fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by
have hs0 : Measurable[B.sigma]
(S.toPODTRSystem.factualS ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 0 (by decide)
⟨0, by decide⟩ (by decide)
exact (hf_meas.comp hs0).stronglyMeasurable
have hind_int : Integrable
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩)) P.μ :=
(S.toPODTRSystem.dVar ⟨0, by decide⟩).integrable_indicator
(S.dbar ⟨0, by decide⟩) (MeasurableSet.singleton _)
have hCE_pull :=
B.condExpGiven_mul_of_stronglyMeasurable_left
(μ := P.μ) hf_sm hf_ind_int hind_int
have hCE_replace :
B.condExpGiven
(fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω) P.μ
=ᵐ[P.μ]
(fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by
refine hCE_pull.trans ?_
filter_upwards [S.e₀_compat] with ω hω
rw [Pi.mul_apply, hω]
calc
∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω ∂P.μ
= ∫ ω, B.condExpGiven
(fun ω => f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω) P.μ ω ∂P.μ :=
(MeasureTheory.integral_condExp B.sigma_le).symm
_ = ∫ ω, f (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ :=
MeasureTheory.integral_congr_ae hCE_replace
theorem weighted_residual_integral_zero_stage1 reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Stage-1 weighted-residual integral vanishes. Let S be a two-stage dynamic-treatment-regime estimation system with strict overlap at level ε, satisfying the system's core identification assumptions (consistency, sequential exchangeability, positivity), and in which the observed outcome has finite second moment. For any weight function g on the stage-1 history (S₁,D₀,S₀) that is measurable and for which the product g(S₁,D₀,S₀) · 1{D₀ = dbar 0} · 1{D₁ = dbar 1} · (Y − μ₁_val(S₁,D₀,S₀)) is integrable, then its expectation under P.μ is zero: the doubly indicator-gated stage-1 outcome residual, weighted by g, has zero mean.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPODTRSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
g :
γ 1 × δ × γ 0 → ℝ
hg_meas :
h_int :
Integrable (fun ω => g (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * ((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * ((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω * (S.toPODTRSystem.factualY ω - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))))) P.μ
conclusion
∫ ω, g (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * ((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator (S.dbar ⟨0, by decide⟩) ω * ((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω * (S.toPODTRSystem.factualY ω - S.μ₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) ∂P.μ
= 0
Proof (Lean source)
theorem weighted_residual_integral_zero_stage1
(S : DTREstimationSystem P δ γ)
{ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(hA : S.toPODTRSystem.Assumptions)
(h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ)
(g : γ 1 × δ × γ 0 → ℝ) (hg_meas : Measurable g)
(h_int : Integrable
(fun ω => g (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω *
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω *
(S.toPODTRSystem.factualY ω -
S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω))))) P.μ) :
∫ ω, g (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω *
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω *
(S.toPODTRSystem.factualY ω -
S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) ∂P.μ = 0 := by
let B1 := S.toPODTRSystem.historyBundle 1 (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 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 M1 : P.Ω → ℝ := fun ω => S.μ₁_val (H1 ω)
let R : P.Ω → ℝ :=
fun ω => I0 ω * (I1 ω * (S.toPODTRSystem.factualY ω - M1 ω))
have hg_sm : StronglyMeasurable[B1.sigma] (fun ω => g (H1 ω)) := by
have hs1 : Measurable[B1.sigma] (S.toPODTRSystem.factualS ⟨1, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide)
⟨1, by decide⟩ (by decide)
have hd0 : Measurable[B1.sigma] (S.toPODTRSystem.factualD ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualD_sigma_history 1 (by decide)
⟨0, by decide⟩ (by decide)
have hs0 : Measurable[B1.sigma] (S.toPODTRSystem.factualS ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide)
⟨0, by decide⟩ (by decide)
exact (hg_meas.comp (hs1.prod (hd0.prod hs0))).stronglyMeasurable
have hYf_int : Integrable S.toPODTRSystem.factualY P.μ := hA.integrable_factualY
have hM1_int : Integrable M1 P.μ := by
have hM1_L2 : MemLp M1 2 P.μ := by
simpa [H1, M1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq
(S.μ₁_val_comp_eq_stageOneReg).symm
exact hM1_L2.integrable (by norm_num)
have hM1_meas : Measurable M1 := by
have hs1 := S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩
have hd0 := S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩
have hs0 := S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩
exact S.μ₁_meas.comp (hs1.prod (hd0.prod hs0))
have hI1Yf_int : Integrable
(fun ω => I1 ω * S.toPODTRSystem.factualY ω) P.μ := by
have h := (S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_mul_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _) hYf_int
exact h.congr (Filter.Eventually.of_forall (fun ω => by simp [I1, 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 ω * (S.toPODTRSystem.factualY ω - M1 ω)) P.μ := by
have hsub := hI1Yf_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 ω * (S.toPODTRSystem.factualY ω - M1 ω)) :=
((S.toPODTRSystem.dVar ⟨1, by decide⟩).measurable_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)).mul
(S.toPODTRSystem.measurable_factualY.sub hM1_meas)
have hR_int : Integrable R 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
simp [R, I0, I1, M1, mul_comm]))
have hcondexp_pull :=
B1.condExpGiven_mul_of_stronglyMeasurable_left
(f := fun ω => g (H1 ω)) (g := R) hg_sm
(by
exact h_int.congr (Filter.Eventually.of_forall (fun ω => by
simp [R, H1, I0, I1, M1])))
hR_int
have h_residual_ce_zero :
B1.condExpGiven R P.μ =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
simpa [B1, R, H1, I0, I1, M1] using
cond_exp_residual_zero_stage1 S h_overlap hA h_y2
have hgresid_ce_zero :
B1.condExpGiven (fun ω => g (H1 ω) * R ω) P.μ
=ᵐ[P.μ] (fun _ => (0 : ℝ)) := by
refine hcondexp_pull.trans ?_
filter_upwards [h_residual_ce_zero] with ω hω
rw [Pi.mul_apply, hω, mul_zero]
calc
∫ ω, g (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
((S.toPODTRSystem.dVar ⟨0, by decide⟩).indicator
(S.dbar ⟨0, by decide⟩) ω *
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω *
(S.toPODTRSystem.factualY ω -
S.μ₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)))) ∂P.μ
= ∫ ω, g (H1 ω) * R ω ∂P.μ := by
rfl
_ = ∫ ω, B1.condExpGiven (fun ω => g (H1 ω) * R ω) P.μ ω ∂P.μ := by
exact (MeasureTheory.integral_condExp B1.sigma_le).symm
_ = ∫ _, (0 : ℝ) ∂P.μ :=
MeasureTheory.integral_congr_ae hgresid_ce_zero
_ = 0 := MeasureTheory.integral_zero _ _
theorem indicator_to_propScore_integral_stage1 reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Stage-1 indicator-to-propensity rewrite. Let S be a two-stage dynamic-treatment-regime estimation system and let f be a real-valued function of the stage-1 history (S₁,D₀,S₀) that is measurable and for which the product f(S₁,D₀,S₀) · 1{D₁ = dbar 1} is integrable. Then the expectation of f(S₁,D₀,S₀) times the indicator of following the target stage-1 treatment dbar 1 equals the expectation of f(S₁,D₀,S₀) times the true stage-1 propensity score e₁_val(S₁,D₀,S₀).
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
f :
γ 1 × δ × γ 0 → ℝ
hf_meas :
hf_ind_int :
Integrable (fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω) P.μ
conclusion
∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * (S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator (S.dbar ⟨1, by decide⟩) ω ∂P.μ
= ∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * S.e₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ
Proof (Lean source)
theorem indicator_to_propScore_integral_stage1
(S : DTREstimationSystem P δ γ)
(f : γ 1 × δ × γ 0 → ℝ) (hf_meas : Measurable f)
(hf_ind_int : Integrable
(fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω) P.μ) :
∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω ∂P.μ
= ∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ := by
let B := S.toPODTRSystem.historyBundle 1 (by decide)
have hf_sm : StronglyMeasurable[B.sigma]
(fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by
have hs1 : Measurable[B.sigma]
(S.toPODTRSystem.factualS ⟨1, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide)
⟨1, by decide⟩ (by decide)
have hd0 : Measurable[B.sigma]
(S.toPODTRSystem.factualD ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualD_sigma_history 1 (by decide)
⟨0, by decide⟩ (by decide)
have hs0 : Measurable[B.sigma]
(S.toPODTRSystem.factualS ⟨0, by decide⟩) :=
S.toPODTRSystem.measurable_factualS_sigma_history 1 (by decide)
⟨0, by decide⟩ (by decide)
exact (hf_meas.comp (hs1.prod (hd0.prod hs0))).stronglyMeasurable
have hind_int : Integrable
((S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩)) P.μ :=
(S.toPODTRSystem.dVar ⟨1, by decide⟩).integrable_indicator
(S.dbar ⟨1, by decide⟩) (MeasurableSet.singleton _)
have hCE_pull :=
B.condExpGiven_mul_of_stronglyMeasurable_left
(μ := P.μ) hf_sm hf_ind_int hind_int
have hCE_replace :
B.condExpGiven
(fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω) P.μ
=ᵐ[P.μ]
(fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω)) := by
refine hCE_pull.trans ?_
filter_upwards [S.e₁_compat] with ω hω
rw [Pi.mul_apply, hω]
calc
∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω ∂P.μ
= ∫ ω, B.condExpGiven
(fun ω => f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
(S.toPODTRSystem.dVar ⟨1, by decide⟩).indicator
(S.dbar ⟨1, by decide⟩) ω) P.μ ω ∂P.μ :=
(MeasureTheory.integral_condExp B.sigma_le).symm
_ = ∫ ω, f (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) *
S.e₁_val
(S.toPODTRSystem.factualS ⟨1, by decide⟩ ω,
S.toPODTRSystem.factualD ⟨0, by decide⟩ ω,
S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∂P.μ :=
MeasureTheory.integral_congr_ae hCE_replace