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 · 12 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
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the observable stage-1 regression assigns to each sample realization the conditional mean of the outcome multiplied by the indicator of the system's target second-period treatment, divided by the conditional mean of that indicator given the second-period history.
Definition (Lean source)
parameters
def
stageOneReg S :
P.Ω → ℝ
def StrictOverlap reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system and a real number, the strict-overlap condition holds exactly when and, almost surely under the population measure, both conditional probabilities of the system's target treatment at their respective stages lie between ε and , inclusively.
Definition (Lean source)
parameters
def
StrictOverlap S ε :
Prop
given by
clause 1
0 < ε
clause 2
ε ≤ 1 / 2
clause 3
∀ᵐ ω ∂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
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the marginal law of the first-period state is the population distribution induced by that system's factual first-period state.
Definition (Lean source)
parameters
def
given by
P.μ.map (S.toPODTRSystem.factualS ⟨0, by decide⟩)
def P_H₁ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the marginal law of the second-period history is the population distribution of the second-period state, first-period treatment, and first-period state, in that order.
Definition (Lean source)
parameters
def
given by
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
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the factual two-stage data map sends each sample realization to its factual first-period state, first-period treatment, second-period state, second-period treatment, and outcome, in that order.
Definition (Lean source)
parameters
def
factualZ S :
P.Ω → γ 0 × δ × γ 1 × δ × ℝ
given by
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
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the joint law of the factual two-stage data tuple is the population distribution induced by its factual two-stage data map.
Definition (Lean source)
parameters
def
given by
P.μ.map S.factualZ
def θ₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the target regime mean outcome is the potential-outcome dynamic-treatment-regime effect for the treatment regime selected by that system.
Definition (Lean source)
parameters
def
θ₀ S :
ℝ
given by
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
hypotheses
conclusion
S.θ₀ = S.toPODTRSystem.dtrEffect S.dbar
Proof (Lean source)
theorem θ₀_eq_dtrEffect (S : DTREstimationSystem P δ γ) :
S.θ₀ = S.toPODTRSystem.dtrEffect S.dbar := rfl
12 supporting declarations (lemmas, instances)
-
stronglyMeasurable_μ₀_vallemma — The stage-0 outcome regression carried by an estimation system is strongly measurable on the stage-0 state space.hypothesesconclusionStronglyMeasurable S.μ₀_valProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_μ₀_val (S : DTREstimationSystem P δ γ) : StronglyMeasurable S.μ₀_val := S.μ₀_meas.stronglyMeasurable -
stronglyMeasurable_e₀_vallemma — The stage-0 propensity carried by an estimation system is strongly measurable on the stage-0 state space.hypothesesconclusionStronglyMeasurable S.e₀_valProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_e₀_val (S : DTREstimationSystem P δ γ) : StronglyMeasurable S.e₀_val := S.e₀_meas.stronglyMeasurable -
stronglyMeasurable_μ₁_vallemma — The stage-1 outcome regression carried by an estimation system is strongly measurable on the stage-1 history space.hypothesesconclusionStronglyMeasurable S.μ₁_valProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_μ₁_val (S : DTREstimationSystem P δ γ) : StronglyMeasurable S.μ₁_val := S.μ₁_meas.stronglyMeasurable -
stronglyMeasurable_e₁_vallemma — The stage-1 propensity carried by an estimation system is strongly measurable on the stage-1 history space.hypothesesconclusionStronglyMeasurable S.e₁_valProof (Lean source)
@[fun_prop] lemma stronglyMeasurable_e₁_val (S : DTREstimationSystem P δ γ) : StronglyMeasurable S.e₁_val := S.e₁_meas.stronglyMeasurable -
μ₀_compatlemma — The stage-0 value-space regression equals the counterfactual stage-0 regression under identification.hypothesesconclusion(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.hypothesesconclusion(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.hypothesesconclusion(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.hypothesesconclusion(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.hypothesesconclusion(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.hypothesesδ :sharedTypeS :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.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] 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 -
P_Z_eqlemma — The joint two-stage data law is the image of the population measure under the map recording the full observed two-stage data tuple.hypothesesconclusionS.P_Z = P.μ.map S.factualZProof (Lean source)
@[causal_defs_simps] lemma P_Z_eq (S : DTREstimationSystem P δ γ) : S.P_Z = P.μ.map S.factualZ := rfl
SeqDRMoment 16 core · 13 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
For a treatment space and the pair of first- and second-period state spaces, the initial-state projection maps every observed two-stage data tuple to its first-period state.
Definition (Lean source)
parameters
δ :
Type
def
projS₀ :
γ 0 × δ × γ 1 × δ × ℝ → γ 0
given by
fun z => z.1
def projD₀ reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space and the pair of first- and second-period state spaces, the first-treatment projection maps every observed two-stage data tuple to its first-period treatment.
Definition (Lean source)
parameters
δ :
Type
def
projD₀ :
γ 0 × δ × γ 1 × δ × ℝ → δ
given by
fun z => z.2.1
def projS₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space and the pair of first- and second-period state spaces, the second-state projection maps every observed two-stage data tuple to its second-period state.
Definition (Lean source)
parameters
δ :
Type
def
projS₁ :
γ 0 × δ × γ 1 × δ × ℝ → γ 1
given by
fun z => z.2.2.1
def projD₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space and the pair of first- and second-period state spaces, the second-treatment projection maps every observed two-stage data tuple to its second-period treatment.
Definition (Lean source)
parameters
δ :
Type
def
projD₁ :
γ 0 × δ × γ 1 × δ × ℝ → δ
given by
fun z => z.2.2.2.1
def projY reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space and the pair of first- and second-period state spaces, the outcome projection maps every observed two-stage data tuple to its observed outcome.
Definition (Lean source)
parameters
δ :
Type
def
projY :
γ 0 × δ × γ 1 × δ × ℝ → ℝ
given by
fun z => z.2.2.2.2
def histH₁ reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space and the pair of first- and second-period state spaces, given an observed two-stage data tuple, the stage-1 history is its second-period state, first-period treatment, and first-period state, in that order.
def indEq reviewed
⚑ flagged
Causalean.Estimation.DTR
For a treatment space, given two treatment values, the real-valued equality indicator is one when they are equal and zero otherwise.
Definition (Lean source)
parameters
δ :
Type
d d' :
δ
def
indEq d d' :
ℝ
given by
haveI : Decidable (d = d') := Classical.dec _ if d = d' then 1 else 0
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
For a treatment space and the pair of first- and second-period state spaces, given a two-period target treatment regime, an observed two-stage data tuple, a stagewise nuisance vector, and a candidate regime mean, the two-stage sequential doubly robust moment is the baseline regression plus its first-stage and second-stage inverse-propensity-weighted residual corrections, minus the candidate mean.
Definition (Lean source)
parameters
def
seqDRMoment dbar z η θ :
ℝ
def η₀ reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the true stagewise nuisance vector consists of that system's two outcome regressions and two treatment propensities.
Definition (Lean source)
parameters
def
given by
⟨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
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, an observed two-stage data tuple, a stagewise nuisance vector, and a candidate regime mean, the system-specific sequential doubly robust moment is the sequential doubly robust moment for the treatment regime selected by the system.
Definition (Lean source)
parameters
δ :
Type
S :
DTREstimationSystem P δ γ
z :
γ 0 × δ × γ 1 × δ × ℝ
η :
DTRNuisanceVec₂ δ γ
θ :
ℝ
def
seqDRMoment S z η θ :
ℝ
given by
seqDRMoment S.dbar z η θ
def ψ_seqDR reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system and an observed two-stage data tuple, the sequential doubly robust influence function is the system-specific sequential doubly robust moment evaluated at the system's true nuisance vector and target regime mean.
Definition (Lean source)
parameters
def
ψ_seqDR S z :
ℝ
given by
S.seqDRMoment z S.η₀ S.θ₀
def H_ε reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a treatment space and the pair of first- and second-period state spaces, given a real number, the overlap-bounded nuisance set consists exactly of stagewise nuisance vectors for which, at every first-period state and every second-period history, each respective treatment propensity lies between ε and , inclusively.
Definition (Lean source)
parameters
def
given by
{ η | (∀ s, ε ≤ η.e₀_fn s ∧ η.e₀_fn s ≤ 1 - ε) ∧ (∀ h, ε ≤ η.e₁_fn h ∧ η.e₁_fn h ≤ 1 - ε) }
def seqDRMomentFunctional reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
For a population outcome system, a treatment space, and the pair of first- and second-period state spaces, given a two-stage dynamic treatment-regime estimation system, the sequential doubly robust moment functional maps every stagewise nuisance vector, observed two-stage data tuple, and candidate regime mean to the sequential doubly robust moment for the system's target regime.
Definition (Lean source)
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
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
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
13 supporting declarations (lemmas, instances)
-
measurable_indEqlemma — On a treatment space whose one-point sets are measurable, comparing a varying treatment against a fixed reference treatment is a measurable real-valued function of the varying treatment.Proof (Lean source)
@[fun_prop] lemma measurable_indEq (d : δ) : Measurable (fun x : δ => indEq x d) := by have hset : MeasurableSet {x : δ | x = d} := MeasurableSet.singleton d have hfun : (fun x : δ => indEq x d) = indicator {x : δ | x = d} (fun _ => (1 : ℝ)) := by funext x by_cases hx : x = d · rw [Set.indicator_of_mem (by simpa using hx)] simp [indEq, hx] · rw [Set.indicator_of_notMem (by simpa using hx)] simp [indEq, hx] rw [hfun] exact measurable_const.indicator hset -
instZeroinstance — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the zero operation on two-stage dynamic-treatment-regime nuisance vectors sets every stage-specific regression and propensity component to zero.parametersδ :sharedTypeinstancegiven byzero := ⟨fun _=> 0, fun _ => 0, fun _ => 0, fun _ => 0, measurable_const, measurable_const, measurable_const, measurable_const⟩ -
instAddinstance — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the addition operation on two-stage dynamic-treatment-regime nuisance vectors is performed componentwise.parametersδ :sharedTypeinstancegiven byadd η η' := ⟨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 — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the negation operation on two-stage dynamic-treatment-regime nuisance vectors is performed componentwise.parametersδ :sharedTypeinstancegiven byneg η := ⟨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 — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the subtraction operation on two-stage dynamic-treatment-regime nuisance vectors is performed componentwise.parametersδ :sharedTypeinstancegiven bysub η η' := ⟨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 — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the real scalar-multiplication operation on two-stage dynamic-treatment-regime nuisance vectors is performed componentwise.parametersδ :sharedTypeinstancegiven bysmul 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δ :sharedTypeh0μ :∀ 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 — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the additive commutative group structure on two-stage dynamic-treatment-regime nuisance vectors uses the zero vector, componentwise addition, componentwise negation, componentwise subtraction, natural-number scalar multiplication, and integer scalar multiplication, and satisfies the natural-zero rule, the natural-successor rule, the integer-zero rule, the positive-integer-successor rule, the negative-integer-successor rule, subtraction as addition of an inverse, associativity, the left-zero law, the right-zero law, inverse cancellation, and commutativity.parametersδ :sharedTypeinstancegiven byclause 1zero := 0clause 2add := (· + ·)clause 4sub := Sub.subclause 5nsmul := nsmulRecclause 6zsmul := zsmulRecclause 7nsmul_zero η := by rflclause 8nsmul_succ n η := by rflclause 9zsmul_zero' η := by rflclause 10zsmul_succ' n η := by rflclause 11zsmul_neg' n η := by rflclause 12sub_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)clause 13add_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)clause 14zero_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)clause 15add_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)clause 16neg_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)clause 17add_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 — For a measurable treatment-history space with measurable singletons and two measurable stage-specific covariate spaces, the real vector-space structure on two-stage dynamic-treatment-regime nuisance vectors uses componentwise scalar multiplication and satisfies multiplication by one, compatibility of successive scalar multiplications, multiplication of zero vectors, distribution over vector addition, distribution over scalar addition, and multiplication by the zero scalar.parametersδ :sharedTypeinstancegiven byclause 1smul := (· • ·)clause 2one_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 _clause 3mul_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); ringclause 4smul_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 tclause 5smul_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 ringclause 6add_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 ringclause 7zero_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)
@[fun_prop] 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.Proof (Lean source)
@[fun_prop] 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.
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 → ℝ,
conclusion 1
conclusion 2
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 → ℝ,
conclusion 1
conclusion 2
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
For a two-stage potential-outcome system on a standard Borel sample space with a finite measure, measurable treatment values that have measurable singletons, and measurable state spaces at both stages, a two-stage dynamic-treatment-regime system, and a fixed two-stage target treatment regime, suppose the conditional probability of the target treatment at stage 0, given the stage-0 history, lies strictly between zero and one almost everywhere, and the analogous conditional probability at stage 1, given the stage-1 history, also lies strictly between zero and one almost everywhere. The dynamic-treatment-regime estimation system is then constructed from those data.
Definition (Lean source)
parameters
def
given by
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
For a potential-outcome system whose sample space is standard Borel and whose measure is finite with a measurable treatment space in which every singleton is measurable and measurable stage-specific covariate spaces, a two-stage dynamic treatment-regime estimation system, an independent identically distributed sample whose observations comprise baseline covariates, first treatment, intermediate covariates, second treatment, and outcome, a one-shot sample split, a sequence of stagewise nuisance-function estimates indexed by sample size and the underlying random outcome, and a sample-size index, the one-shot double-machine-learning sequentially doubly robust estimator is the function of the underlying random outcome that averages, over the split's estimation fold, the sequential doubly robust moment at the target treatment regime, using the nuisance estimate at that sample size and target value zero.
Definition (Lean source)
parameters
δ :
Type
S :
DTREstimationSystem P δ γ
sample :
IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
η_hat :
ℕ → P.Ω → DTRNuisanceVec₂ δ γ
n :
ℕ
def
dml_DTR_estimator S sample split η_hat n :
P.Ω → ℝ
given by
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
δ :
Type
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
For a potential-outcome system whose sample space is standard Borel and whose measure is finite with a measurable treatment space in which every singleton is measurable and measurable stage-specific covariate spaces, a two-stage dynamic treatment-regime estimation system, and a real number for which every stage-0 and stage-1 true propensity score lies between that number and one minus that number, inclusive, the abstract general moment associated with the two-stage sequential doubly robust score has the system's true nuisance functions and target value, its two stagewise aggregate error seminorms, and that score as its moment function.
Definition (Lean source)
parameters
δ :
Type
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 - ε)
def
seqDRGeneralMoment S h_e_pointwise :
GeneralMoment P.Ω P.μ (γ 0 × δ × γ 1 × δ × ℝ) S.P_Z (DTRNuisanceVec₂ δ γ)
given by
clause 1
m := fun η z θ => S.seqDRMomentFunctional η z θ
clause 2
η₀ := S.η₀
clause 3
θ₀ := S.θ₀
clause 4
H_ε := DTREstimationSystem.H_ε ε
clause 5
clause 6
clause 7
m_meas := fun η θ => S.measurable_seqDRMomentFunctional η θ
clause 8
η₀_mem := h_e_pointwise
clause 9
J₀ := -1
clause 10
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
δ :
Type
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.hypothesesδ :sharedTypeS :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 ε.hypothesesδ :sharedTypeS :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
δ :
Type
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.hypothesesconclusionMeasurable (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
δ :
Type
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.η₀.hypothesesconclusionMeasurable S.ψ_seqDRProof (Lean source)
@[fun_prop] 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.hypothesesProof (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.hypothesesProof (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.hypothesesδ :sharedTypeS :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 fun_prop have hI0Y_int : Integrable (fun ω => I0 ω * Y ω) P.μ := by fun_prop 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 fun_prop have hM1_meas : Measurable M1 := by fun_prop have hI0M0_int : Integrable (fun ω => I0 ω * M0 ω) P.μ := by fun_prop have hI0M1_int : Integrable (fun ω => I0 ω * M1 ω) P.μ := by fun_prop 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 condexp_linearity have hI0_sm_B1 : StronglyMeasurable[B1.sigma] I0 := by fun_prop 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 fun_prop 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 := by fun_prop (disch := measurability) 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 fun_prop 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 rw [Pi.sub_apply, h1, h0] ring -
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.hypothesesδ :sharedTypeS :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 fun_prop have hI1_int : Integrable I1 P.μ := by fun_prop 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 fun_prop have hI1Y_int : Integrable (fun ω => I1 ω * Y ω) P.μ := by fun_prop have hI1Yf_int : Integrable (fun ω => I1 ω * Yf ω) P.μ := by fun_prop have hI1M1_int : Integrable (fun ω => I1 ω * M1 ω) P.μ := by fun_prop have hI0I1Y_int : Integrable (fun ω => I0 ω * (I1 ω * Y ω)) P.μ := by fun_prop have hI0I1Yf_int : Integrable (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ := by fun_prop have hI0I1M1_int : Integrable (fun ω => I0 ω * (I1 ω * M1 ω)) P.μ := by fun_prop 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 condexp_linearity 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 fun_prop have hM1_sm_B1 : StronglyMeasurable[B1.sigma] M1 := by fun_prop have hI0M1_sm_B1 : StronglyMeasurable[B1.sigma] (fun ω => I0 ω * M1 ω) := by fun_prop 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 fun_prop 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 := by fun_prop (disch := measurability) 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 (fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) * Y ω) P.μ rw [heq] exact hI1Y_int) have hExch : B1.condExpGiven (fun ω => I1 ω * Y ω) P.μ =ᵐ[P.μ] (fun ω => B1.condExpGiven I1 P.μ ω * B1.condExpGiven Y P.μ ω) := by unfold POCFBundle.condExpGiven have hprod_rw : (fun ω => u (S.toPODTRSystem.factualD ⟨1, by decide⟩ ω) * Y ω) = (fun ω => I1 ω * 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 hpull_I0Y := B1.condExpGiven_mul_of_stronglyMeasurable_left (f := I0) (g := fun ω => I1 ω * Y ω) hI0_sm_B1 hI0I1Y_int hI1Y_int have hCE_fact : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Yf ω)) P.μ =ᵐ[P.μ] (fun ω => I0 ω * (S.e₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * M1 ω)) := by refine hCE_fact_to_cf.trans ?_ 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 ⊢ filter_upwards [hpull_I0Y, hExch, S.e₁_compat, S.indD_mul_μ₁_val_comp_eq hA] with ω hp hE he hμ have hp' : B1.condExpGiven (fun ω => I0 ω * (I1 ω * Y ω)) P.μ ω = I0 ω * B1.condExpGiven (fun ω => I1 ω * Y ω) P.μ ω := by exact hp have hμ_local : I0 ω * M1 ω = I0 ω * B1.condExpGiven Y P.μ ω := by have hμ' : S.toPODTRSystem.indD S.dbar 1 ω * M1 ω = S.toPODTRSystem.indD S.dbar 1 ω * B1.condExpGiven Y P.μ ω := hμ rw [hI0_eq_indD] exact hμ' rw [hp', hE, he] calc I0 ω * (S.e₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * B1.condExpGiven Y P.μ ω) = S.e₁_val (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) * (I0 ω * B1.condExpGiven Y P.μ ω) := by ring _ = S.e₁_val -- … 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.hypothesesconclusionS.θ₀ = ∫ ω, 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
For a real overlap margin, the sequential doubly robust remainder constant is .
Definition (Lean source)
parameters
ε :
ℝ
def
seqDR_rem_const ε :
ℝ
given by
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
δ :
Type
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)|
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
δ :
Type
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
δ :
Type
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
δ :
Type
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
δ :
Type
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
δ :
Type
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