Estimation.DTR.ScoreL2
Square-integrability of the dynamic-treatment-regime score on the nuisance neighbourhood.
ScoreL2 1 core · 0 supporting This module proves the L² continuity statement for the two-stage sequential doubly robust DTR score. ★ seqDR_score_diff_isLittleOp_one
Sequential DR score L² continuity for two-stage regimes
This module proves the L² continuity statement for the two-stage sequential
doubly robust DTR score. The headline theorem
DTREstimationSystem.seqDR_score_diff_isLittleOp_one says that
‖m_seqDR(η_hat n, ·, θ₀) - m_seqDR(η₀, ·, θ₀)‖_{L²(P_Z)} = o_p(1)
whenever the four stagewise nuisance errors for μ₀, μ₁, e₀, and e₁
converge in their natural history-space L² norms and the estimated propensities
remain in the overlap-bounded set H_ε.
The proof combines the pointwise Lipschitz bound from
ScoreL2.Helpers, L² norm transport from the history marginals to the full
observed data law P_Z, and a truncation lemma for residuals multiplied by
propensity-estimation errors. This is the score-difference input used by the
DTR double-machine-learning layer.
theorem seqDR_score_diff_isLittleOp_one reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Sequential DR score L²(P_Z) continuity. Consider a two-stage dynamic-treatment-regime estimation system in which the estimated propensity scores stay strictly between ε and 1-ε, the system's identification assumptions (consistency, sequential exchangeability, positivity) hold, the observed outcome has finite second moment, and every potential outcome under a fixed two-stage treatment regime has finite second moment. Given a sequence of nuisance-estimator draws η̂(n) that always land inside the ε-overlap-bounded nuisance set, whose stage-0 outcome-regression, stage-1 outcome-regression, stage-0 propensity-score, and stage-1 propensity-score estimation errors are each square-integrable against the corresponding history law, for every draw and every sample point, and whose four stagewise L² estimation-error rates each vanish in probability (are ), then the L²(P_Z) distance between the sequential doubly-robust score evaluated at η̂(n) and at the true nuisance η₀ is itself .
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
hA :
S.toPODTRSystem.Assumptions
h_y2 :
Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ
h_yd2 :
∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ
η_hat :
ℕ → P.Ω → DTRNuisanceVec₂ δ γ
h_in_H :
∀ n ω, η_hat n ω ∈ DTREstimationSystem.H_ε ε
h_mu0_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀
h_mu1_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁
h_e0_memLp :
∀ n ω, MemLp (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀
h_e1_memLp :
∀ n ω, MemLp (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁
h_mu0_rate :
IsLittleOp (fun n ω => (eLpNorm (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal) (fun _ => (1 : ℝ)) P.μ
h_mu1_rate :
IsLittleOp (fun n ω => (eLpNorm (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal) (fun _ => (1 : ℝ)) P.μ
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.μ
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.μ
conclusion
IsLittleOp (fun n ω => (eLpNorm (fun z => S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ - S.seqDRMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
Proof (Lean source)
theorem seqDR_score_diff_isLittleOp_one
(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_mu0_memLp : ∀ n ω,
MemLp (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀)
(h_mu1_memLp : ∀ n ω,
MemLp (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁)
(h_e0_memLp : ∀ n ω,
MemLp (fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀)
(h_e1_memLp : ∀ n ω,
MemLp (fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁)
(h_mu0_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2 S.P_H₀).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_mu1_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2 S.P_H₁).toReal)
(fun _ => (1 : ℝ)) P.μ)
(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.μ)
(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.μ) :
IsLittleOp
(fun n ω =>
(eLpNorm (fun z =>
S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ -
S.seqDRMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
classical
have _hA_used := hA
rcases h_overlap with ⟨hε_pos, hε_half, hprop⟩
have h_overlap' : S.StrictOverlap ε := ⟨hε_pos, hε_half, hprop⟩
haveI : IsProbabilityMeasure S.P_Z := by
unfold DTREstimationSystem.P_Z
exact Measure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable
let R0 : γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun z =>
|S.μ₁_val (histH₁ z) - S.μ₀_val (projS₀ z)|
+ |projY z - S.μ₁_val (histH₁ z)|
let R1 : γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun z =>
|projY z - S.μ₁_val (histH₁ z)|
let dμ0Z : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
(η_hat n ω).μ₀_fn (projS₀ z) - S.μ₀_val (projS₀ z)
let dμ1Z : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
(η_hat n ω).μ₁_fn (histH₁ z) - S.μ₁_val (histH₁ z)
let de0Z : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
(η_hat n ω).e₀_fn (projS₀ z) - S.e₀_val (projS₀ z)
let de1Z : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
(η_hat n ω).e₁_fn (histH₁ z) - S.e₁_val (histH₁ z)
let cross0 : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
R0 z * |de0Z n ω z|
let cross1 : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
R1 z * |de1Z n ω z|
let score : ℕ → P.Ω → γ 0 × δ × γ 1 × δ × ℝ → ℝ := fun n ω z =>
S.seqDRMomentFunctional (η_hat n ω) z S.θ₀ -
S.seqDRMomentFunctional S.η₀ z S.θ₀
have hprojY_meas : Measurable (fun z : γ 0 × δ × γ 1 × δ × ℝ => projY z) := by
unfold projY
measurability
have hμ0Z_val_memLp : MemLp (fun z => S.μ₀_val (projS₀ z)) 2 S.P_Z := by
have hmap : MemLp S.μ₀_val 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z)) := by
simpa [P_Z_map_projS₀_eq_P_H₀ S] using μ₀_val_memLp S hA h_yd2
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_projS₀.aemeasurable).1 hmap
have hμ1Z_val_memLp : MemLp (fun z => S.μ₁_val (histH₁ z)) 2 S.P_Z := by
have hmap : MemLp S.μ₁_val 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z)) := by
simpa [P_Z_map_histH₁_eq_P_H₁ S] using μ₁_val_memLp S h_overlap' h_y2
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_histH₁.aemeasurable).1 hmap
have hY_Z_memLp : MemLp (fun z : γ 0 × δ × γ 1 × δ × ℝ => projY z) 2 S.P_Z := by
have hY_L2 : MemLp S.toPODTRSystem.factualY 2 P.μ :=
(memLp_two_iff_integrable_sq
S.toPODTRSystem.measurable_factualY.aestronglyMeasurable).2 h_y2
rw [DTREstimationSystem.P_Z]
exact (memLp_map_measure_iff hprojY_meas.aestronglyMeasurable
S.measurable_factualZ.aemeasurable).2 (by
simpa [DTREstimationSystem.factualZ, projY, Function.comp_def] using hY_L2)
have hR1_meas : Measurable R1 := by
simpa [R1, Function.comp_def] using
(continuous_abs.measurable.comp
(hprojY_meas.sub (S.μ₁_meas.comp measurable_histH₁)))
have hR0_meas : Measurable R0 := by
have hres : Measurable
(fun z : γ 0 × δ × γ 1 × δ × ℝ =>
|S.μ₁_val (histH₁ z) - S.μ₀_val (projS₀ z)|) := by
simpa [Function.comp_def] using
(continuous_abs.measurable.comp
((S.μ₁_meas.comp measurable_histH₁).sub
(S.μ₀_meas.comp measurable_projS₀)))
exact hres.add hR1_meas
have hR1_nonneg : ∀ z, 0 ≤ R1 z := by
intro z
dsimp [R1]
positivity
have hR0_nonneg : ∀ z, 0 ≤ R0 z := by
intro z
dsimp [R0]
positivity
have hR1_memLp : MemLp R1 2 S.P_Z := by
simpa [R1, Real.norm_eq_abs] using (hY_Z_memLp.sub hμ1Z_val_memLp).norm
have hR0_memLp : MemLp R0 2 S.P_Z := by
have h01 : MemLp (fun z =>
|S.μ₁_val (histH₁ z) - S.μ₀_val (projS₀ z)|) 2 S.P_Z := by
simpa [Real.norm_eq_abs] using (hμ1Z_val_memLp.sub hμ0Z_val_memLp).norm
exact h01.add hR1_memLp
have hdμ0Z_memLp : ∀ n ω, MemLp (dμ0Z n ω) 2 S.P_Z := by
intro n ω
have hmap : MemLp
(fun s₀ => (η_hat n ω).μ₀_fn s₀ - S.μ₀_val s₀) 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z)) := by
simpa [P_Z_map_projS₀_eq_P_H₀ S] using h_mu0_memLp n ω
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_projS₀.aemeasurable).1 hmap
have hdμ1Z_memLp : ∀ n ω, MemLp (dμ1Z n ω) 2 S.P_Z := by
intro n ω
have hmap : MemLp
(fun h => (η_hat n ω).μ₁_fn h - S.μ₁_val h) 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z)) := by
simpa [P_Z_map_histH₁_eq_P_H₁ S] using h_mu1_memLp n ω
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_histH₁.aemeasurable).1 hmap
have hde0Z_memLp : ∀ n ω, MemLp (de0Z n ω) 2 S.P_Z := by
intro n ω
have hmap : MemLp
(fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z)) := by
simpa [P_Z_map_projS₀_eq_P_H₀ S] using h_e0_memLp n ω
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_projS₀.aemeasurable).1 hmap
have hde1Z_memLp : ∀ n ω, MemLp (de1Z n ω) 2 S.P_Z := by
intro n ω
have hmap : MemLp
(fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2
(S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z)) := by
simpa [P_Z_map_histH₁_eq_P_H₁ S] using h_e1_memLp n ω
exact (memLp_map_measure_iff hmap.aestronglyMeasurable
measurable_histH₁.aemeasurable).1 hmap
have hde0Z_meas : ∀ n ω, Measurable (de0Z n ω) := by
intro n ω
exact ((η_hat n ω).e₀_meas.comp measurable_projS₀).sub
(S.e₀_meas.comp measurable_projS₀)
have hde1Z_meas : ∀ n ω, Measurable (de1Z n ω) := by
intro n ω
exact ((η_hat n ω).e₁_meas.comp measurable_histH₁).sub
(S.e₁_meas.comp measurable_histH₁)
have hde0Z_bdd : ∀ n ω z, |de0Z n ω z| ≤ 1 := by
intro n ω z
have hη := h_in_H n ω
have hη_nonneg : 0 ≤ (η_hat n ω).e₀_fn (projS₀ z) :=
le_trans hε_pos.le ((hη.1 (projS₀ z)).1)
have hη_le_one : (η_hat n ω).e₀_fn (projS₀ z) ≤ 1 := by
linarith [(hη.1 (projS₀ z)).2, hε_pos.le]
have hS_nonneg : 0 ≤ S.e₀_val (projS₀ z) := le_of_lt (S.e₀_pos _)
have hS_le_one : S.e₀_val (projS₀ z) ≤ 1 := le_of_lt (S.e₀_lt_one _)
dsimp [de0Z]
rw [abs_le]
constructor <;> linarith
have hde1Z_bdd : ∀ n ω z, |de1Z n ω z| ≤ 1 := by
intro n ω z
have hη := h_in_H n ω
have hη_nonneg : 0 ≤ (η_hat n ω).e₁_fn (histH₁ z) :=
le_trans hε_pos.le ((hη.2 (histH₁ z)).1)
have hη_le_one : (η_hat n ω).e₁_fn (histH₁ z) ≤ 1 := by
linarith [(hη.2 (histH₁ z)).2, hε_pos.le]
have hS_nonneg : 0 ≤ S.e₁_val (histH₁ z) := le_of_lt (S.e₁_pos _)
have hS_le_one : S.e₁_val (histH₁ z) ≤ 1 := le_of_lt (S.e₁_lt_one _)
dsimp [de1Z]
rw [abs_le]
constructor <;> linarith
have hde0Z_rate :
IsLittleOp
(fun n ω => (eLpNorm (de0Z n ω) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
have heq :
(fun n ω => (eLpNorm (de0Z n ω) 2 S.P_Z).toReal) =
(fun n ω =>
(eLpNorm
(fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀) 2 S.P_H₀).toReal) := by
funext n ω
exact congrArg toReal
(by
dsimp [de0Z]
exact eLpNorm_comp_projS₀_eq (S := S)
(f := fun s₀ => (η_hat n ω).e₀_fn s₀ - S.e₀_val s₀)
(h_e0_memLp n ω).aestronglyMeasurable)
rw [heq]
exact h_e0_rate
have hde1Z_rate :
IsLittleOp
(fun n ω => (eLpNorm (de1Z n ω) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
have heq :
(fun n ω => (eLpNorm (de1Z n ω) 2 S.P_Z).toReal) =
(fun n ω =>
(eLpNorm
(fun h => (η_hat n ω).e₁_fn h - S.e₁_val h) 2 S.P_H₁).toReal) := by
funext n ω
exact congrArg toReal
(by
dsimp [de1Z]
exact eLpNorm_comp_histH₁_eq (S := S)
(f := fun h => (η_hat n ω).e₁_fn h - S.e₁_val h)
(h_e1_memLp n ω).aestronglyMeasurable)
rw [heq]
exact h_e1_rate
have hcross0_rate :
IsLittleOp
(fun n ω => (eLpNorm (cross0 n ω) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
simpa [cross0] using
-- … truncated; follow the source link for the rest …
Helpers 3 core · 14 supporting This module collects analytic helpers for proving L² consistency of the two-stage sequential doubly robust DTR score. ★ seqDR_real_bound★ seqDR_score_diff_pointwise_bound
Sequential DR score norm helpers
This module collects analytic helpers for proving L² consistency of the
two-stage sequential doubly robust DTR score. It defines the overlap envelope
K_seqDR, proves elementary indicator and inverse-overlap bounds, transports
L² norms from the stage histories to the observed data law, and supplies the
truncation lemma residual_mul_error_isLittleOp_one for residuals multiplied by
bounded nuisance errors.
The later lemmas provide the pointwise score algebra used by
ScoreL2.lean: seqDR_stage0_ratio_bound,
seqDR_stage1_ratio_bound, seqDR_real_bound, and the full almost-sure bound
DTREstimationSystem.seqDR_score_diff_pointwise_bound. The module also records
the square-integrability of the true stagewise regression representatives under
the corresponding history marginals.
def K_seqDR reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
The sequential doubly robust Lipschitz constant combines the stagewise inverse-overlap bounds used in score continuity.
Definition (Lean source)
noncomputable def K_seqDR (ε : ℝ) : ℝ :=
1 + 2 / ε + 4 / ε ^ 2 + 4 / ε ^ 3
lemma seqDR_real_bound reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Pointwise Lipschitz bound for the two-stage sequential DR score (real-valued form). Consider a stage-0 propensity e0 and its estimate ê0, a stage-1 propensity e1 and its estimate ê1, true and estimated stage-0/stage-1 outcome-regression values μ0, μ0h, μ1, μ1h, an outcome value y, a target parameter θ, and treatment indicators I0, I1, where ε is strictly positive, both the true and estimated stage-0 propensities are at least ε, both the true and estimated stage-1 propensities are at least ε, and both treatment indicators have absolute value at most 1. Then the absolute difference between the sequential doubly-robust moment built from the estimated nuisances (ê0, ê1, μ0h, μ1h) and from the true nuisances (e0, e1, μ0, μ1) is bounded by the Lipschitz constant K_seqDR ε times the sum of the stage-0 regression error, the stage-1 regression error, and cross terms in which the stage-0 and stage-1 propensity errors are weighted by outcome/regression residuals.
Formal statement
hypotheses
ε e0 ê0 e1 ê1 μ0 μ0h μ1 μ1h y θ I0 I1 :
ℝ
hε :
0 < ε
he0 :
ε ≤ e0
hê0 :
ε ≤ ê0
he1 :
ε ≤ e1
hê1 :
ε ≤ ê1
hI0 :
|I0| ≤ 1
hI1 :
|I1| ≤ 1
conclusion
|(μ0h + (I0 / ê0) * (μ1h - μ0h) + (I0 * I1 / (ê0 * ê1)) * (y - μ1h) - θ)
- (μ0 + (I0 / e0) * (μ1 - μ0) + (I0 * I1 / (e0 * e1)) * (y - μ1) - θ)|
≤ K_seqDR ε * (|μ0h - μ0| + |μ1h - μ1| + (|μ1 - μ0| + |y - μ1|) * |ê0 - e0| + |y - μ1| * |ê1 - e1|)
Proof (Lean source)
lemma seqDR_real_bound
{ε e0 ê0 e1 ê1 μ0 μ0h μ1 μ1h y θ I0 I1 : ℝ}
(hε : 0 < ε) (he0 : ε ≤ e0) (hê0 : ε ≤ ê0)
(he1 : ε ≤ e1) (hê1 : ε ≤ ê1)
(hI0 : |I0| ≤ 1) (hI1 : |I1| ≤ 1) :
|(μ0h + (I0 / ê0) * (μ1h - μ0h)
+ (I0 * I1 / (ê0 * ê1)) * (y - μ1h) - θ)
- (μ0 + (I0 / e0) * (μ1 - μ0)
+ (I0 * I1 / (e0 * e1)) * (y - μ1) - θ)|
≤ K_seqDR ε *
(|μ0h - μ0| + |μ1h - μ1|
+ (|μ1 - μ0| + |y - μ1|) * |ê0 - e0|
+ |y - μ1| * |ê1 - e1|) := by
have hK1 : 1 ≤ K_seqDR ε := K_seqDR_one_le hε
have hKμ0 : 1 + 1 / ε ≤ K_seqDR ε := K_seqDR_mu0_le hε
have hKμ1 : 1 / ε + 1 / ε ^ 2 ≤ K_seqDR ε := K_seqDR_mu1_le hε
have hK2 : 1 / ε ^ 2 ≤ K_seqDR ε := K_seqDR_inv_sq_le hε
have hK3 : 1 / ε ^ 3 ≤ K_seqDR ε := K_seqDR_inv_cubed_le hε
have hKnonneg : 0 ≤ K_seqDR ε := le_trans zero_le_one hK1
set d0 : ℝ := |μ0h - μ0|
set d1 : ℝ := |μ1h - μ1|
set r0 : ℝ := |μ1 - μ0|
set r1 : ℝ := |y - μ1|
set de0 : ℝ := |ê0 - e0|
set de1 : ℝ := |ê1 - e1|
have hd0 : 0 ≤ d0 := by simp [d0]
have hd1 : 0 ≤ d1 := by simp [d1]
have hr0 : 0 ≤ r0 := by simp [r0]
have hr1 : 0 ≤ r1 := by simp [r1]
have hde0 : 0 ≤ de0 := by simp [de0]
have hde1 : 0 ≤ de1 := by simp [de1]
have hstage0 :
|I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)| ≤
(d1 + d0) / ε + r0 * de0 / ε ^ 2 := by
rw [abs_mul]
have hb := seqDR_stage0_ratio_bound (ε := ε) (e := e0) (ê := ê0)
(μ0 := μ0) (μ0h := μ0h) (μ1 := μ1) (μ1h := μ1h) hε he0 hê0
have hnonneg : 0 ≤ (d1 + d0) / ε + r0 * de0 / ε ^ 2 := by positivity
calc
|I0| * |(μ1h - μ0h) / ê0 - (μ1 - μ0) / e0|
≤ 1 * |(μ1h - μ0h) / ê0 - (μ1 - μ0) / e0| :=
mul_le_mul_of_nonneg_right hI0 (abs_nonneg _)
_ ≤ 1 * ((d1 + d0) / ε + r0 * de0 / ε ^ 2) := by
simpa [d0, d1, r0, de0, add_comm] using hb
_ = (d1 + d0) / ε + r0 * de0 / ε ^ 2 := one_mul _
have hstage1 :
|I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1))| ≤
d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3 := by
rw [abs_mul, abs_mul]
have hI01 : |I0| * |I1| ≤ 1 := by
have hI1nonneg : 0 ≤ |I1| := abs_nonneg _
calc
|I0| * |I1| ≤ 1 * |I1| := mul_le_mul_of_nonneg_right hI0 hI1nonneg
_ ≤ 1 * 1 := mul_le_mul_of_nonneg_left hI1 zero_le_one
_ = 1 := by ring
have hb := seqDR_stage1_ratio_bound (ε := ε) (e0 := e0) (ê0 := ê0)
(e1 := e1) (ê1 := ê1) (y := y) (μ1 := μ1) (μ1h := μ1h)
hε he0 hê0 he1 hê1
calc
|I0| * |I1| * |(y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)|
≤ 1 * |(y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)| :=
mul_le_mul_of_nonneg_right hI01 (abs_nonneg _)
_ ≤ 1 * (d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3) := by
simpa [d1, r1, de0, de1] using hb
_ = d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3 := one_mul _
have hsplit :
((μ0h + (I0 / ê0) * (μ1h - μ0h)
+ (I0 * I1 / (ê0 * ê1)) * (y - μ1h) - θ)
- (μ0 + (I0 / e0) * (μ1 - μ0)
+ (I0 * I1 / (e0 * e1)) * (y - μ1) - θ)) =
(μ0h - μ0)
+ I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)
+ I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)) := by
ring
rw [hsplit]
have hpre :
|(μ0h - μ0)
+ I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)
+ I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1))|
≤ d0 + ((d1 + d0) / ε + r0 * de0 / ε ^ 2) +
(d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3) := by
calc
|(μ0h - μ0)
+ I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)
+ I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1))|
≤ |μ0h - μ0|
+ |I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)|
+ |I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1))| := by
nlinarith [abs_add_le (μ0h - μ0)
(I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0)),
abs_add_le ((μ0h - μ0)
+ I0 * ((μ1h - μ0h) / ê0 - (μ1 - μ0) / e0))
(I0 * I1 * ((y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)))]
_ ≤ d0 + ((d1 + d0) / ε + r0 * de0 / ε ^ 2) +
(d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3) := by
simpa [d0] using add_le_add (add_le_add le_rfl hstage0) hstage1
have htarget :
d0 + ((d1 + d0) / ε + r0 * de0 / ε ^ 2) +
(d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3)
≤ K_seqDR ε * (d0 + d1 + (r0 + r1) * de0 + r1 * de1) := by
have hcoef0 : (1 + 1 / ε) * d0 ≤ K_seqDR ε * d0 :=
mul_le_mul_of_nonneg_right hKμ0 hd0
have hcoef1 : (1 / ε + 1 / ε ^ 2) * d1 ≤ K_seqDR ε * d1 :=
mul_le_mul_of_nonneg_right hKμ1 hd1
have hcross0 : r0 * de0 / ε ^ 2 ≤ K_seqDR ε * (r0 * de0) := by
calc
r0 * de0 / ε ^ 2 = (1 / ε ^ 2) * (r0 * de0) := by ring
_ ≤ K_seqDR ε * (r0 * de0) :=
mul_le_mul_of_nonneg_right hK2 (mul_nonneg hr0 hde0)
have hcross1 : r1 * de0 / ε ^ 3 ≤ K_seqDR ε * (r1 * de0) := by
calc
r1 * de0 / ε ^ 3 = (1 / ε ^ 3) * (r1 * de0) := by ring
_ ≤ K_seqDR ε * (r1 * de0) :=
mul_le_mul_of_nonneg_right hK3 (mul_nonneg hr1 hde0)
have hcross2 : r1 * de1 / ε ^ 3 ≤ K_seqDR ε * (r1 * de1) := by
calc
r1 * de1 / ε ^ 3 = (1 / ε ^ 3) * (r1 * de1) := by ring
_ ≤ K_seqDR ε * (r1 * de1) :=
mul_le_mul_of_nonneg_right hK3 (mul_nonneg hr1 hde1)
calc
d0 + ((d1 + d0) / ε + r0 * de0 / ε ^ 2) +
(d1 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3)
= (1 + 1 / ε) * d0 + (1 / ε + 1 / ε ^ 2) * d1
+ r0 * de0 / ε ^ 2 + r1 * de0 / ε ^ 3 + r1 * de1 / ε ^ 3 := by
ring
_ ≤ K_seqDR ε * d0 + K_seqDR ε * d1
+ K_seqDR ε * (r0 * de0) + K_seqDR ε * (r1 * de0)
+ K_seqDR ε * (r1 * de1) := by
nlinarith
_ = K_seqDR ε * (d0 + d1 + (r0 + r1) * de0 + r1 * de1) := by
ring
exact hpre.trans htarget
theorem seqDR_score_diff_pointwise_bound reviewed
⚑ flagged
Causalean.Estimation.DTR.DTREstimationSystem
Pointwise Lipschitz bound for the sequential DR score difference. Let S be a two-stage dynamic-treatment-regime estimation system with strict overlap at level ε (the true propensity scores lie in [ε, 1-ε]), and let η be a candidate nuisance vector whose estimated propensity components are likewise confined to [ε, 1-ε]. Then, for almost every observation z under the observed-data law S.P_Z, the absolute difference between the sequential doubly-robust moment evaluated at η and at the true nuisance vector η₀ is bounded by the Lipschitz constant K_seqDR ε times the sum of the stage-0 regression error, the stage-1 regression error, and cross terms in which the stage-0 and stage-1 propensity-score errors are weighted by the corresponding outcome/regression residuals.
Formal statement
hypotheses
S :
DTREstimationSystem P δ γ
ε :
ℝ
h_overlap :
S.StrictOverlap ε
η :
DTRNuisanceVec₂ δ γ
hη :
η ∈ DTREstimationSystem.H_ε ε
conclusion
∀ᵐ z ∂S.P_Z,
|S.seqDRMomentFunctional η z S.θ₀ - S.seqDRMomentFunctional S.η₀ z S.θ₀|
≤ K_seqDR ε * (|η.μ₀_fn (projS₀ z) - S.μ₀_val (projS₀ z)| + |η.μ₁_fn (histH₁ z) - S.μ₁_val (histH₁ z)| + (|S.μ₁_val (histH₁ z) - S.μ₀_val (projS₀ z)| + |projY z - S.μ₁_val (histH₁ z)|) * |η.e₀_fn (projS₀ z) - S.e₀_val (projS₀ z)| + |projY z - S.μ₁_val (histH₁ z)| * |η.e₁_fn (histH₁ z) - S.e₁_val (histH₁ z)|)
Proof (Lean source)
theorem seqDR_score_diff_pointwise_bound
(S : DTREstimationSystem P δ γ) {ε : ℝ}
(h_overlap : S.StrictOverlap ε)
(η : DTRNuisanceVec₂ δ γ) (hη : η ∈ DTREstimationSystem.H_ε ε) :
∀ᵐ z ∂S.P_Z,
|S.seqDRMomentFunctional η z S.θ₀ - S.seqDRMomentFunctional S.η₀ z S.θ₀|
≤ K_seqDR ε *
(|η.μ₀_fn (projS₀ z) - S.μ₀_val (projS₀ z)|
+ |η.μ₁_fn (histH₁ z) - S.μ₁_val (histH₁ z)|
+ (|S.μ₁_val (histH₁ z) - S.μ₀_val (projS₀ z)|
+ |projY z - S.μ₁_val (histH₁ z)|)
* |η.e₀_fn (projS₀ z) - S.e₀_val (projS₀ z)|
+ |projY z - S.μ₁_val (histH₁ z)|
* |η.e₁_fn (histH₁ z) - S.e₁_val (histH₁ z)|) := by
rcases h_overlap with ⟨hε_pos, _hε_half, hprop⟩
have h_e_ω : ∀ᵐ ω ∂P.μ,
(ε ≤ S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ∧
S.e₀_val (S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) ≤ 1 - ε)
∧ (ε ≤ 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⟩ ω) ≤ 1 - ε) := by
filter_upwards [hprop, S.e₀_compat, S.e₁_compat] with ω hω hcomp0 hcomp1
rw [hcomp0] at hω
rw [hcomp1] at hω
exact hω
have h_e_z : ∀ᵐ z ∂S.P_Z,
(ε ≤ S.e₀_val (projS₀ z) ∧ S.e₀_val (projS₀ z) ≤ 1 - ε)
∧ (ε ≤ S.e₁_val (histH₁ z) ∧ S.e₁_val (histH₁ z) ≤ 1 - ε) := by
have hset : MeasurableSet
{z : γ 0 × δ × γ 1 × δ × ℝ |
(ε ≤ S.e₀_val (projS₀ z) ∧ S.e₀_val (projS₀ z) ≤ 1 - ε)
∧ (ε ≤ S.e₁_val (histH₁ z) ∧ S.e₁_val (histH₁ z) ≤ 1 - ε)} := by
exact (measurableSet_Icc.preimage (S.e₀_meas.comp measurable_projS₀)).inter
(measurableSet_Icc.preimage (S.e₁_meas.comp measurable_histH₁))
unfold DTREstimationSystem.P_Z
rw [MeasureTheory.ae_map_iff S.measurable_factualZ.aemeasurable hset]
filter_upwards [h_e_ω] with ω hω
simpa [DTREstimationSystem.factualZ, projS₀, histH₁, projS₁, projD₀]
using hω
filter_upwards [h_e_z] with z hz
have hη0 : ε ≤ η.e₀_fn (projS₀ z) := (hη.1 (projS₀ z)).1
have hη1 : ε ≤ η.e₁_fn (histH₁ z) := (hη.2 (histH₁ z)).1
simpa [DTREstimationSystem.seqDRMomentFunctional, seqDRMoment,
DTREstimationSystem.η₀, div_eq_mul_inv, mul_assoc, mul_left_comm, mul_comm] using
(seqDR_real_bound (ε := ε)
(e0 := S.e₀_val (projS₀ z)) (ê0 := η.e₀_fn (projS₀ z))
(e1 := S.e₁_val (histH₁ z)) (ê1 := η.e₁_fn (histH₁ z))
(μ0 := S.μ₀_val (projS₀ z)) (μ0h := η.μ₀_fn (projS₀ z))
(μ1 := S.μ₁_val (histH₁ z)) (μ1h := η.μ₁_fn (histH₁ z))
(y := projY z) (θ := S.θ₀)
(I0 := indEq (projD₀ z) (S.dbar 0)) (I1 := indEq (projD₁ z) (S.dbar 1))
hε_pos hz.1.1 hη0 hz.2.1 hη1
(by
rw [abs_of_nonneg (indEq_nonneg (projD₀ z) (S.dbar 0))]
exact indEq_le_one (projD₀ z) (S.dbar 0))
(by
rw [abs_of_nonneg (indEq_nonneg (projD₁ z) (S.dbar 1))]
exact indEq_le_one (projD₁ z) (S.dbar 1)))
14 supporting declarations (lemmas, instances)
-
indEq_nonneglemma — The real-valued equality indicator is always nonnegative.Proof (Lean source)
-
indEq_le_onelemma — The real-valued equality indicator is always bounded above by one.Proof (Lean source)
-
K_seqDR_one_lelemma — The sequential doubly robust Lipschitz constant dominates one under positive overlap.Proof (Lean source)
lemma K_seqDR_one_le {ε : ℝ} (hε : 0 < ε) : 1 ≤ K_seqDR ε := by unfold K_seqDR field_simp [hε.ne'] nlinarith [sq_nonneg ε, pow_pos hε 3] -
K_seqDR_mu0_lelemma — The sequential doubly robust Lipschitz constant dominates the stage-zero regression coefficient bound.Proof (Lean source)
lemma K_seqDR_mu0_le {ε : ℝ} (hε : 0 < ε) : 1 + 1 / ε ≤ K_seqDR ε := by unfold K_seqDR field_simp [hε.ne'] nlinarith [sq_nonneg ε, pow_pos hε 3] -
K_seqDR_mu1_lelemma — The sequential doubly robust Lipschitz constant dominates the stage-one regression coefficient bound.Proof (Lean source)
lemma K_seqDR_mu1_le {ε : ℝ} (hε : 0 < ε) : 1 / ε + 1 / ε ^ 2 ≤ K_seqDR ε := by unfold K_seqDR field_simp [hε.ne'] nlinarith [sq_nonneg ε, pow_pos hε 3] -
K_seqDR_inv_sq_lelemma — The sequential doubly robust Lipschitz constant dominates the squared inverse-overlap bound.Proof (Lean source)
lemma K_seqDR_inv_sq_le {ε : ℝ} (hε : 0 < ε) : 1 / ε ^ 2 ≤ K_seqDR ε := by unfold K_seqDR field_simp [hε.ne'] nlinarith [sq_nonneg ε, pow_pos hε 3] -
K_seqDR_inv_cubed_lelemma — The sequential doubly robust Lipschitz constant dominates the cubed inverse-overlap bound.Proof (Lean source)
lemma K_seqDR_inv_cubed_le {ε : ℝ} (hε : 0 < ε) : 1 / ε ^ 3 ≤ K_seqDR ε := by unfold K_seqDR field_simp [hε.ne'] nlinarith [sq_nonneg ε, pow_pos hε 3] -
eLpNorm_comp_projS₀_eqlemma — Pulling a stage-zero function back along the full DTR data law preserves its L² norm.hypothesesProof (Lean source)
lemma eLpNorm_comp_projS₀_eq (S : DTREstimationSystem P δ γ) {f : γ 0 → ℝ} (hf : AEStronglyMeasurable f S.P_H₀) : eLpNorm (fun z : γ 0 × δ × γ 1 × δ × ℝ => f (projS₀ z)) 2 S.P_Z = eLpNorm f 2 S.P_H₀ := by have hfmap : AEStronglyMeasurable f (S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z)) := by simpa [P_Z_map_projS₀_eq_P_H₀ S] using hf rw [← P_Z_map_projS₀_eq_P_H₀ S] simpa [Function.comp_def] using (MeasureTheory.eLpNorm_map_measure (μ := S.P_Z) (f := fun z : γ 0 × δ × γ 1 × δ × ℝ => projS₀ z) (g := f) (p := 2) hfmap measurable_projS₀.aemeasurable).symm -
eLpNorm_comp_histH₁_eqlemma — Pulling a stage-one history function back along the full DTR data law preserves its L² norm.hypothesesProof (Lean source)
lemma eLpNorm_comp_histH₁_eq (S : DTREstimationSystem P δ γ) {f : γ 1 × δ × γ 0 → ℝ} (hf : AEStronglyMeasurable f S.P_H₁) : eLpNorm (fun z : γ 0 × δ × γ 1 × δ × ℝ => f (histH₁ z)) 2 S.P_Z = eLpNorm f 2 S.P_H₁ := by have hfmap : AEStronglyMeasurable f (S.P_Z.map (fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z)) := by simpa [P_Z_map_histH₁_eq_P_H₁ S] using hf rw [← P_Z_map_histH₁_eq_P_H₁ S] simpa [Function.comp_def] using (MeasureTheory.eLpNorm_map_measure (μ := S.P_Z) (f := fun z : γ 0 × δ × γ 1 × δ × ℝ => histH₁ z) (g := f) (p := 2) hfmap measurable_histH₁.aemeasurable).symm -
residual_mul_error_isLittleOp_onetheorem — Multiplying an L²-convergent error by a fixed square-integrable residual still gives a stochastic little-o L² norm.hypothesesα :R :α → ℝhR_meas :hR_nonneg :∀ z, 0 ≤ R zhR_memLp :MemLp R 2 νdeZ :ℕ → P.Ω → α → ℝhdeZ_memLp :∀ n ω, MemLp (deZ n ω) 2 νhdeZ_meas :∀ n ω, Measurable (deZ n ω)hdeZ_bdd :∀ n ω z, |deZ n ω z| ≤ 1hdeZ_rate :IsLittleOp (fun n ω => (eLpNorm (deZ n ω) 2 ν).toReal) (fun _ => (1 : ℝ)) P.μconclusionIsLittleOp (fun n ω => (eLpNorm (fun z => R z * |deZ n ω z|) 2 ν).toReal) (fun _ => (1 : ℝ)) P.μProof (Lean source)
theorem residual_mul_error_isLittleOp_one {α : Type*} [MeasurableSpace α] {ν : Measure α} [IsProbabilityMeasure ν] {R : α → ℝ} (hR_meas : Measurable R) (hR_nonneg : ∀ z, 0 ≤ R z) (hR_memLp : MemLp R 2 ν) {deZ : ℕ → P.Ω → α → ℝ} (hdeZ_memLp : ∀ n ω, MemLp (deZ n ω) 2 ν) (hdeZ_meas : ∀ n ω, Measurable (deZ n ω)) (hdeZ_bdd : ∀ n ω z, |deZ n ω z| ≤ 1) (hdeZ_rate : IsLittleOp (fun n ω => (eLpNorm (deZ n ω) 2 ν).toReal) (fun _ => (1 : ℝ)) P.μ) : IsLittleOp (fun n ω => (eLpNorm (fun z => R z * |deZ n ω z|) 2 ν).toReal) (fun _ => (1 : ℝ)) P.μ := by classical intro δ hδ rw [ENNReal.tendsto_nhds_zero] intro κ hκ by_cases hκtop : κ = ⊤ · filter_upwards with n simp [hκtop] let τ : ℝ := δ / 4 have hτpos : 0 < τ := by dsimp [τ] linarith obtain ⟨M, hMpos, hMtail⟩ := hR_memLp.eLpNorm_indicator_norm_ge_pos_le hR_meas.stronglyMeasurable hτpos let tail : α → ℝ := {z | M ≤ R z}.indicator R have htail_set : MeasurableSet {z : α | M ≤ R z} := measurableSet_le measurable_const hR_meas have htail_memLp : MemLp tail 2 ν := hR_memLp.indicator htail_set have htail_norm_le : (eLpNorm tail 2 ν).toReal ≤ τ := by have hle : eLpNorm tail 2 ν ≤ ofReal τ := by have htail_eq : tail = ({z : α | M ≤ ‖R z‖₊}.indicator R) := by funext z by_cases hz : M ≤ R z · simp [tail, hz, Real.norm_eq_abs, abs_of_nonneg (hR_nonneg z)] · simp [tail, hz, Real.norm_eq_abs, abs_of_nonneg (hR_nonneg z)] simpa [htail_eq] using hMtail calc (eLpNorm tail 2 ν).toReal ≤ (ofReal τ).toReal := ENNReal.toReal_mono ENNReal.ofReal_ne_top hle _ = τ := ENNReal.toReal_ofReal hτpos.le have hcross_bound : ∀ n ω, (eLpNorm (fun z : α => R z * |deZ n ω z|) 2 ν).toReal ≤ M * (eLpNorm (deZ n ω) 2 ν).toReal + τ := by intro n ω let bulk : α → ℝ := fun z => M * |deZ n ω z| let upper : α → ℝ := fun z => bulk z + tail z have hbulk_memLp : MemLp bulk 2 ν := by have h_abs : MemLp (fun z => |deZ n ω z|) 2 ν := by simpa [Real.norm_eq_abs] using (hdeZ_memLp n ω).norm exact h_abs.const_smul M have hupper_memLp : MemLp upper 2 ν := by exact hbulk_memLp.add htail_memLp have hpoint : ∀ z, ‖R z * |deZ n ω z|‖ ≤ upper z := by intro z have hRz : 0 ≤ R z := hR_nonneg z have hdez_nonneg : 0 ≤ |deZ n ω z| := abs_nonneg _ have hdez_le : |deZ n ω z| ≤ 1 := hdeZ_bdd n ω z by_cases hz : M ≤ R z · have htail_eq : tail z = R z := by simp [tail, hz] have hmain : ‖R z * |deZ n ω z|‖ ≤ R z := by rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hRz, abs_of_nonneg hdez_nonneg] exact mul_le_of_le_one_right hRz hdez_le dsimp [upper, bulk] rw [htail_eq] have hbulk_nonneg : 0 ≤ M * |deZ n ω z| := mul_nonneg hMpos.le hdez_nonneg exact hmain.trans (by nlinarith) · have htail_eq : tail z = 0 := by simp [tail, hz] have hR_le_M : R z ≤ M := le_of_not_ge hz have hmain : ‖R z * |deZ n ω z|‖ ≤ M * |deZ n ω z| := by rw [Real.norm_eq_abs, abs_mul, abs_of_nonneg hRz, abs_of_nonneg hdez_nonneg] exact mul_le_mul_of_nonneg_right hR_le_M hdez_nonneg dsimp [upper, bulk] rw [htail_eq] simpa using hmain have hmono : lpNorm (fun z : α => R z * |deZ n ω z|) 2 ν ≤ lpNorm upper 2 ν := lpNorm_mono_real hupper_memLp hpoint have htri : lpNorm upper 2 ν ≤ lpNorm bulk 2 ν + lpNorm tail 2 ν := by exact lpNorm_add_le (f := bulk) (g := tail) (μ := ν) hbulk_memLp (by norm_num : (1 : ENNReal) ≤ 2) have hbulk_norm : lpNorm bulk 2 ν = M * (eLpNorm (deZ n ω) 2 ν).toReal := by change lpNorm (M • (fun z : α => |deZ n ω z|)) 2 ν = M * (eLpNorm (deZ n ω) 2 ν).toReal rw [lpNorm_const_smul] rw [lpNorm_fun_abs (hdeZ_memLp n ω).aestronglyMeasurable] rw [← toReal_eLpNorm (hdeZ_memLp n ω).aestronglyMeasurable] have hcoef : (↑‖M‖₊ : ℝ) = M := by simp [Real.norm_eq_abs, abs_of_pos hMpos] rw [hcoef] have htail_lp : lpNorm tail 2 ν = (eLpNorm tail 2 ν).toReal := by rw [toReal_eLpNorm htail_memLp.aestronglyMeasurable] calc (eLpNorm (fun z : α => R z * |deZ n ω z|) 2 ν).toReal = lpNorm (fun z : α => R z * |deZ n ω z|) 2 ν := by have h_abs : Measurable (fun z : α => |deZ n ω z|) := by simpa [Function.comp_def] using (continuous_abs.measurable.comp (hdeZ_meas n ω)) rw [toReal_eLpNorm (hR_meas.fun_mul h_abs).aestronglyMeasurable] _ ≤ lpNorm upper 2 ν := hmono _ ≤ lpNorm bulk 2 ν + lpNorm tail 2 ν := htri _ = M * (eLpNorm (deZ n ω) 2 ν).toReal + (eLpNorm tail 2 ν).toReal := by rw [hbulk_norm, htail_lp] _ ≤ M * (eLpNorm (deZ n ω) 2 ν).toReal + τ := add_le_add_right htail_norm_le (M * (eLpNorm (deZ n ω) 2 ν).toReal) have hsmall := (ENNReal.tendsto_nhds_zero.mp (hdeZ_rate (δ / (2 * M)) (by positivity))) κ hκ filter_upwards [hsmall] with n hn refine (measure_mono ?_).trans hn intro ω hω have hnorm_nonneg : 0 ≤ (eLpNorm (fun z : α => R z * |deZ n ω z|) 2 ν).toReal := ENNReal.toReal_nonneg have hlt_norm : δ < (eLpNorm (fun z : α => R z * |deZ n ω z|) 2 ν).toReal := by simpa [abs_of_nonneg hnorm_nonneg] using hω have hde_large : δ / (2 * M) < (eLpNorm (deZ n ω) 2 ν).toReal := by have hb := hcross_bound n ω by_contra hnot have hle : (eLpNorm (deZ n ω) 2 ν).toReal ≤ δ / (2 * M) := le_of_not_gt hnot have hprod_le : M * (eLpNorm (deZ n ω) 2 ν).toReal ≤ δ / 2 := by calc M * (eLpNorm (deZ n ω) 2 ν).toReal ≤ M * (δ / (2 * M)) := mul_le_mul_of_nonneg_left hle hMpos.le _ = δ / 2 := by field_simp [hMpos.ne'] have hcross_le : (eLpNorm (fun z : α => R z * |deZ n ω z|) 2 ν).toReal ≤ δ / 2 + τ := by exact hb.trans (add_le_add hprod_le le_rfl) dsimp [τ] at hcross_le nlinarith have hde_nonneg : 0 ≤ (eLpNorm (deZ n ω) 2 ν).toReal := ENNReal.toReal_nonneg simpa [abs_of_nonneg hde_nonneg] using hde_large -
seqDR_stage0_ratio_boundlemma — The stage-zero weighted regression contrast is Lipschitz in the stage-zero nuisance errors under overlap.hypothesesε e ê μ0 μ0h μ1 μ1h :ℝhε :0 < εhe :ε ≤ ehê :ε ≤ êconclusion|(μ1h - μ0h) / ê - (μ1 - μ0) / e|≤ (|μ1h - μ1| + |μ0h - μ0|) / ε + |μ1 - μ0| * |ê - e| / ε ^ 2Proof (Lean source)
lemma seqDR_stage0_ratio_bound {ε e ê μ0 μ0h μ1 μ1h : ℝ} (hε : 0 < ε) (he : ε ≤ e) (hê : ε ≤ ê) : |(μ1h - μ0h) / ê - (μ1 - μ0) / e| ≤ (|μ1h - μ1| + |μ0h - μ0|) / ε + |μ1 - μ0| * |ê - e| / ε ^ 2 := by have he_pos : 0 < e := lt_of_lt_of_le hε he have hê_pos : 0 < ê := lt_of_lt_of_le hε hê have he_ne : e ≠ 0 := he_pos.ne' have hê_ne : ê ≠ 0 := hê_pos.ne' have hεsq_pos : 0 < ε ^ 2 := sq_pos_of_pos hε have hprod_pos : 0 < ê * e := mul_pos hê_pos he_pos have hmul : ε ^ 2 ≤ ê * e := by nlinarith [mul_le_mul hê he hε.le hê_pos.le] have hid : (μ1h - μ0h) / ê - (μ1 - μ0) / e = ((μ1h - μ1) - (μ0h - μ0)) / ê - (μ1 - μ0) * (ê - e) / (ê * e) := by field_simp [hê_ne, he_ne] ring rw [hid] calc |((μ1h - μ1) - (μ0h - μ0)) / ê - (μ1 - μ0) * (ê - e) / (ê * e)| ≤ |((μ1h - μ1) - (μ0h - μ0)) / ê| + |(μ1 - μ0) * (ê - e) / (ê * e)| := abs_sub _ _ _ = |(μ1h - μ1) - (μ0h - μ0)| / ê + |μ1 - μ0| * |ê - e| / (ê * e) := by rw [abs_div, abs_of_pos hê_pos, abs_div, abs_mul, abs_of_pos hprod_pos] _ ≤ (|μ1h - μ1| + |μ0h - μ0|) / ε + |μ1 - μ0| * |ê - e| / ε ^ 2 := by have hnum : |(μ1h - μ1) - (μ0h - μ0)| ≤ |μ1h - μ1| + |μ0h - μ0| := abs_sub _ _ have hterm1 : |(μ1h - μ1) - (μ0h - μ0)| / ê ≤ (|μ1h - μ1| + |μ0h - μ0|) / ε := by rw [div_eq_mul_inv, div_eq_mul_inv] exact (mul_le_mul hnum ((inv_le_inv₀ hê_pos hε).2 hê) (inv_nonneg.mpr hê_pos.le) (by positivity)) have hterm2 : |μ1 - μ0| * |ê - e| / (ê * e) ≤ |μ1 - μ0| * |ê - e| / ε ^ 2 := by rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_left ((inv_le_inv₀ hprod_pos hεsq_pos).2 hmul) (mul_nonneg (abs_nonneg _) (abs_nonneg _)) exact add_le_add hterm1 hterm2 -
seqDR_stage1_ratio_boundlemma — The stage-one weighted residual contrast is Lipschitz in the stage-one regression error and both propensity errors under overlap.hypothesesε e0 ê0 e1 ê1 y μ1 μ1h :ℝhε :0 < εhe0 :ε ≤ e0hê0 :ε ≤ ê0he1 :ε ≤ e1hê1 :ε ≤ ê1conclusion|(y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)|≤ |μ1h - μ1| / ε ^ 2 + |y - μ1| * |ê0 - e0| / ε ^ 3 + |y - μ1| * |ê1 - e1| / ε ^ 3Proof (Lean source)
lemma seqDR_stage1_ratio_bound {ε e0 ê0 e1 ê1 y μ1 μ1h : ℝ} (hε : 0 < ε) (he0 : ε ≤ e0) (hê0 : ε ≤ ê0) (he1 : ε ≤ e1) (hê1 : ε ≤ ê1) : |(y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1)| ≤ |μ1h - μ1| / ε ^ 2 + |y - μ1| * |ê0 - e0| / ε ^ 3 + |y - μ1| * |ê1 - e1| / ε ^ 3 := by have he0_pos : 0 < e0 := lt_of_lt_of_le hε he0 have hê0_pos : 0 < ê0 := lt_of_lt_of_le hε hê0 have he1_pos : 0 < e1 := lt_of_lt_of_le hε he1 have hê1_pos : 0 < ê1 := lt_of_lt_of_le hε hê1 have hprod_hat_pos : 0 < ê0 * ê1 := mul_pos hê0_pos hê1_pos have hprod_true_pos : 0 < e0 * e1 := mul_pos he0_pos he1_pos have hden0_pos : 0 < ê0 * e0 * ê1 := mul_pos (mul_pos hê0_pos he0_pos) hê1_pos have hden1_pos : 0 < e0 * ê1 * e1 := mul_pos (mul_pos he0_pos hê1_pos) he1_pos have hprod_hat_ne : ê0 * ê1 ≠ 0 := hprod_hat_pos.ne' have hprod_true_ne : e0 * e1 ≠ 0 := hprod_true_pos.ne' have hεsq_pos : 0 < ε ^ 2 := sq_pos_of_pos hε have hεcub_pos : 0 < ε ^ 3 := pow_pos hε 3 have hprod_hat_ge : ε ^ 2 ≤ ê0 * ê1 := by nlinarith [mul_le_mul hê0 hê1 hε.le hê0_pos.le] have hden0_ge : ε ^ 3 ≤ ê0 * e0 * ê1 := by nlinarith [mul_le_mul (mul_le_mul hê0 he0 hε.le hê0_pos.le) hê1 hε.le (mul_pos hê0_pos he0_pos).le] have hden1_ge : ε ^ 3 ≤ e0 * ê1 * e1 := by nlinarith [mul_le_mul (mul_le_mul he0 hê1 hε.le he0_pos.le) he1 hε.le (mul_pos he0_pos hê1_pos).le] have hid : (y - μ1h) / (ê0 * ê1) - (y - μ1) / (e0 * e1) = - (μ1h - μ1) / (ê0 * ê1) - (y - μ1) * (ê0 - e0) / (ê0 * e0 * ê1) - (y - μ1) * (ê1 - e1) / (e0 * ê1 * e1) := by field_simp [hprod_hat_ne, hprod_true_ne, hê0_pos.ne', he0_pos.ne', hê1_pos.ne', he1_pos.ne'] ring rw [hid] calc |- (μ1h - μ1) / (ê0 * ê1) - (y - μ1) * (ê0 - e0) / (ê0 * e0 * ê1) - (y - μ1) * (ê1 - e1) / (e0 * ê1 * e1)| ≤ |-(μ1h - μ1) / (ê0 * ê1) - (y - μ1) * (ê0 - e0) / (ê0 * e0 * ê1)| + |(y - μ1) * (ê1 - e1) / (e0 * ê1 * e1)| := abs_sub _ _ _ ≤ |-(μ1h - μ1) / (ê0 * ê1)| + |(y - μ1) * (ê0 - e0) / (ê0 * e0 * ê1)| + |(y - μ1) * (ê1 - e1) / (e0 * ê1 * e1)| := by nlinarith [abs_sub (-(μ1h - μ1) / (ê0 * ê1)) ((y - μ1) * (ê0 - e0) / (ê0 * e0 * ê1))] _ = |μ1h - μ1| / (ê0 * ê1) + |y - μ1| * |ê0 - e0| / (ê0 * e0 * ê1) + |y - μ1| * |ê1 - e1| / (e0 * ê1 * e1) := by rw [abs_div, abs_neg, abs_of_pos hprod_hat_pos] rw [abs_div, abs_mul, abs_of_pos hden0_pos] rw [abs_div, abs_mul, abs_of_pos hden1_pos] _ ≤ |μ1h - μ1| / ε ^ 2 + |y - μ1| * |ê0 - e0| / ε ^ 3 + |y - μ1| * |ê1 - e1| / ε ^ 3 := by have h1 : |μ1h - μ1| / (ê0 * ê1) ≤ |μ1h - μ1| / ε ^ 2 := by rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_left ((inv_le_inv₀ hprod_hat_pos hεsq_pos).2 hprod_hat_ge) (abs_nonneg _) have h2 : |y - μ1| * |ê0 - e0| / (ê0 * e0 * ê1) ≤ |y - μ1| * |ê0 - e0| / ε ^ 3 := by rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_left ((inv_le_inv₀ hden0_pos hεcub_pos).2 hden0_ge) (mul_nonneg (abs_nonneg _) (abs_nonneg _)) have h3 : |y - μ1| * |ê1 - e1| / (e0 * ê1 * e1) ≤ |y - μ1| * |ê1 - e1| / ε ^ 3 := by rw [div_eq_mul_inv, div_eq_mul_inv] exact mul_le_mul_of_nonneg_left ((inv_le_inv₀ hden1_pos hεcub_pos).2 hden1_ge) (mul_nonneg (abs_nonneg _) (abs_nonneg _)) nlinarith -
μ₀_val_memLplemma — The true stage-zero regression representative is square-integrable under the stage-zero history marginal.hypothesesS :DTREstimationSystem P δ γhA :S.toPODTRSystem.Assumptionsh_yd2 :∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μconclusionMemLp S.μ₀_val 2 S.P_H₀Proof (Lean source)
lemma μ₀_val_memLp (S : DTREstimationSystem P δ γ) (hA : S.toPODTRSystem.Assumptions) (h_yd2 : ∀ dbar : Fin 2 → δ, Integrable (fun ω => (S.toPODTRSystem.Y_of dbar ω) ^ 2) P.μ) : 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) 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 have hcomp_L2 : MemLp (fun ω => S.μ₀_val (S.toPODTRSystem.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.toPODTRSystem.measurable_factualS ⟨0, by decide⟩).aemeasurable).2 hcomp_L2 -
μ₁_val_memLplemma — The true stage-one regression representative is square-integrable under the stage-one history marginal.hypothesesS :DTREstimationSystem P δ γε :ℝh_overlap :S.StrictOverlap εh_y2 :Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μconclusionMemLp S.μ₁_val 2 S.P_H₁Proof (Lean source)
lemma μ₁_val_memLp (S : DTREstimationSystem P δ γ) {ε : ℝ} (h_overlap : S.StrictOverlap ε) (h_y2 : Integrable (fun ω => (S.toPODTRSystem.factualY ω) ^ 2) P.μ) : MemLp S.μ₁_val 2 S.P_H₁ := by let H1 : P.Ω → γ 1 × δ × γ 0 := fun ω => (S.toPODTRSystem.factualS ⟨1, by decide⟩ ω, S.toPODTRSystem.factualD ⟨0, by decide⟩ ω, S.toPODTRSystem.factualS ⟨0, by decide⟩ ω) have hH1_meas : Measurable H1 := by dsimp [H1] exact (S.toPODTRSystem.measurable_factualS ⟨1, by decide⟩).prod ((S.toPODTRSystem.measurable_factualD ⟨0, by decide⟩).prod (S.toPODTRSystem.measurable_factualS ⟨0, by decide⟩)) have 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