Estimation.DTR.DML
This file defines the one-shot double machine learning estimator for the two-period dynamic-treatment-regime effect.
Basic 2 core · 1 supporting Defines dml_DTR_estimator, the fold-B empirical mean of the two-stage sequential doubly robust pseudo-outcome. ★ seqDRMomentFunctional_memLp_two
One-shot DTR DML estimator and score interfaces
Defines dml_DTR_estimator, the fold-B empirical mean of the two-stage
sequential doubly robust pseudo-outcome. It also proves the joint measurability
and L² packaging lemmas needed to instantiate the abstract DML theorem. The
asymptotic-linearity wrapper itself is in AsymptoticLinearity.
lemma seqDRMomentFunctional_memLp_two reviewed
⚑ flagged
Causalean.Estimation.DTR
For a potential-outcome system, treatment space, and two-stage covariate spaces, a dynamic-treatment-regime estimation system, an overlap level, strict overlap, square-integrability of the factual outcome, a nuisance specification, its membership in the bounded nuisance class, and square-integrability of its stage-zero and stage-one outcome regressions, the resulting sequential doubly robust moment at the target is square-integrable under the observed-data law.
Formal statement
hypotheses
δ :
Type
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
h_y2 :
Integrable (fun ω => (S.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ
η :
DTRNuisanceVec₂ δ γ
hη :
η ∈ DTREstimationSystem.H_ε ε
h_mu0 :
MemLp η.μ₀_fn 2 S.P_H₀
h_mu1 :
MemLp η.μ₁_fn 2 S.P_H₁
conclusion
MemLp (fun z => S.seqDRMomentFunctional η z S.θ₀) 2 S.P_Z
Proof (Lean source)
lemma seqDRMomentFunctional_memLp_two
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(h_y2 : Integrable (fun ω => (S.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ)
(η : DTRNuisanceVec₂ δ γ)
(hη : η ∈ DTREstimationSystem.H_ε ε)
(h_mu0 : MemLp η.μ₀_fn 2 S.P_H₀)
(h_mu1 : MemLp η.μ₁_fn 2 S.P_H₁) :
MemLp (fun z => S.seqDRMomentFunctional η z S.θ₀) 2 S.P_Z := by
have hY_L2 : MemLp S.toPOLongitudinalPathSystem.factualY 2 P.μ :=
(memLp_two_iff_integrable_sq
S.toPOLongitudinalPathSystem.measurable_factualY.aestronglyMeasurable).2 h_y2
have hμ0_comp_L2 :
MemLp (fun ω => η.μ₀_fn
(S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) 2 P.μ := by
have hmap : MemLp η.μ₀_fn 2
(P.μ.map (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩)) := by
simpa [DTREstimationSystem.P_H₀] using h_mu0
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
(S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable).1 hmap
have hμ1_comp_L2 :
MemLp (fun ω => η.μ₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) 2 P.μ := by
let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω =>
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)
have hH1_meas : Measurable H1 := by
dsimp [H1]
exact (S.toPOLongitudinalPathSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩))
have hmap : MemLp η.μ₁_fn 2 (P.μ.map H1) := by
simpa [DTREstimationSystem.P_H₁, H1] using h_mu1
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
hH1_meas.aemeasurable).1 hmap
have hw0_bound :
∀ᵐ ω ∂P.μ,
‖indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)‖ ≤ ε⁻¹ := by
refine Eventually.of_forall fun ω => ?_
have he := hη.1 (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)
by_cases hD : S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω =
S.dbar ⟨0, by decide⟩
· have hpos : 0 < η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) :=
lt_of_lt_of_le h_overlap.1 he.1
have hle : (η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos h_overlap.1).2 he.1
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.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) *
η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))‖ ≤ (ε * ε)⁻¹ := by
refine Eventually.of_forall fun ω => ?_
have he0 := hη.1 (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)
have he1 := hη.2
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)
by_cases hD0 : S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω =
S.dbar ⟨0, by decide⟩
· by_cases hD1 : S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω =
S.dbar ⟨1, by decide⟩
· have hpos0 : 0 < η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) :=
lt_of_lt_of_le h_overlap.1 he0.1
have hpos1 : 0 < η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) :=
lt_of_lt_of_le h_overlap.1 he1.1
have hle0 : (η.e₀_fn
(S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos0 h_overlap.1).2 he0.1
have hle1 : (η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))⁻¹ ≤ ε⁻¹ :=
(inv_le_inv₀ hpos1 h_overlap.1).2 he1.1
have hle :
(η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))⁻¹ *
(η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))⁻¹
≤ ε⁻¹ * ε⁻¹ :=
mul_le_mul hle1 hle0 (inv_nonneg.mpr hpos0.le)
(inv_nonneg.mpr h_overlap.1.le)
have hind0eq : indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) = 1 := by
unfold indEq
rw [if_pos]
simpa using hD0
have hind1eq : indEq (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩) = 1 := by
unfold indEq
rw [if_pos]
simpa using hD1
rw [hind0eq, hind1eq, one_mul, norm_div, norm_one, norm_mul]
rw [show ‖η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)‖ =
η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) from
Real.norm_of_nonneg hpos0.le]
rw [show ‖η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)‖ =
η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.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 hind1zero : indEq (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩) = 0 := by
unfold indEq
rw [if_neg]
simpa using hD1
rw [hind1zero, 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)
have hind0zero : indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) = 0 := by
unfold indEq
rw [if_neg]
simpa using hD0
rw [hind0zero, zero_mul, zero_div, norm_zero]
exact hεεinv_nonneg
have hw0_Linf :
MemLp
(fun ω => indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
η.e₀_fn (S.toPOLongitudinalPathSystem.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.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩)).div
(η.e₀_meas.comp (S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩))
have hw1_Linf :
MemLp
(fun ω =>
(indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) *
η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) ⊤ P.μ := by
refine MemLp.of_bound ?_ (ε * ε)⁻¹ hw1_bound
apply Measurable.aestronglyMeasurable
have hind0 : Measurable (fun ω => indEq
(S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩)) :=
(measurable_indEq_left (S.dbar ⟨0, by decide⟩)).comp
(S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩)
have hind1 : Measurable (fun ω => indEq
(S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) :=
(measurable_indEq_left (S.dbar ⟨1, by decide⟩)).comp
(S.toPOLongitudinalPathSystem.measurable_factualD ⟨1, by decide⟩)
have he0 : Measurable (fun ω =>
η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) :=
η.e₀_meas.comp (S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩)
have he1 : Measurable (fun ω =>
η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) :=
η.e₁_meas.comp
((S.toPOLongitudinalPathSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩)))
exact (hind0.mul hind1).div (he0.mul he1)
have hterm0_L2 :
MemLp
(fun ω =>
(indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) /
η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) *
(η.μ₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) -
η.μ₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) 2 P.μ :=
(hμ1_comp_L2.sub hμ0_comp_L2).mul hw0_Linf
have hterm1_L2 :
MemLp
(fun ω =>
((indEq (S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω)
(S.dbar ⟨0, by decide⟩) *
indEq (S.toPOLongitudinalPathSystem.factualD ⟨1, by decide⟩ ω)
(S.dbar ⟨1, by decide⟩)) /
(η.e₀_fn (S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω) *
η.e₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) *
(S.toPOLongitudinalPathSystem.factualY ω -
η.μ₁_fn
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω))) 2 P.μ :=
(hY_L2.sub hμ1_comp_L2).mul hw1_Linf
have hscore_comp_L2 :
MemLp (fun ω => S.seqDRMomentFunctional η (S.factualZ ω) S.θ₀) 2 P.μ := by
have hconst_L2 : MemLp (fun _ : P.Ω => S.θ₀) 2 P.μ := memLp_const _
have hsum_L2 :=
((hμ0_comp_L2.add hterm0_L2).add hterm1_L2).sub hconst_L2
exact hsum_L2
have hscore_meas :
Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ =>
S.seqDRMomentFunctional η z S.θ₀) :=
S.measurable_seqDRMomentFunctional η S.θ₀
rw [DTREstimationSystem.P_Z]
exact (memLp_map_measure_iff hscore_meas.aestronglyMeasurable
S.measurable_factualZ.aemeasurable).2 hscore_comp_L2
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
1 supporting declaration (lemmas, instances)
-
measurable_seqDRMomentFunctional_uncurrylemma — Given a dynamic-treatment-regime estimation system, target value, and parameterized nuisance functions, if the first outcome regression, first propensity, second outcome regression, and second propensity are jointly measurable in the parameter and observation, then the corresponding sequential doubly robust moment is jointly measurable.hypothesesδ :sharedTypeΩ' :Type*S :DTREstimationSystem P δ γθ :ℝη_fn :Ω' → DTRNuisanceVec₂ δ γh_mu0 :Measurable (fun p : Ω' × γ 0 => (η_fn p.1).μ₀_fn p.2)h_e0 :Measurable (fun p : Ω' × γ 0 => (η_fn p.1).e₀_fn p.2)h_mu1 :Measurable (fun p : Ω' × (γ 1 × δ × γ 0) => (η_fn p.1).μ₁_fn p.2)h_e1 :Measurable (fun p : Ω' × (γ 1 × δ × γ 0) => (η_fn p.1).e₁_fn p.2)conclusionMeasurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => S.seqDRMomentFunctional (η_fn p.1) p.2 θ)Proof (Lean source)
lemma measurable_seqDRMomentFunctional_uncurry {Ω' : Type*} [MeasurableSpace Ω'] (S : DTREstimationSystem P δ γ) (θ : ℝ) (η_fn : Ω' → DTRNuisanceVec₂ δ γ) (h_mu0 : Measurable (fun p : Ω' × γ 0 => (η_fn p.1).μ₀_fn p.2)) (h_e0 : Measurable (fun p : Ω' × γ 0 => (η_fn p.1).e₀_fn p.2)) (h_mu1 : Measurable (fun p : Ω' × (γ 1 × δ × γ 0) => (η_fn p.1).μ₁_fn p.2)) (h_e1 : Measurable (fun p : Ω' × (γ 1 × δ × γ 0) => (η_fn p.1).e₁_fn p.2)) : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => S.seqDRMomentFunctional (η_fn p.1) p.2 θ) := by unfold DTREstimationSystem.seqDRMomentFunctional unfold Causalean.Estimation.DTR.seqDRMoment have hpS0 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (p.1, projS₀ p.2)) := by unfold projS₀ exact Measurable.prodMk measurable_fst measurable_snd.fst have hpH1 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (p.1, histH₁ p.2)) := by unfold histH₁ projS₁ projD₀ projS₀ measurability have hμ0 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (η_fn p.1).μ₀_fn (projS₀ p.2)) := h_mu0.comp hpS0 have he0 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (η_fn p.1).e₀_fn (projS₀ p.2)) := h_e0.comp hpS0 have hμ1 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (η_fn p.1).μ₁_fn (histH₁ p.2)) := h_mu1.comp hpH1 have he1 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => (η_fn p.1).e₁_fn (histH₁ p.2)) := h_e1.comp hpH1 have hind0 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => indEq (projD₀ p.2) (S.dbar 0)) := by unfold projD₀ exact (measurable_indEq_left (S.dbar 0)).comp measurable_snd.snd.fst have hind1 : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => indEq (projD₁ p.2) (S.dbar 1)) := by unfold projD₁ exact (measurable_indEq_left (S.dbar 1)).comp measurable_snd.snd.snd.snd.fst have hy : Measurable (fun p : Ω' × (γ 0 × δ × γ 1 × δ × ℝ) => projY p.2) := by unfold projY exact measurable_snd.snd.snd.snd.snd 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
AsymptoticLinearity 1 core · 0 supporting Proves dml_DTR_isAsymLinear for the two-stage sequential doubly robust estimator. ★ dml_DTR_isAsymLinear
Asymptotic linearity for one-shot DTR DML
Proves dml_DTR_isAsymLinear for the two-stage sequential doubly robust
estimator. The wrapper translates stagewise overlap, measurability, L², four
individual o_p(1) rates, and two same-stage product rates into the abstract
sequential-DML interface.
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 evaluation-fold fraction |B(n)|/n converges to some c > 0. 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 each learner is measurable with respect to the auxiliary training fold's σ-algebra jointly with the covariate history at stage 0 and at stage 1. Finally, each stagewise estimation error converges to zero in L² at rate o_p(1), and both same-stage products of an outcome-regression error with its corresponding propensity error vanish at the doubly-robust rate o_p(n^{-1/2}).
Formal statement
hypotheses
δ :
Type
S :
DTREstimationSystem P δ γ
ε :
ℝ
hA :
S.toPOLongitudinalPathSystem.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.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ dbar : Fin 2 → δ,
Integrable (fun ω => (S.toPOLongitudinalPathSystem.Y_of dbar ω) ^ 2) P.μ
sample :
IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < 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₁
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.μ
Same-stage product rates.
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.μ
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.toPOLongitudinalPathSystem.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.toPOLongitudinalPathSystem.factualY ω) ^ 2) P.μ)
(h_yd2 : ∀ dbar : Fin 2 → δ,
Integrable (fun ω => (S.toPOLongitudinalPathSystem.Y_of dbar ω) ^ 2) P.μ)
(sample : IIDSample P.Ω (γ 0 × δ × γ 1 × δ × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
{c : ℝ} (hc_pos : 0 < c)
(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₁)
-- 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.μ)
-- Same-stage product rates.
(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.μ) :
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.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable
haveI : IsProbabilityMeasure S.P_H₁ := by
unfold DTREstimationSystem.P_H₁
exact Measure.isProbabilityMeasure_map
((S.toPOLongitudinalPathSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPOLongitudinalPathSystem.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.toPOLongitudinalPathSystem.Y_of S.dbar) 2 P.μ :=
(memLp_two_iff_integrable_sq
(S.toPOLongitudinalPathSystem.measurable_Y_of S.dbar).aestronglyMeasurable).2
(h_yd2 S.dbar)
have hcond_L2 :
MemLp ((S.toPOLongitudinalPathSystem.historyBundle 0 (by decide)).condExpGiven
(S.toPOLongitudinalPathSystem.Y_of S.dbar) P.μ) 2 P.μ := by
simpa [POCFBundle.condExpGiven] using hYd_L2.condExp
have hcomp_L2 :
MemLp (fun ω => S.μ₀_val
(S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)) 2 P.μ :=
hcond_L2.ae_eq (S.μ₀_compat hA)
rw [DTREstimationSystem.P_H₀]
exact (memLp_map_measure_iff S.μ₀_meas.aestronglyMeasurable
(S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable).2 hcomp_L2
have hμ1_val_memLp : MemLp S.μ₁_val 2 S.P_H₁ := by
let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω =>
(S.toPOLongitudinalPathSystem.factualS ⟨1, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualD ⟨0, by decide⟩ ω,
S.toPOLongitudinalPathSystem.factualS ⟨0, by decide⟩ ω)
have hH1_meas : Measurable H1 := by
dsimp [H1]
exact (S.toPOLongitudinalPathSystem.measurable_factualS ⟨1, by decide⟩).prod
((S.toPOLongitudinalPathSystem.measurable_factualD ⟨0, by decide⟩).prod
(S.toPOLongitudinalPathSystem.measurable_factualS ⟨0, by decide⟩))
have hcomp_L2 :
MemLp (fun ω => S.μ₁_val (H1 ω)) 2 P.μ := by
simpa [H1] using (S.stageOneReg_memLp h_overlap h_y2).ae_eq
(S.μ₁_val_comp_eq_stageOneReg).symm
rw [DTREstimationSystem.P_H₁]
exact (memLp_map_measure_iff S.μ₁_meas.aestronglyMeasurable
hH1_meas.aemeasurable).2 hcomp_L2
have he0_val_memLp : MemLp S.e₀_val 2 S.P_H₀ := by
refine MemLp.of_bound S.e₀_meas.aestronglyMeasurable 1 ?_
refine Eventually.of_forall fun s => ?_
rw [Real.norm_eq_abs]
exact abs_le.mpr ⟨by linarith [S.e₀_pos s], by linarith [S.e₀_lt_one s]⟩
have he1_val_memLp : MemLp S.e₁_val 2 S.P_H₁ := by
refine MemLp.of_bound S.e₁_meas.aestronglyMeasurable 1 ?_
refine Eventually.of_forall fun h => ?_
rw [Real.norm_eq_abs]
-- … truncated; follow the source link for the rest …