Estimation.PLR
Partially linear regression DML: Robinson partialling-out scores, nuisance bundles, mean-zero and remainder facts, Jacobian consistency, and one-step plus feasible asymptotic normality.
Nuisance 2 core · 8 supporting This file packages the two partially-linear-model nuisance functions — the outcome regression lFn and the treatment regression mFn — together with their measurability witnesses into a single type PLRNuisance, and equips ★ ext
Bundled nuisance space for the partially linear model
This file packages the two partially-linear-model nuisance functions — the
outcome regression lFn and the treatment regression mFn — together with
their measurability witnesses into a single type PLRNuisance, and equips it
with componentwise real-vector-space structure. This bundled nuisance space is
the nuisance space used by the partially linear double-machine-learning moment
instance.
structure PLRNuisance reviewed
⚑ flagged
Causalean.Estimation.PLR
A partially linear nuisance bundles an outcome regression and a treatment regression on the covariates, requiring each to be measurable.
Definition (Lean source)
parameters
γ :
Type*
fields
theorem ext reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRNuisance
Two nuisance pairs η and η' are equal whenever their outcome-regression components agree at every covariate value and their treatment-regression components agree at every covariate value, so the two pairs are equal.
Formal statement
hypotheses
conclusion
η = η'
Proof (Lean source)
@[ext]
theorem ext {η η' : PLRNuisance γ}
(hl : ∀ x, η.lFn x = η'.lFn x)
(hm : ∀ x, η.mFn x = η'.mFn x) : η = η' := by
cases η
cases η'
simp only at hl hm
congr
· funext x
exact hl x
· funext x
exact hm x
8 supporting declarations (lemmas, instances)
-
instZeroinstance — For every covariate space equipped with a $\sigma$-algebra, the zero operation on partially linear nuisance pairs assigns the pair whose outcome and treatment regressions are both identically zero.parametersγ :sharedType u_1instancegiven byzero := ⟨fun _ => 0, fun _ => 0, measurable_const, measurable_const⟩ -
instAddinstance — For every covariate space equipped with a $\sigma$-algebra, the addition operation on partially linear nuisance pairs assigns to each pair of nuisance pairs the pair obtained by adding their outcome regressions and their treatment regressions pointwise.parametersγ :sharedType u_1instancegiven byadd η η' := ⟨fun x=> η.lFn x+ η'.lFn x, fun x => η.mFn x+ η'.mFn x, η.lMeas.add η'.lMeas, η.mMeas.add η'.mMeas⟩ -
instNeginstance — For every covariate space equipped with a $\sigma$-algebra, the negation operation on partially linear nuisance pairs assigns to each nuisance pair the pair obtained by negating both regressions pointwise.parametersγ :sharedType u_1instancegiven byneg η := ⟨fun x => -η.lFn x, fun x => -η.mFn x, η.lMeas.neg, η.mMeas.neg⟩ -
instSubinstance — For every covariate space equipped with a $\sigma$-algebra, the subtraction operation on partially linear nuisance pairs assigns to each ordered pair of nuisance pairs the pair obtained by subtracting their outcome regressions and their treatment regressions pointwise.parametersγ :sharedType u_1instancegiven bysub η η' := ⟨fun x=> η.lFn x- η'.lFn x, fun x => η.mFn x- η'.mFn x, η.lMeas.sub η'.lMeas, η.mMeas.sub η'.mMeas⟩ -
instSMulRealinstance — For every covariate space equipped with a $\sigma$-algebra, the real-scalar multiplication operation on partially linear nuisance pairs assigns to every real scalar and nuisance pair the pair obtained by multiplying both regressions pointwise by that scalar.parametersγ :sharedType u_1instancegiven bysmul t η := ⟨fun x=> t * η.lFn x, fun x => t * η.mFn x, measurable_const.mul η.lMeas, measurable_const.mul η.mMeas⟩ -
ext_ifftheorem∀ {γ : Type u_1} [inst : MeasurableSpace γ] {η η' : PLRNuisance γ}, η = η' ↔ (∀ (x : γ), η.lFn x = η'.lFn x) ∧ ∀ (x : γ), η.mFn x = η'.mFn xProof (Lean source)
@[ext] -
instAddCommGroupinstance — For every covariate space equipped with a $\sigma$-algebra, the additive commutative group structure on partially linear nuisance pairs supplies the zero pair, componentwise addition, componentwise negation, componentwise subtraction, repeated addition by natural numbers, repeated addition and negation by integers, the zero-multiple law, the successor-multiple law, the zero integer-multiple law, the positive successor integer-multiple law, the negative successor integer-multiple law, subtraction as addition of a negative, associativity of addition, the left zero law, the right zero law, cancellation of a pair with its negative, and commutativity of addition.parametersγ :sharedType u_1instancegiven 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 x · exact sub_eq_add_neg (η.lFn x) (η'.lFn x) · exact sub_eq_add_neg (η.mFn x) (η'.mFn x)clause 13add_assoc η η' η'' := by apply ext <;> intro x · exact add_assoc (η.lFn x) (η'.lFn x) (η''.lFn x) · exact add_assoc (η.mFn x) (η'.mFn x) (η''.mFn x)clause 14zero_add η := by apply ext <;> intro x · exact zero_add (η.lFn x) · exact zero_add (η.mFn x)clause 15add_zero η := by apply ext <;> intro x · exact add_zero (η.lFn x) · exact add_zero (η.mFn x)clause 16neg_add_cancel η := by apply ext <;> intro x · exact neg_add_cancel (η.lFn x) · exact neg_add_cancel (η.mFn x)clause 17add_comm η η' := by apply ext <;> intro x · exact add_comm (η.lFn x) (η'.lFn x) · exact add_comm (η.mFn x) (η'.mFn x) -
instModuleRealinstance — For every covariate space equipped with a $\sigma$-algebra, the real vector-space structure on partially linear nuisance pairs supplies the scalar multiplication operation, the unit-scalar law, the successive-scalar law, the scalar-times-zero law, distributivity of scalar multiplication over addition of nuisance pairs, distributivity over addition of scalars, and the zero-scalar law.parametersγ :sharedType u_1instancegiven byclause 1smul := (· • ·)clause 2one_smul η := by apply ext <;> intro x · change (1 : ℝ) * η.lFn x= η.lFn x exact one_mul _ · change (1 : ℝ) * η.mFn x = η.mFn x exact one_mul _clause 3mul_smul t u η := by apply ext <;> intro x · change (t * u) * η.lFn x= t * (u * η.lFn x) ring · change (t * u) * η.mFn x = t * (u * η.mFn x) ringclause 4smul_zero t := by apply ext <;> intro x · change t * (0 : ℝ)= 0 exact mul_zero t · change t * (0 : ℝ) = 0 exact mul_zero tclause 5smul_add t η η' := by apply ext <;> intro x · change t * (η.lFn x + η'.lFn x)= t * η.lFn x+ t * η'.lFn x ring · change t * (η.mFn x + η'.mFn x) = t * η.mFn x+ t * η'.mFn x ringclause 6add_smul t u η := by apply ext <;> intro x · change (t + u) * η.lFn x= t * η.lFn x+ u * η.lFn x ring · change (t + u) * η.mFn x = t * η.mFn x+ u * η.mFn x ringclause 7zero_smul η := by apply ext <;> intro x · change (0 : ℝ) * η.lFn x= 0 exact zero_mul _ · change (0 : ℝ) * η.mFn x = 0 exact zero_mul _
Moment 5 core · 4 supporting This file provides the partialling-out moment functional for the partially linear model, its decomposition into the linear-in-parameter form, and the measurability of these maps in the data. ★ plrMoment_decomp
Partially linear orthogonal score
This file provides the partialling-out moment functional for the partially linear model, its decomposition into the linear-in-parameter form, and the measurability of these maps in the data. The score is linear in the structural slope, with coefficient minus the squared treatment residual and constant term given by the residualized outcome times the treatment residual.
def plrResidual reviewed
⚑ flagged
Causalean.Estimation.PLR
For a measurable covariate space, a pair of outcome and treatment regression functions, and an observed covariate, treatment, and outcome triple, the partially linear treatment residual is the observed treatment minus its treatment-regression prediction.
Definition (Lean source)
parameters
def
plrResidual η z :
ℝ
given by
z.2.1 - η.mFn z.1
def plrMomentFunctional reviewed
⚑ flagged
Causalean.Estimation.PLR
For a measurable covariate space, a pair of outcome and treatment regression functions, an observed covariate, treatment, and outcome triple, and a real-valued structural slope, the Robinson partialling-out score is the product of the treatment residual and the outcome residual after subtracting that slope times the treatment residual.
Definition (Lean source)
parameters
def
plrMomentFunctional η z θ :
ℝ
given by
(z.2.2 - η.lFn z.1 - θ * plrResidual η z) * plrResidual η z
def plrMomentA reviewed
⚑ flagged
Causalean.Estimation.PLR
For a measurable covariate space, a pair of outcome and treatment regression functions, and an observed covariate, treatment, and outcome triple, the coefficient of the partially linear score that is linear in the structural slope is minus the squared treatment residual.
Definition (Lean source)
def plrMomentB reviewed
⚑ flagged
Causalean.Estimation.PLR
For a measurable covariate space, a pair of outcome and treatment regression functions, and an observed covariate, treatment, and outcome triple, the constant term in the partially linear score is the product of the treatment residual and the outcome minus its outcome-regression prediction.
Definition (Lean source)
lemma plrMoment_decomp reviewed
⚑ flagged
Causalean.Estimation.PLR
Robinson score decomposition. The partialling-out score decomposes into its linear coefficient in θ times the target parameter θ plus a constant term.
Formal statement
hypotheses
conclusion
Proof (Lean source)
lemma plrMoment_decomp (η : PLRNuisance γ) (z : γ × ℝ × ℝ) (θ : ℝ) :
plrMomentFunctional η z θ = plrMomentA η z * θ + plrMomentB η z := by
simp only [plrMomentFunctional, plrMomentA, plrMomentB]
ring
4 supporting declarations (lemmas, instances)
-
measurable_plrResiduallemma — The treatment residual is measurable as a function of the observed data.Proof (Lean source)
@[fun_prop] lemma measurable_plrResidual (η : PLRNuisance γ) : Measurable (fun z : γ × ℝ × ℝ => plrResidual η z) := (measurable_fst.comp measurable_snd).sub (η.mMeas.comp measurable_fst) -
measurable_plrMomentFunctionallemma — The Robinson partialling-out score is measurable in the observed data.hypothesesconclusionMeasurable (fun z : γ × ℝ × ℝ => plrMomentFunctional η z θ)Proof (Lean source)
@[fun_prop] lemma measurable_plrMomentFunctional (η : PLRNuisance γ) (θ : ℝ) : Measurable (fun z : γ × ℝ × ℝ => plrMomentFunctional η z θ) := by have hv := measurable_plrResidual η have hy : Measurable (fun z : γ × ℝ × ℝ => z.2.2) := by fun_prop exact (((hy.sub (η.lMeas.comp measurable_fst)).sub (hv.const_mul θ)).mul hv) -
measurable_plrMomentAlemma — The linear-score coefficient is measurable in the observed data.Proof (Lean source)
@[fun_prop] lemma measurable_plrMomentA (η : PLRNuisance γ) : Measurable (fun z : γ × ℝ × ℝ => plrMomentA η z) := by have hv := measurable_plrResidual η exact (hv.pow_const 2).neg -
measurable_plrMomentBlemma — The linear-score constant term is measurable in the observed data.Proof (Lean source)
@[fun_prop] lemma measurable_plrMomentB (η : PLRNuisance γ) : Measurable (fun z : γ × ℝ × ℝ => plrMomentB η z) := by have hv := measurable_plrResidual η have hy : Measurable (fun z : γ × ℝ × ℝ => z.2.2) := by fun_prop exact (hy.sub (η.lMeas.comp measurable_fst)).mul hv
Setup 9 core · 4 supporting This file provides the value-space estimation system carrying the regression representatives, the joint observed-data law, and the GeneralMoment instance of the abstract DML framework. ★ plrMomentFunctional_factualZ
Partially linear DML estimation system
This file provides the value-space estimation system carrying the regression
representatives, the joint observed-data law, and the GeneralMoment instance of
the abstract DML framework. The main declarations are PLRSystem,
PLRSystem.factualZ, PLRSystem.P_Z, PLRSystem.P_X, PLRSystem.η₀,
PLRSystem.θ₀, PLRSystem.residSecondMoment, PLRSystem.plrGeneralMoment, and
the change-of-variables helper PLRSystem.integral_P_Z. The resulting partially
linear moment has a DGP-dependent Jacobian equal to minus the residual treatment
variance; sibling files prove the mean-zero, finite-variance, score-L², and
doubly-robust remainder facts used for structural-slope DML normality.
structure PLRSystem reviewed
⚑ flagged
Causalean.Estimation.PLR
A partially linear estimation system extends a partially linear causal model with value-space regression representatives — an outcome-regression representative and a treatment-regression representative on the covariates — subject to: each representative is measurable; the outcome representative agrees almost surely with the conditional mean of the outcome given the covariates and the treatment representative agrees almost surely with the conditional mean of the treatment given the covariates; and the treatment retains nonzero variation after partialling out the covariate, which is what makes the partialling-out Jacobian invertible.
Definition (Lean source)
parameters
fields
Value-space outcome regression `ℓ_val(x)` (the conditional mean of `Y` as a
function of the covariate value).
lVal :
γ → ℝ
The outcome regression representative is measurable.
lVal_meas :
Measurable lVal
Value-space treatment regression `m_val(x)`.
mVal :
γ → ℝ
The treatment regression representative is measurable.
mVal_meas :
Measurable mVal
`ℓ_val` represents the outcome regression: `ℓ_val(X) = E[Y | σ(X)]` a.s.
lVal_compat :
(fun ω => lVal (toPOPartialLinearSystem.factualX ω)) =ᵐ[P.μ] toPOPartialLinearModel.lReg
`m_val` represents the treatment regression: `m_val(X) = E[D | σ(X)]` a.s.
mVal_compat :
(fun ω => mVal (toPOPartialLinearSystem.factualX ω)) =ᵐ[P.μ] toPOPartialLinearModel.mReg
Nondegeneracy: the treatment retains variation after partialling out the
covariate, `E[(D − m_val(X))²] ≠ 0`. This is what makes the partialling-out
Jacobian invertible.
nondegenerate :
∫ ω, (toPOPartialLinearSystem.factualD ω - mVal (toPOPartialLinearSystem.factualX ω)) ^ 2 ∂P.μ
≠ 0
def factualZ reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the observed-data map assigns every population unit its covariate, factual treatment, and factual outcome, in that order.
def P_Z reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the joint observed-data measure is the population measure transported through the map that records each unit's covariate, factual treatment, and factual outcome.
def P_X reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the covariate marginal measure is the population measure transported through the factual covariate map.
def η₀ reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the true nuisance pair consists of that system's value-space outcome regression and treatment regression.
Definition (Lean source)
parameters
def
given by
⟨S.lVal, S.mVal, S.lVal_meas, S.mVal_meas⟩
def θ₀ reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the target parameter is the structural slope of its partially linear model.
def residSecondMoment reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the residual treatment second moment is the population integral of the squared difference between factual treatment and its value-space treatment regression evaluated at the factual covariate.
def plrGeneralMoment reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space and a partially linear estimation system built on it, the partially linear general moment system is the abstract moment system with the Robinson partialling-out score, the system's true regression pair and structural slope, and a Jacobian equal to the negative residual treatment second moment.
Definition (Lean source)
parameters
def
given by
clause 1
m := plrMomentFunctional
clause 2
η₀ := S.η₀
clause 3
θ₀ := S.θ₀
clause 4
H_ε := univ
clause 5
clause 6
clause 7
m_meas := fun η θ => measurable_plrMomentFunctional η θ
clause 8
η₀_mem := Set.mem_univ _
clause 9
J₀ := -S.residSecondMoment
clause 10
J₀_ne_zero := neg_ne_zero.mpr S.nondegenerate
lemma plrMomentFunctional_factualZ reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Robinson score at the true nuisance, pulled back to the population space. For the observed data generated from a population outcome ω, the Robinson partialling-out score evaluated at the true nuisance pair, true data, and true parameter equals the true residualized outcome times the true treatment residual.
Formal statement
hypotheses
conclusion
plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀
= (S.factualY ω - S.lVal (S.factualX ω) - S.θ * (S.factualD ω - S.mVal (S.factualX ω))) * (S.factualD ω - S.mVal (S.factualX ω))
Proof (Lean source)
lemma plrMomentFunctional_factualZ (ω : P.Ω) :
plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀
= (S.factualY ω - S.lVal (S.factualX ω)
- S.θ * (S.factualD ω - S.mVal (S.factualX ω)))
* (S.factualD ω - S.mVal (S.factualX ω)) := by
rfl
4 supporting declarations (lemmas, instances)
-
measurable_factualZlemma — The observed-data map is measurable.hypothesesconclusionMeasurable S.factualZProof (Lean source)
@[fun_prop] lemma measurable_factualZ : Measurable S.factualZ := S.measurable_factualX.prodMk (S.measurable_factualD.prodMk S.measurable_factualY) -
P_Z_eqlemma — The joint observed-data law is the image of the population measure under the map recording the observed covariate, treatment, and outcome.hypothesesconclusionS.P_Z = P.μ.map S.factualZProof (Lean source)
@[causal_defs_simps] lemma P_Z_eq : S.P_Z = P.μ.map S.factualZ := rfl -
P_X_eqlemma — The covariate marginal is the image of the population measure under the observed covariate map.hypothesesconclusionS.P_X = P.μ.map S.factualXProof (Lean source)
@[causal_defs_simps] lemma P_X_eq : S.P_X = P.μ.map S.factualX := rfl -
integral_P_Zlemma — Integrating a measurable function under the joint observed-data law equals integrating its pullback under the population measure.hypothesesγ :sharedType u_1f :γ × ℝ × ℝ → ℝhf :conclusion∫ z, f z ∂S.P_Z = ∫ ω, f (S.factualZ ω) ∂P.μProof (Lean source)
lemma integral_P_Z {f : γ × ℝ × ℝ → ℝ} (hf : Measurable f) : ∫ z, f z ∂S.P_Z = ∫ ω, f (S.factualZ ω) ∂P.μ := by rw [P_Z, MeasureTheory.integral_map S.measurable_factualZ.aemeasurable hf.aestronglyMeasurable]
DML 2 core · 0 supporting This file delivers the asymptotic linearity and √n-asymptotic normality of the one-step double-machine-learning estimator of the structural slope in the partially linear model, by composing the abstract Chernozhukov-form ★ plr_dml_isAsymLinear★ plr_dml_tendstoNormal
Headline partially linear DML theorems
This file delivers the asymptotic linearity and √n-asymptotic normality of the one-step double-machine-learning estimator of the structural slope in the partially linear model, by composing the abstract Chernozhukov-form engine with the three model-specific analytic facts (mean-zero, finite-variance, doubly-robust remainder) and the generic asymptotic-linearity ⇒ normality bridge.
theorem plr_dml_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Headline partially linear DML asymptotic-linearity theorem. Fix a partially linear estimation system, an i.i.d. sample of covariate-treatment-outcome triples, and a sample split whose evaluation-fold share converges to a fixed positive limit. If the model's integrability and square-integrability conditions hold — the structural error, its product with the treatment residual, the baseline-covariate term, and the treatment are integrable, the true treatment residual is square-integrable, and the true score has finite second moment; for the estimated nuisance sequence η_hat, at every fold and draw the outcome- and treatment-regression errors are square-integrable in the covariate law, with the resulting cross terms against the structural error and the treatment residual integrable; the estimated score is jointly measurable, fold-A measurable, and integrable/square-integrable at every fold; the L²(P_Z) distance between the estimated and true score is ; and the product of the two nuisance-error seminorms is ; then the one-step double-machine-learning estimator of the structural slope is asymptotically linear at the true slope, with influence function — the inverse-Jacobian-scaled Robinson partialling-out score at the truth.
Formal statement
hypotheses
γ :
Type u_1
S :
PLRSystem P γ
sample :
IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
η_hat :
ℕ → P.Ω → PLRNuisance γ
Model-level integrability facts feeding the three PLR lemmas.
hU :
Integrable S.U P.μ
hUV :
Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ
hbX :
Integrable (fun ω => S.b (S.factualX ω)) P.μ
hD :
Integrable S.factualD P.μ
hV :
MemLp S.resid 2 P.μ
hsq :
Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ
Per-`(n, ω)` remainder regularity, so `plr_remainder_bound` applies at each estimated nuisance `η_hat n ω`.
hΔl :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X
hΔm :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X
hUΔm :
∀ n ω,
Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
hΔlV :
∀ n ω,
Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ
hVΔm :
∀ n ω,
Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
The abstract engine's measurability and rate bundle (copied verbatim from `dml_chernozhukov_asymptoticLinear` with `M := S.plrGeneralMoment`).
h_m_meas :
∀ n,
Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_int :
∀ n ω,
Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z
h_m_sq_int :
∀ n ω,
Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z
h_score_diff_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
conclusion
IsAsymLinear (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) sample split.foldB
Proof (Lean source)
theorem plr_dml_isAsymLinear
(S : PLRSystem P γ)
(sample : IIDSample P.Ω (γ × ℝ × ℝ) 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))
(η_hat : ℕ → P.Ω → PLRNuisance γ)
-- Model-level integrability facts feeding the three PLR lemmas.
(hU : Integrable S.U P.μ)
(hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ)
(hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ)
(hD : Integrable S.factualD P.μ)
(hV : MemLp S.resid 2 P.μ)
(hsq : Integrable
(fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ)
-- Per-`(n, ω)` remainder regularity, so `plr_remainder_bound` applies at
-- each estimated nuisance `η_hat n ω`.
(hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X)
(hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X)
(hUΔm : ∀ n ω, Integrable
(fun ω' => S.U ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
(hΔlV : ∀ n ω, Integrable
(fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω'))
* S.resid ω') P.μ)
(hVΔm : ∀ n ω, Integrable
(fun ω' => S.resid ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
-- The abstract engine's measurability and rate bundle (copied verbatim from
-- `dml_chernozhukov_asymptoticLinear` with `M := S.plrGeneralMoment`).
(h_m_meas :
∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀))
(h_m_foldA_uncurry :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ × ℝ × ℝ))]
(fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_int : ∀ n ω,
Integrable (fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z)
(h_m_sq_int : ∀ n ω,
Integrable (fun z =>
(S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z)
(h_score_diff_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ -
S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀)
2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_product_rate :
IsLittleOp
(fun n ω =>
((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) *
((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) :
IsAsymLinear
(dmlChernozhukovEstimator
S.plrGeneralMoment sample split η_hat)
S.θ₀
(fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)
sample
split.foldB := by
set Crem : ℝ := 1 + |S.θ₀| with hCrem_def
have hMZ := S.plr_meanZero hU hUV hbX hD
have hFV := S.plr_finite_var hsq
have hBR_at :
∀ n ω,
|∫ z, plrMomentFunctional (η_hat n ω) z S.θ₀ ∂S.P_Z| ≤
Crem * ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) *
((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ) :=
fun n ω =>
S.plr_remainder_bound (η_hat n ω) hD hbX hU (hΔl n ω) (hΔm n ω) hV
(hUΔm n ω) (hΔlV n ω) (hVΔm n ω) hUV
simpa [plrGeneralMoment] using
(dml_chernozhukov_asymptoticLinear
S.plrGeneralMoment hMZ hFV sample split hc_pos h_split_rate η_hat
(Crem := Crem) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int
h_m_sq_int h_score_diff_rate h_product_rate)
theorem plr_dml_tendstoNormal reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Headline partially linear DML asymptotic-normality theorem. Fix a partially linear estimation system, an i.i.d. sample of covariate-treatment-outcome triples, and a sample split whose evaluation-fold share converges to a fixed positive limit. Suppose the structural error, its product with the treatment residual, the baseline-covariate term, and the treatment are integrable, the true treatment residual is square-integrable, and the true score has finite second moment; for the estimated nuisance sequence η_hat, the outcome- and treatment-regression errors are square-integrable in the covariate law at every fold and draw, with the resulting cross terms against the structural error and the treatment residual integrable; the estimated score is jointly measurable and measurable as a function of the nuisance-training fold alone and jointly with the observation, and integrable and square-integrable at every fold and draw; the estimated score converges to the true score in L²(P_Z) at rate , and the product of the two nuisance-error seminorms is ; and the influence function, the rescaled estimator at each n, and the normalized influence sum at each n are all measurable. Then the rescaled double-machine-learning estimator of the structural slope, recentered at the true slope and scaled by the square root of the fold-B sample size, converges in distribution to a centered Gaussian whose variance is the second moment of the inverse-Jacobian-scaled partialling-out score at the true regressions.
Formal statement
hypotheses
γ :
Type u_1
S :
PLRSystem P γ
sample :
IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
η_hat :
ℕ → P.Ω → PLRNuisance γ
hU :
Integrable S.U P.μ
hUV :
Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ
hbX :
Integrable (fun ω => S.b (S.factualX ω)) P.μ
hD :
Integrable S.factualD P.μ
hV :
MemLp S.resid 2 P.μ
hsq :
Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ
hΔl :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X
hΔm :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X
hUΔm :
∀ n ω,
Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
hΔlV :
∀ n ω,
Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ
hVΔm :
∀ n ω,
Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
h_m_meas :
∀ n,
Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_int :
∀ n ω,
Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z
h_m_sq_int :
∀ n ω,
Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z
h_score_diff_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
hψ_meas :
Measurable (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)
hθn_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n,
AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)) P.μ hθn_meas
Proof (Lean source)
theorem plr_dml_tendstoNormal
(S : PLRSystem P γ)
(sample : IIDSample P.Ω (γ × ℝ × ℝ) 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))
(η_hat : ℕ → P.Ω → PLRNuisance γ)
(hU : Integrable S.U P.μ)
(hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ)
(hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ)
(hD : Integrable S.factualD P.μ)
(hV : MemLp S.resid 2 P.μ)
(hsq : Integrable
(fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ)
(hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X)
(hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X)
(hUΔm : ∀ n ω, Integrable
(fun ω' => S.U ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
(hΔlV : ∀ n ω, Integrable
(fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω'))
* S.resid ω') P.μ)
(hVΔm : ∀ n ω, Integrable
(fun ω' => S.resid ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
(h_m_meas :
∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀))
(h_m_foldA_uncurry :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ × ℝ × ℝ))]
(fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_int : ∀ n ω,
Integrable (fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z)
(h_m_sq_int : ∀ n ω,
Integrable (fun z =>
(S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z)
(h_score_diff_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ -
S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀)
2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_product_rate :
IsLittleOp
(fun n ω =>
((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) *
((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(hψ_meas :
Measurable
(fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀))
(hθn_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)
split.foldB n) P.μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator
(dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB)
(gaussianMeasure 0
(∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2
∂S.P_Z))
P.μ
hθn_meas := by
have hAL :=
S.plr_dml_isAsymLinear sample split hc_pos h_split_rate η_hat
hU hUV hbX hD hV hsq hΔl hΔm hUΔm hΔlV hVΔm
h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int
h_score_diff_rate h_product_rate
exact hAL.tendsto_normal_foldB split hψ_meas hθn_meas hSum_meas
Feasible 2 core · 0 supporting This file treats the one-dimensional partially linear regression model, so the orthogonal score is affine in a single scalar treatment-effect parameter. ★ plr_dml_feasible_tendstoNormal
Feasible partially linear DML
This file treats the one-dimensional partially linear regression model, so the
orthogonal score is affine in a single scalar treatment-effect parameter. It
defines the solved Robinson ratio estimator plrFeasibleEstimator, whose
numerator is the empirical covariance of residualized outcome and treatment and
whose denominator is the empirical treatment residual variance. The theorem
plr_dml_feasible_tendstoNormal reduces its √|B|-asymptotic normality to the
one-step normality theorem plr_dml_tendstoNormal by the standard
asymptotic-equivalence argument.
def plrFeasibleEstimator reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
For a partially linear potential-outcomes system with a finite population measure and a measurable covariate space, a partially linear estimation system built on it, an independent and identically distributed sample from its joint observed-data law, a one-shot evaluation-fold split of that sample, a sequence of estimated outcome-and-treatment regression pairs, and a sample-size index, the feasible partially linear double-machine-learning estimator maps each population state to the ratio of the evaluation-fold sum of residualized-outcome times residualized-treatment to the evaluation-fold sum of squared residualized-treatment.
Definition (Lean source)
parameters
γ :
Type u_1
S :
PLRSystem P γ
sample :
IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
η_hat :
ℕ → P.Ω → PLRNuisance γ
n :
ℕ
def
plrFeasibleEstimator S sample split η_hat n :
P.Ω → ℝ
given by
fun ω
=> (∑ i ∈ split.foldB n, plrMomentB (η_hat n ω) (sample.Z i ω)) / (∑ i ∈ split.foldB n, (plrResidual (η_hat n ω) (sample.Z i ω)) ^ 2)
theorem plr_dml_feasible_tendstoNormal reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Feasible partially linear DML asymptotic-normality theorem. Fix a partially linear estimation system, an i.i.d. sample of covariate-treatment-outcome triples, and a sample split whose evaluation-fold share converges to a fixed positive limit. Suppose the structural error, its product with the treatment residual, the baseline-covariate term, and the treatment are integrable, the true treatment residual is square-integrable, and the true score has finite second moment; for the estimated nuisance sequence η_hat, the outcome- and treatment-regression errors are square-integrable in the covariate law at every fold and draw, with the resulting cross terms against the structural error and the treatment residual integrable; the estimated score is jointly measurable and measurable as a function of the nuisance-training fold alone and jointly with the observation, and integrable and square-integrable at every fold and draw; the estimated score converges to the true score in L²(P_Z) at rate , and the product of the two nuisance-error seminorms is ; and the influence function, the one-step rescaled estimator at each n, and the normalized influence sum at each n are all measurable. Suppose in addition the empirical partialling-out Jacobian over fold B converges in probability to its population value J₀, and the rescaled feasible estimator is measurable at each n. Then the rescaled feasible estimator — the solved Robinson partialling-out estimator, recentered at the true slope and scaled by the square root of the fold-B sample size — converges in distribution to the same centered Gaussian as the one-step estimator: a normal law whose variance is the population second moment of the inverse-Jacobian-scaled partialling-out score at the true regressions.
Formal statement
hypotheses
γ :
Type u_1
S :
PLRSystem P γ
sample :
IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
η_hat :
ℕ → P.Ω → PLRNuisance γ
hU :
Integrable S.U P.μ
hUV :
Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ
hbX :
Integrable (fun ω => S.b (S.factualX ω)) P.μ
hD :
Integrable S.factualD P.μ
hV :
MemLp S.resid 2 P.μ
hsq :
Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ
hΔl :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X
hΔm :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X
hUΔm :
∀ n ω,
Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
hΔlV :
∀ n ω,
Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ
hVΔm :
∀ n ω,
Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ
h_m_meas :
∀ n,
Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)
h_m_int :
∀ n ω,
Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z
h_m_sq_int :
∀ n ω,
Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z
h_score_diff_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
h_product_rate :
IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ
hψ_meas :
Measurable (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)
hθn_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n,
AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ
The single new probabilistic hypothesis: in-probability consistency of the empirical partialling-out Jacobian over fold B to its population value.
hJ_consist :
Tendsto_inProb (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) (fun _ => S.plrGeneralMoment.J₀) P.μ
hθn_feas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)) P.μ hθn_feas
Proof (Lean source)
theorem plr_dml_feasible_tendstoNormal
(S : PLRSystem P γ)
(sample : IIDSample P.Ω (γ × ℝ × ℝ) 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))
(η_hat : ℕ → P.Ω → PLRNuisance γ)
(hU : Integrable S.U P.μ)
(hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ)
(hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ)
(hD : Integrable S.factualD P.μ)
(hV : MemLp S.resid 2 P.μ)
(hsq : Integrable
(fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ)
(hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X)
(hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X)
(hUΔm : ∀ n ω, Integrable
(fun ω' => S.U ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
(hΔlV : ∀ n ω, Integrable
(fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω'))
* S.resid ω') P.μ)
(hVΔm : ∀ n ω, Integrable
(fun ω' => S.resid ω' *
((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ)
(h_m_meas :
∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀))
(h_m_foldA_uncurry :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ × ℝ × ℝ))]
(fun (p : P.Ω × (γ × ℝ × ℝ)) =>
S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀))
(h_m_int : ∀ n ω,
Integrable (fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z)
(h_m_sq_int : ∀ n ω,
Integrable (fun z =>
(S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z)
(h_score_diff_rate :
IsLittleOp
(fun n ω =>
(eLpNorm
(fun z =>
S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ -
S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀)
2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_product_rate :
IsLittleOp
(fun n ω =>
((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) *
((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ)
(hψ_meas :
Measurable
(fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀))
(hθn_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)
split.foldB n) P.μ)
-- The single new probabilistic hypothesis: in-probability consistency of the
-- empirical partialling-out Jacobian over fold B to its population value.
(hJ_consist :
Tendsto_inProb
(fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω))
(fun _ => S.plrGeneralMoment.J₀) P.μ)
(hθn_feas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator
(plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB)
(gaussianMeasure 0
(∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2
∂S.P_Z))
P.μ
hθn_feas := by
-- Step 1: the one-step rescaled estimator converges to the Gaussian target.
have hOS :=
S.plr_dml_tendstoNormal sample split hc_pos h_split_rate η_hat
hU hUV hbX hD hV hsq hΔl hΔm hUΔm hΔlV hVΔm
h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int
h_score_diff_rate h_product_rate hψ_meas hθn_meas hSum_meas
-- Abbreviations.
set J₀ : ℝ := S.plrGeneralMoment.J₀ with hJ₀_def
have hJ₀_ne : J₀ ≠ 0 := S.plrGeneralMoment.J₀_ne_zero
-- The empirical partialling-out Jacobian `Pₙ mₐ = |B|⁻¹ Σ mₐ`.
set Pmₐ : ℕ → P.Ω → ℝ :=
fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω) with hPmₐ_def
-- The normalized influence sum `(√|B|)⁻¹ Σ ψ`.
set Sψ : ℕ → P.Ω → ℝ :=
fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ *
∑ i ∈ split.foldB n, plrMomentFunctional (η_hat n ω) (sample.Z i ω) S.θ₀
with hSψ_def
-- The one-step rescaled estimator (the `Xn` of the Slutsky step).
set Xn : ℕ → P.Ω → ℝ :=
IsAsymLinear.rescaledEstimator
(dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB with hXn_def
-- The feasible rescaled estimator (the `Yn`).
set Yn : ℕ → P.Ω → ℝ :=
IsAsymLinear.rescaledEstimator
(plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB with hYn_def
-- The factor that turns out to be `o_p(1)`: `J₀⁻¹ − (Pₙmₐ)⁻¹`.
set Fn : ℕ → P.Ω → ℝ :=
fun n ω => S.plrGeneralMoment.J₀_inv - (Pmₐ n ω)⁻¹ with hFn_def
-- Step 4: `(√|B|)⁻¹ Σ ψ = −J₀ · (one-step rescaled estimator)` pointwise,
-- hence `O_p(1)` by tightness of the one-step Gaussian limit.
have hSψ_eq : Sψ = fun n ω => (-J₀) * Xn n ω := by
funext n ω
-- Abbreviate the influence sum `Σ ψ`; `m(η̂, z, θ₀) = plrMomentFunctional`
-- definitionally, so this is also the empirical-moment sum of `Xn`.
set Sumψ : ℝ := ∑ i ∈ split.foldB n,
plrMomentFunctional (η_hat n ω) (sample.Z i ω) S.θ₀ with hSumψ_def
-- The one-step empirical-moment sum is `Sumψ` (definitional projection
-- equalities `m = plrMomentFunctional`, `θ₀ = S.θ₀`).
have hθ₀_proj : S.plrGeneralMoment.θ₀ = S.θ₀ := rfl
have hsum_m : (∑ i ∈ split.foldB n,
S.plrGeneralMoment.m (η_hat n ω) (sample.Z i ω) S.θ₀) = Sumψ :=
rfl
have hXn_val : Xn n ω = sqrt ((split.foldB n).card : ℝ) *
(-(J₀⁻¹ * (((split.foldB n).card : ℝ)⁻¹ * Sumψ))) := by
simp only [hXn_def, IsAsymLinear.rescaledEstimator, dmlChernozhukovEstimator,
GeneralMoment.J₀_inv, hJ₀_def, hθ₀_proj, hsum_m]
ring
have hSψ_val : Sψ n ω = (sqrt ((split.foldB n).card : ℝ))⁻¹ * Sumψ := rfl
rw [hSψ_val, hXn_val]
rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard
· -- Empty fold: both sides vanish.
simp only [hcard, cast_zero, Real.sqrt_zero, inv_zero, zero_mul,
mul_zero, neg_zero]
· -- Nonempty fold: use `√|B| · |B|⁻¹ = (√|B|)⁻¹` and `J₀ · J₀⁻¹ = 1`.
have hcard_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by
exact_mod_cast hcard
have hcard_ne : ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hcard_pos
have hsqrt_ne : sqrt ((split.foldB n).card : ℝ) ≠ 0 :=
ne_of_gt (Real.sqrt_pos.mpr hcard_pos)
have hsqrt_sq : sqrt ((split.foldB n).card : ℝ) *
sqrt ((split.foldB n).card : ℝ) = ((split.foldB n).card : ℝ) :=
Real.mul_self_sqrt (le_of_lt hcard_pos)
-- `(√|B|)⁻¹ = √|B| · |B|⁻¹` since `|B| = √|B| · √|B|`.
have hsqrt_inv : (sqrt ((split.foldB n).card : ℝ))⁻¹
= sqrt ((split.foldB n).card : ℝ) * ((split.foldB n).card : ℝ)⁻¹ := by
field_simp
linarith [hsqrt_sq]
rw [hsqrt_inv]
field_simp
-- `(√|B|)⁻¹ Σ ψ = O_p(1)`.
have hSψ_bigO : IsBigOp Sψ (fun _ => (1 : ℝ)) P.μ := by
rw [hSψ_eq]
exact const_mul (-J₀) (Tendsto_dist.tightness hθn_meas hOS)
-- Step 3: `(Pₙmₐ)⁻¹ →ₚ J₀⁻¹`, hence `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ →ₚ 0`, i.e. `o_p(1)`.
have hPmₐ_inv : Tendsto_inProb (fun n ω => 1 / Pmₐ n ω) (fun _ => 1 / J₀) P.μ := by
have := (hJ_consist).inv hJ₀_ne
simpa [hPmₐ_def, hJ₀_def] using this
have hFn_inProb : Tendsto_inProb Fn (fun _ => 0) P.μ := by
-- `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ = (1/J₀) − (1/Pₙmₐ)`; it converges to `0`.
have hconv :
Tendsto_inProb (fun n ω => (fun n ω => 1 / Pmₐ n ω) n ω - 1 / J₀)
(fun _ => 0) P.μ := hPmₐ_inv.sub_const
-- Rewrite `1/x = x⁻¹` and flip the sign to match `Fn`.
have hneg :
Tendsto_inProb (fun n ω => -(fun n ω => 1 / Pmₐ n ω - 1 / J₀) n ω)
(fun _ => 0) P.μ := by
have hcont : ContinuousAt (fun x : ℝ => -x) (0 : ℝ) := (continuous_neg).continuousAt
have := hconv.comp_continuousAt (g := fun x : ℝ => -x) hcont
simpa using this
have hFn_eq : Fn = fun n ω => -((fun n ω => 1 / Pmₐ n ω) n ω - 1 / J₀) := by
funext n ω
simp only [hFn_def, GeneralMoment.J₀_inv, hJ₀_def, one_div]
ring
rw [hFn_eq]
exact hneg
have hFn_littleO : IsLittleOp Fn (fun _ => (1 : ℝ)) P.μ :=
hFn_inProb.isLittleOp_one
-- Step 5: the product `Fn · Sψ = o_p(1)`.
have hprod_littleO :
IsLittleOp (fun n ω => Sψ n ω * Fn n ω) (fun _ => (1 : ℝ)) P.μ :=
hSψ_bigO.mul_isLittleOp_one_isLittleOp hFn_littleO
-- Step 2 + 6: off the null event `{Pₙmₐ = 0}`, the rescaled difference equals
-- `Fn · Sψ`. The null event has vanishing measure, so the rescaled difference
-- is itself `o_p(1)`.
-- (a) The algebraic identity on `{Pₙmₐ ≠ 0}`.
have hdiff_eq :
∀ n ω, Pmₐ n ω ≠ 0 →
Yn n ω - Xn n ω = Sψ n ω * Fn n ω := by
intro n ω hPne
-- On a nonempty fold (forced by `Pₙmₐ ≠ 0`), expand both estimators.
have hcard_pos : 0 < (split.foldB n).card := by
rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hpos
· exact absurd (by
simp only [hPmₐ_def, Finset.card_eq_zero.mp hz, Finset.sum_empty,
mul_zero]) hPne
· exact hpos
have hcardR_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard_pos
have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hcardR_pos
have hsqrt_pos : (0 : ℝ) < sqrt ((split.foldB n).card : ℝ) :=
Real.sqrt_pos.mpr hcardR_pos
have hsqrt_ne : sqrt ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hsqrt_pos
have hsqrt_sq : sqrt ((split.foldB n).card : ℝ) *
sqrt ((split.foldB n).card : ℝ) = ((split.foldB n).card : ℝ) :=
Real.mul_self_sqrt (le_of_lt hcardR_pos)
-- Denominator of the feasible estimator: `D := Σ residual²`.
set D : ℝ := ∑ i ∈ split.foldB n,
(plrResidual (η_hat n ω) (sample.Z i ω)) ^ 2 with hD_def
-- `Σ mₐ = −D`.
-- … truncated; follow the source link for the rest …
JacobianConsistency 1 core · 3 supporting This file proves that the empirical Jacobian of the partially linear partialling-out score, averaged over the estimation fold, converges in probability to its population value. ★ plr_jacobian_consistency
Fold-B partialling-out Jacobian consistency
This file proves that the empirical Jacobian of the partially linear partialling-out score, averaged over the estimation fold, converges in probability to its population value. It supplies the Jacobian-consistency condition needed by the feasible partially linear double-machine-learning asymptotic-normality result.
theorem plr_jacobian_consistency reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Fold-B Jacobian consistency. Assume the treatment is integrable; the true partialling-out moment at the truth is square-integrable under the observed-data law, and the squared true treatment residual is integrable; that for the estimated nuisance sequence η_hat, at every fold and draw, the treatment-regression error is square-integrable in the covariate law, both marginally and against the true treatment residual; that the treatment-regression error converges to zero in L²(P_X) at rate ; and that the partialling-out-moment increment mₐ(η̂,·) − mₐ(η₀,·) is jointly measurable, fold-A measurable, square-integrable under the observed-data law, and converges to zero in L²(P_Z) at rate . Then the empirical partialling-out Jacobian at the estimated nuisance, averaged over the estimation fold, converges in probability to its population value :
Formal statement
hypotheses
γ :
Type u_1
S :
PLRSystem P γ
sample :
IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z
split :
OneShotSplit sample
η_hat :
ℕ → P.Ω → PLRNuisance γ
hD :
Integrable S.factualD P.μ
Square-integrability of the partialling-out moment at the truth (a fourth-moment condition on the treatment residual), so the fold-B WLLN applies to `mₐ(η₀, ·)`.
hg0_memLp :
MemLp (plrMomentA S.η₀) 2 S.P_Z
Per-`(n, ω)` integrability witnesses for the bias decomposition.
hresid_sq :
Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) ^ 2) P.μ
hΔm_sq :
∀ n ω,
Integrable (fun ω' => (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω')) ^ 2) P.μ
hcross :
∀ n ω,
Integrable (fun ω' => (S.factualD ω' - S.mVal (S.factualX ω')) * (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω'))) P.μ
L²(P_X) square-integrability of the treatment-regression error.
hΔm_memLp :
∀ n ω, MemLp (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X
The treatment-regression L²(P_X) `o_p(1)` rate.
h_m_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
Fold-A measurability of the partialling-out-moment increment (mirroring the `h_m_foldA`-style hypotheses of `plr_dml_isAsymLinear`: `η̂` is fold-A trained).
hΔa_meas :
∀ n,
hΔa_foldA :
∀ n,
Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z)
hΔa_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (uncurry (fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z))
Per-`(n, ω)` `L²(P_Z)` membership of the increment.
hΔa_memLp :
L²(P_Z) `o_p(1)` rate of the increment (mirroring the boundedness bookkeeping of `plr_score_diff_isLittleOp_one`: the residual is bounded, `Δm` is bounded, and the L²(P_X) rate then propagates to the `mₐ`-increment).
hΔa_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
conclusion
Tendsto_inProb (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) (fun _ => S.plrGeneralMoment.J₀) P.μ
Proof (Lean source)
theorem plr_jacobian_consistency
(S : PLRSystem P γ)
(sample : IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z)
(split : OneShotSplit sample)
(η_hat : ℕ → P.Ω → PLRNuisance γ)
(hD : Integrable S.factualD P.μ)
-- Square-integrability of the partialling-out moment at the truth (a fourth-moment
-- condition on the treatment residual), so the fold-B WLLN applies to `mₐ(η₀, ·)`.
(hg0_memLp : MemLp (plrMomentA S.η₀) 2 S.P_Z)
-- Per-`(n, ω)` integrability witnesses for the bias decomposition.
(hresid_sq : Integrable
(fun ω => (S.factualD ω - S.mVal (S.factualX ω)) ^ 2) P.μ)
(hΔm_sq : ∀ n ω, Integrable
(fun ω' => (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω')) ^ 2) P.μ)
(hcross : ∀ n ω, Integrable
(fun ω' => (S.factualD ω' - S.mVal (S.factualX ω'))
* (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω'))) P.μ)
-- L²(P_X) square-integrability of the treatment-regression error.
(hΔm_memLp : ∀ n ω, MemLp (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X)
-- The treatment-regression L²(P_X) `o_p(1)` rate.
(h_m_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
-- Fold-A measurability of the partialling-out-moment increment (mirroring the
-- `h_m_foldA`-style hypotheses of `plr_dml_isAsymLinear`: `η̂` is fold-A trained).
(hΔa_meas :
∀ n, Measurable (uncurry
(fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z)))
(hΔa_foldA :
∀ n,
Measurable[comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance]
(fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z))
(hΔa_uncurry_foldA :
∀ n,
Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod
(inferInstance : MeasurableSpace (γ × ℝ × ℝ))]
(uncurry
(fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z)))
-- Per-`(n, ω)` `L²(P_Z)` membership of the increment.
(hΔa_memLp : ∀ n ω,
MemLp (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z)
-- L²(P_Z) `o_p(1)` rate of the increment (mirroring the boundedness bookkeeping of
-- `plr_score_diff_isLittleOp_one`: the residual is bounded, `Δm` is bounded, and the
-- L²(P_X) rate then propagates to the `mₐ`-increment).
(hΔa_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ) :
Tendsto_inProb
(fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω))
(fun _ => S.plrGeneralMoment.J₀) P.μ := by
classical
-- Abbreviations: the truth statistic `g₀`, the truth-Jacobian average `Y₀`, and the
-- target `Yn`.
set g₀ : (γ × ℝ × ℝ) → ℝ := plrMomentA S.η₀ with hg₀_def
set Yn : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω) with hYn_def
set Y₀ : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, g₀ (sample.Z i ω) with hY₀_def
set J₀ : ℝ := S.plrGeneralMoment.J₀ with hJ₀_def
-- STEP 2: `Y₀ →ₚ J₀` by the fold-B WLLN, with the limit rewritten by step 1.
have hY₀_lim : Tendsto_inProb Y₀ (fun _ => J₀) P.μ := by
have hwlln := OneShotSplit.foldB_sampleMean_tendsto_inProb sample split
(measurable_plrMomentA S.η₀) hg0_memLp
have hint : ∫ z, g₀ z ∂S.P_Z = J₀ := S.integral_plrMomentA_η₀_eq_J₀
rw [hint] at hwlln
exact hwlln
-- STEP 3a (bias): `bias n ω = ∫ Δa dP_Z = −‖Δm‖²₂`, which is `o_p(1)`.
set bias : ℕ → P.Ω → ℝ := fun n ω =>
∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z with hbias_def
have hbias_eq : ∀ n ω, bias n ω
= -((eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal) ^ 2 := by
intro n ω
simp only [hbias_def]
rw [S.integral_plrMomentA_diff_eq (η_hat n ω) hD hresid_sq (hΔm_sq n ω) (hcross n ω)]
rw [S.integral_Δm_sq_eq_rate_sq (η_hat n ω) (hΔm_memLp n ω)]
-- `‖Δm‖₂ →ₚ 0`, so its square →ₚ 0, so `bias →ₚ 0`, hence `o_p(1)`.
set rateM : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal with hrateM_def
have hrateM_lo : IsLittleOp rateM (fun _ => (1 : ℝ)) P.μ := h_m_rate
have hrateM_inProb : Tendsto_inProb rateM (fun _ => 0) P.μ :=
tendsto_inProb_zero_of_isLittleOp_one hrateM_lo
have hrateMsq_inProb : Tendsto_inProb (fun n ω => (rateM n ω) ^ 2) (fun _ => 0) P.μ := by
have hcont : ContinuousAt (fun x : ℝ => x ^ 2) (0 : ℝ) :=
(continuous_pow 2).continuousAt
have := hrateM_inProb.comp_continuousAt (g := fun x : ℝ => x ^ 2) hcont
simpa using this
have hbias_inProb : Tendsto_inProb bias (fun _ => 0) P.μ := by
have heq : bias = fun n ω => -((rateM n ω) ^ 2) := by
funext n ω; rw [hbias_eq n ω, hrateM_def]
rw [heq]
have hcont : ContinuousAt (fun x : ℝ => -x) (0 : ℝ) := (continuous_neg).continuousAt
have := hrateMsq_inProb.comp_continuousAt (g := fun x : ℝ => -x) hcont
simpa using this
have hbias_lo : IsLittleOp bias (fun _ => (1 : ℝ)) P.μ := hbias_inProb.isLittleOp_one
-- The "effective" bias `(|B|⁻¹·|B|)·bias` — equal to `bias` on nonempty folds and `0`
-- on empty folds — so that the pointwise decomposition below holds for ALL `n`. Its
-- `{0,1}`-valued prefactor leaves it `o_p(1)`.
set biasEff : ℕ → P.Ω → ℝ := fun n ω =>
(((split.foldB n).card : ℝ)⁻¹ * (split.foldB n).card) * bias n ω with hbiasEff_def
have hbiasEff_lo : IsLittleOp biasEff (fun _ => (1 : ℝ)) P.μ := by
refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hbias_lo ?_
intro n ω
simp only [hbiasEff_def]
rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard
· simp [hcard]
· have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := by
simp only [ne_eq, Nat.cast_eq_zero]; omega
rw [inv_mul_cancel₀ hcardR_ne, one_mul, one_mul]
-- STEP 3b (centered): `centered n ω = |B|⁻¹ Σ (Δa(Zᵢ) − ∫Δa)` is `o_p(1)`.
set centered : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n,
((plrMomentA (η_hat n ω) (sample.Z i ω) - plrMomentA S.η₀ (sample.Z i ω))
- ∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z) with hcentered_def
have hcentered_lo : IsLittleOp centered (fun _ => (1 : ℝ)) P.μ := by
-- The fold-B centered empirical-process bound gives the `(√|B|)⁻¹`-normalized sum
-- as `o_p(1)`; renormalizing by the extra `(√|B|)⁻¹ → 0` factor keeps it `o_p(1)`.
-- The random function family `f n ω z = mₐ(η̂(n,ω), z) − mₐ(η₀, z)`.
set f : ℕ → P.Ω → (γ × ℝ × ℝ) → ℝ :=
fun n ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z with hf_def
-- The `(√|B|)⁻¹`-normalized centered fold-B sum is `o_p(1)`.
have hsqrt_centered :
IsLittleOp
(fun n ω =>
(sqrt ((split.foldB n).card : ℝ))⁻¹ *
∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ x, f n ω x ∂S.P_Z))
(fun _ => (1 : ℝ)) P.μ :=
foldB_centered_sum_isLittleOp_one sample split f hΔa_meas
hΔa_uncurry_foldA hΔa_memLp hΔa_rate
set centeredSqrt : ℕ → P.Ω → ℝ :=
fun n ω =>
(sqrt ((split.foldB n).card : ℝ))⁻¹ *
∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ x, f n ω x ∂S.P_Z)
with hcenteredSqrt_def
-- `centeredSqrt` is `O_p(1)` (it converges in probability to `0`).
have hcenteredSqrt_bigO : IsBigOp centeredSqrt (fun _ => (1 : ℝ)) P.μ :=
(tendsto_inProb_zero_of_isLittleOp_one hsqrt_centered).isBigOp_one
-- The deterministic factor `(√|B(n)|)⁻¹ → 0`, since `|B(n)| → ∞`.
have ha_tendsto :
Tendsto (fun n => (sqrt ((split.foldB n).card : ℝ))⁻¹) atTop (𝓝 0) := by
have hcard : Tendsto (fun n => ((split.foldB n).card : ℝ)) atTop atTop :=
tendsto_natCast_atTop_atTop.comp split.foldB_card_tendsto
have hsqrt : Tendsto (fun n => sqrt ((split.foldB n).card : ℝ)) atTop atTop :=
Real.tendsto_sqrt_atTop.comp hcard
exact hsqrt.inv_tendsto_atTop
-- `centered = (√|B|)⁻¹ · centeredSqrt`, an `o_p(1)·(→0)` product.
have hprod_lo :
IsLittleOp
(fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * centeredSqrt n ω)
(fun _ => (1 : ℝ)) P.μ :=
IsBigOp.const_mul_tendsto_zero hcenteredSqrt_bigO ha_tendsto
-- Pointwise: `centered = (√|B|)⁻¹ · centeredSqrt`.
have hcentered_eq :
centered = fun n ω =>
(sqrt ((split.foldB n).card : ℝ))⁻¹ * centeredSqrt n ω := by
funext n ω
simp only [hcentered_def, hcenteredSqrt_def, hf_def]
rw [← mul_assoc]
-- `|B|⁻¹ = (√|B|)⁻¹ · (√|B|)⁻¹`.
have hinv :
((split.foldB n).card : ℝ)⁻¹
= (sqrt ((split.foldB n).card : ℝ))⁻¹ *
(sqrt ((split.foldB n).card : ℝ))⁻¹ := by
rw [← mul_inv]
rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard
· simp [hcard]
· have hcardR_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard
rw [Real.mul_self_sqrt (le_of_lt hcardR_pos)]
rw [hinv]
rw [hcentered_eq]
exact hprod_lo
-- STEP 3 combine: `Yn − Y₀ = centered + biasEff` pointwise, for ALL `n` (the empty
-- fold makes every term — including `biasEff` — vanish).
have hYn_sub_Y₀ : ∀ n ω, Yn n ω - Y₀ n ω = centered n ω + biasEff n ω := by
intro n ω
rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard
· -- Empty fold: every term is `0`.
simp only [hYn_def, hY₀_def, hcentered_def, hbiasEff_def, hbias_def, hg₀_def,
Finset.card_eq_zero.mp hcard, Finset.sum_empty, Finset.card_empty, mul_zero,
cast_zero, inv_zero, zero_mul, sub_zero, add_zero]
· -- Nonempty fold: `|B|⁻¹ Σ Δa = |B|⁻¹ Σ (Δa − c) + c` where `c = ∫Δa` and the
-- correction `|B|⁻¹ · |B| · c = c`.
have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := by
simp only [ne_eq, Nat.cast_eq_zero]; omega
simp only [hYn_def, hY₀_def, hcentered_def, hbiasEff_def, hbias_def, hg₀_def]
set c : ℝ := ∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z with hc_def
-- RHS centered sum splits as `Σ (Δaᵢ) − |B|·c`.
rw [Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul]
rw [Finset.sum_sub_distrib, mul_sub, ← mul_assoc]
rw [inv_mul_cancel₀ hcardR_ne, one_mul]
ring
have hYn_sub_Y₀_lo : IsLittleOp (fun n ω => Yn n ω - Y₀ n ω) (fun _ => (1 : ℝ)) P.μ := by
have heq : (fun n ω => Yn n ω - Y₀ n ω) = fun n ω => centered n ω + biasEff n ω := by
funext n ω; exact hYn_sub_Y₀ n ω
rw [heq]
exact IsLittleOp.add_one hcentered_lo hbiasEff_lo
-- STEP 4: `Yn − J₀ = (Yn − Y₀) + (Y₀ − J₀)`, both `o_p(1)`; back to `Tendsto_inProb`.
have hY₀_sub_lo : IsLittleOp (fun n ω => Y₀ n ω - J₀) (fun _ => (1 : ℝ)) P.μ :=
hY₀_lim.sub_const.isLittleOp_one
have hYn_sub_J₀_lo : IsLittleOp (fun n ω => Yn n ω - J₀) (fun _ => (1 : ℝ)) P.μ := by
have heq : (fun n ω => Yn n ω - J₀)
= fun n ω => (Yn n ω - Y₀ n ω) + (Y₀ n ω - J₀) := by
funext n ω; ring
rw [heq]
exact IsLittleOp.add_one hYn_sub_Y₀_lo hY₀_sub_lo
-- Convert `IsLittleOp (Yn − J₀) 1` back into `Tendsto_inProb Yn J₀`.
have hYn_sub_inProb : Tendsto_inProb (fun n ω => Yn n ω - J₀) (fun _ => 0) P.μ :=
tendsto_inProb_zero_of_isLittleOp_one hYn_sub_J₀_lo
-- `Yn = (Yn − J₀) + J₀`, so `Yn →ₚ J₀`.
have hfinal : Tendsto_inProb Yn (fun _ => J₀) P.μ := by
have hcont : ContinuousAt (fun x : ℝ => x + J₀) (0 : ℝ) :=
(continuous_add_const J₀).continuousAt
have := hYn_sub_inProb.comp_continuousAt (g := fun x : ℝ => x + J₀) hcont
simpa using this
exact hfinal
3 supporting declarations (lemmas, instances)
-
integral_plrMomentA_η₀_eq_J₀lemma — The population integral of the partialling-out moment at the truth equals the Jacobian: ∫ mₐ(η₀, ·) dP_Z = J₀ = −E[(D − m_val(X))²].hypothesesconclusion∫ z, plrMomentA S.η₀ z ∂S.P_Z = S.plrGeneralMoment.J₀Proof (Lean source)
lemma integral_plrMomentA_η₀_eq_J₀ (S : PLRSystem P γ) : ∫ z, plrMomentA S.η₀ z ∂S.P_Z = S.plrGeneralMoment.J₀ := by rw [S.integral_P_Z (measurable_plrMomentA S.η₀)] change ∫ ω, plrMomentA S.η₀ (S.factualZ ω) ∂P.μ = -S.residSecondMoment rw [residSecondMoment, ← integral_neg] apply integral_congr_ae filter_upwards with ω simp only [plrMomentA, plrResidual, η₀, factualZ] -
instIsProbabilityMeasureP_Zinstance — For a potential-outcome system equipped with a finite probability measure, a measurable covariate space, and a partially linear regression system based on them, the system's joint observed-data law is a probability measure.parametersinstancegiven byMeasure.isProbabilityMeasure_map S.measurable_factualZ.aemeasurable -
integral_plrMomentA_diff_eqlemma — Bias of the empirical-Jacobian increment. The population integral of the increment Δa := mₐ(η̂, ·) − mₐ(η₀, ·) is minus the squared L²(P_X) magnitude of the treatment-regression error Δm := m_val − m̂:hypothesesγ :sharedType u_1S :PLRSystem P γη :hD :Integrable S.factualD P.μhresid_sq :Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) ^ 2) P.μhΔm_sq :Integrable (fun ω => (S.mVal (S.factualX ω) - η.mFn (S.factualX ω)) ^ 2) P.μhcross :Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) * (S.mVal (S.factualX ω) - η.mFn (S.factualX ω))) P.μconclusion∫ z, (plrMomentA η z - plrMomentA S.η₀ z) ∂S.P_Z= -∫ ω, (S.mVal (S.factualX ω) - η.mFn (S.factualX ω)) ^ 2 ∂P.μProof (Lean source)
lemma integral_plrMomentA_diff_eq (S : PLRSystem P γ) (η : PLRNuisance γ) (hD : Integrable S.factualD P.μ) (hresid_sq : Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) ^ 2) P.μ) (hΔm_sq : Integrable (fun ω => (S.mVal (S.factualX ω) - η.mFn (S.factualX ω)) ^ 2) P.μ) (hcross : Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) * (S.mVal (S.factualX ω) - η.mFn (S.factualX ω))) P.μ) : ∫ z, (plrMomentA η z - plrMomentA S.η₀ z) ∂S.P_Z = -∫ ω, (S.mVal (S.factualX ω) - η.mFn (S.factualX ω)) ^ 2 ∂P.μ := by -- Change of variables to `μ`. have hmeas : Measurable (fun z => plrMomentA η z - plrMomentA S.η₀ z) := (measurable_plrMomentA η).sub (measurable_plrMomentA S.η₀) rw [S.integral_P_Z hmeas] -- Abbreviate the (pulled-back) residual and regression error. set V₀ : P.Ω → ℝ := fun ω => S.factualD ω - S.mVal (S.factualX ω) with hV₀_def set Δm : P.Ω → ℝ := fun ω => S.mVal (S.factualX ω) - η.mFn (S.factualX ω) with hΔm_def -- Pointwise expansion: `Δa ∘ Z = −2·V₀·Δm − Δm²`. have hpt : (fun ω => plrMomentA η (S.factualZ ω) - plrMomentA S.η₀ (S.factualZ ω)) = fun ω => (-2) * (V₀ ω * Δm ω) - Δm ω ^ 2 := by funext ω simp only [plrMomentA, plrResidual, η₀, factualZ, hV₀_def, hΔm_def] ring rw [hpt] -- Linearity of the integral over the two summands. have hsmul : Integrable (fun ω => (-2 : ℝ) * (V₀ ω * Δm ω)) P.μ := hcross.const_mul _ have hΔmsq' : Integrable (fun ω => Δm ω ^ 2) P.μ := hΔm_sq rw [integral_sub hsmul hΔmsq', integral_const_mul] -- The cross term `∫ V₀·Δm` vanishes by orthogonality of the residual. have hcross_zero : ∫ ω, V₀ ω * Δm ω ∂P.μ = 0 := by -- `V₀ =ᵐ resid` via `mVal_compat` (`m_val(X) =ᵐ mReg`, `resid = D − mReg`). have hV₀_ae : (fun ω => V₀ ω * Δm ω) =ᵐ[P.μ] fun ω => S.resid ω * Δm ω := by filter_upwards [S.mVal_compat] with ω hω simp only [hV₀_def] have hr : S.resid ω = S.factualD ω - S.mReg ω := rfl rw [hr, hω] rw [integral_congr_ae hV₀_ae] -- Orthogonality: `Δm = (m_val − m̂)(X)` is a covariate function, residual ⟂. have hh_meas : Measurable (fun x => S.mVal x - η.mFn x) := S.mVal_meas.sub η.mMeas have hresid_int : Integrable S.resid P.μ := by have : S.resid = fun ω => S.factualD ω - S.mReg ω := rfl rw [this] exact hD.sub MeasureTheory.integrable_condExp have hwg_int : Integrable (fun ω => S.resid ω * (S.mVal (S.factualX ω) - η.mFn (S.factualX ω))) P.μ := by have hae : (fun ω => S.resid ω * (S.mVal (S.factualX ω) - η.mFn (S.factualX ω))) =ᵐ[P.μ] fun ω => V₀ ω * Δm ω := by filter_upwards [S.mVal_compat] with ω hω simp only [hV₀_def, hΔm_def] have hr : S.resid ω = S.factualD ω - S.mReg ω := rfl rw [hr, hω] exact (hcross.congr hae.symm) exact S.integral_condExpZero_mul_comp_factualX hh_meas (S.condExp_resid_sigmaX hD) hresid_int hwg_int rw [hcross_zero] simp only [hΔm_def, mul_zero, zero_sub]
MeanZero 2 core · 0 supporting This file proves the two partially linear score facts consumed by the double machine-learning engine: plr_meanZero, the population mean-zero identity at the truth, and plr_finite_var, finite second moment of the true sco ★ plr_meanZero★ plr_finite_var
Mean-zero and finite variance for the partially linear score
This file proves the two partially linear score facts consumed by the double
machine-learning engine: plr_meanZero, the population mean-zero identity at the
truth, and plr_finite_var, finite second moment of the true score under the
observed-data law.
lemma plr_meanZero reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
If the structural error is integrable, the product of the structural error and the true treatment residual is integrable, the baseline covariate function is integrable, and the treatment is integrable, then the Robinson partialling-out score, evaluated at the true outcome and treatment regressions and the true structural slope, has zero mean under the observed-data law.
Formal statement
hypotheses
γ :
Type u_1
hU :
Integrable S.U P.μ
hUV :
Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ
hbX :
Integrable (fun ω => S.b (S.factualX ω)) P.μ
hD :
Integrable S.factualD P.μ
conclusion
MeanZero S.plrGeneralMoment
Proof (Lean source)
lemma plr_meanZero
(hU : Integrable S.U P.μ)
(hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ)
(hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ)
(hD : Integrable S.factualD P.μ) :
MeanZero S.plrGeneralMoment := by
change ∫ z, plrMomentFunctional S.η₀ z S.θ₀ ∂S.P_Z = 0
rw [S.integral_P_Z (measurable_plrMomentFunctional S.η₀ S.θ₀)]
have hae :
(fun ω => plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀)
=ᵐ[P.μ] fun ω => S.U ω * S.toPOPartialLinearModel.resid ω := by
filter_upwards [S.lVal_compat, S.mVal_compat, S.factualY_sub_lReg hD hbX hU]
with ω hl hm hY
rw [S.plrMomentFunctional_factualZ ω, hl, hm]
have hresid : S.toPOPartialLinearModel.resid ω = S.factualD ω - S.mReg ω := rfl
rw [← hresid, hY]
ring
rw [integral_congr_ae hae, S.integral_U_resid hU hUV]
lemma plr_finite_var reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
If the squared Robinson partialling-out score — evaluated at the true outcome and treatment regressions and the true structural slope, pulled back to the population space — is integrable, then the squared score is integrable under the observed-data law , i.e. the score has finite variance at the truth.
Formal statement
hypotheses
γ :
Type u_1
hsq :
Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ
conclusion
Integrable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) S.P_Z
Proof (Lean source)
lemma plr_finite_var
(hsq : Integrable
(fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ) :
Integrable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) S.P_Z := by
have hg : AEStronglyMeasurable
(fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) S.P_Z :=
((measurable_plrMomentFunctional S.η₀ S.θ₀).pow_const 2).aestronglyMeasurable
change Integrable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) (P.μ.map S.factualZ)
rw [MeasureTheory.integrable_map_measure hg S.measurable_factualZ.aemeasurable]
exact hsq
RemainderBound 1 core · 1 supporting This file proves the doubly-robust bilinear bound on the population moment at an estimated nuisance, the analytic heart of the partially linear DML guarantee. ★ plr_remainder_bound
Doubly-robust remainder for the partially linear score
This file proves the doubly-robust bilinear bound on the population moment at an
estimated nuisance, the analytic heart of the partially linear DML guarantee.
The helper integral_condExpZero_mul_comp_factualX turns conditional
mean-zero-with-respect-to-σ(X) into orthogonality against covariate functions,
and plr_remainder_bound applies that orthogonality to bound the partially
linear population score by the product of outcome- and treatment-regression
L²(P_X) errors.
lemma plr_remainder_bound reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Doubly-robust bilinear remainder. Fix any candidate nuisance pair η of outcome and treatment regressions. Assume the treatment, the baseline covariate function, and the structural error are integrable; that the outcome- and treatment-regression errors of η and the true treatment residual are square-integrable; and that the resulting orthogonal cross terms and the true structural-error/treatment-residual product are all integrable. Then the population Robinson partialling-out score at η and the true structural slope is bounded in absolute value by times the product of the two L²(P_X) nuisance-error seminorms:
Formal statement
hypotheses
γ :
Type u_1
η :
hD :
Integrable S.factualD P.μ
hbX :
Integrable (fun ω => S.b (S.factualX ω)) P.μ
hU :
Integrable S.U P.μ
hΔl :
MemLp (fun x => η.lFn x - S.lVal x) 2 S.P_X
hΔm :
MemLp (fun x => η.mFn x - S.mVal x) 2 S.P_X
hV :
MemLp S.resid 2 P.μ
L¹ control of the orthogonal cross terms (each derivable from the above by Cauchy–Schwarz, but kept as explicit integrability hypotheses).
hUΔm :
Integrable (fun ω => S.U ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ
hΔlV :
Integrable (fun ω => (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) * S.resid ω) P.μ
hVΔm :
Integrable (fun ω => S.resid ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ
hUV :
Integrable (fun ω => S.U ω * S.resid ω) P.μ
conclusion
|∫ z, plrMomentFunctional η z S.θ₀ ∂S.P_Z|
Proof (Lean source)
lemma plr_remainder_bound (η : PLRNuisance γ)
(hD : Integrable S.factualD P.μ)
(hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ)
(hU : Integrable S.U P.μ)
(hΔl : MemLp (fun x => η.lFn x - S.lVal x) 2 S.P_X)
(hΔm : MemLp (fun x => η.mFn x - S.mVal x) 2 S.P_X)
(hV : MemLp S.resid 2 P.μ)
-- L¹ control of the orthogonal cross terms (each derivable from the above
-- by Cauchy–Schwarz, but kept as explicit integrability hypotheses).
(hUΔm : Integrable
(fun ω => S.U ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ)
(hΔlV : Integrable
(fun ω => (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) * S.resid ω) P.μ)
(hVΔm : Integrable
(fun ω => S.resid ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ)
(hUV : Integrable (fun ω => S.U ω * S.resid ω) P.μ) :
|∫ z, plrMomentFunctional η z S.θ₀ ∂S.P_Z|
≤ (1 + |S.θ₀|)
* ((S.plrGeneralMoment.ρ₁ η S.η₀ : NNReal) : ℝ)
* ((S.plrGeneralMoment.ρ₂ η S.η₀ : NNReal) : ℝ) := by
-- Notation for the two pulled-back nuisance errors.
set δl : P.Ω → ℝ := fun ω => η.lFn (S.factualX ω) - S.lVal (S.factualX ω) with hδl_def
set δm : P.Ω → ℝ := fun ω => η.mFn (S.factualX ω) - S.mVal (S.factualX ω) with hδm_def
-- L²(μ) membership of the pulled-back errors, transported from L²(P_X).
have hδl : MemLp δl 2 P.μ :=
hΔl.comp_of_map (f := S.factualX) S.measurable_factualX.aemeasurable
have hδm : MemLp δm 2 P.μ :=
hΔm.comp_of_map (f := S.factualX) S.measurable_factualX.aemeasurable
-- Step 1: change of variables to the `μ`-level integral.
rw [S.integral_P_Z (measurable_plrMomentFunctional η S.θ₀)]
-- Step 2: pointwise-a.e. rewrite of the integrand.
have hae :
(fun ω => plrMomentFunctional η (S.factualZ ω) S.θ₀)
=ᵐ[P.μ] fun ω => (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω) := by
filter_upwards [S.lVal_compat, S.mVal_compat, S.factualY_sub_lReg hD hbX hU]
with ω hl hm hY
simp only [plrMomentFunctional, plrResidual, hδl_def, hδm_def]
change (S.factualY ω - η.lFn (S.factualX ω)
- S.θ₀ * (S.factualD ω - η.mFn (S.factualX ω)))
* (S.factualD ω - η.mFn (S.factualX ω))
= (S.U ω - (η.lFn (S.factualX ω) - S.lVal (S.factualX ω))
+ S.θ * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω)))
* (S.resid ω - (η.mFn (S.factualX ω) - S.mVal (S.factualX ω)))
have hr : S.resid ω = S.factualD ω - S.mReg ω := rfl
have ht : S.θ₀ = S.θ := rfl
rw [ht]
rw [hr] at hY ⊢
rw [hl, hm]
linear_combination (S.factualD ω - η.mFn (S.factualX ω)) * hY
rw [integral_congr_ae hae]
-- `δl, δm` are σ(X)-pullbacks, hence orthogonal to `U` and `resid`.
have hδl_meas : Measurable (fun x => η.lFn x - S.lVal x) := η.lMeas.sub S.lVal_meas
have hδm_meas : Measurable (fun x => η.mFn x - S.mVal x) := η.mMeas.sub S.mVal_meas
-- Step 3: the three orthogonal cross terms vanish.
have h_U_resid : ∫ ω, S.U ω * S.resid ω ∂P.μ = 0 := S.integral_U_resid hU hUV
have h_U_δm : ∫ ω, S.U ω * δm ω ∂P.μ = 0 := by
rw [hδm_def]
exact S.integral_condExpZero_mul_comp_factualX hδm_meas
S.condExp_U_sigmaX hU hUΔm
have h_δl_resid : ∫ ω, δl ω * S.resid ω ∂P.μ = 0 := by
have hcomm : (fun ω => δl ω * S.resid ω)
= fun ω => S.resid ω * (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) := by
funext ω; rw [hδl_def]; ring
rw [hcomm]
exact S.integral_condExpZero_mul_comp_factualX hδl_meas
(S.condExp_resid_sigmaX hD) (hV.integrable (by norm_num))
(by simpa [mul_comm] using hΔlV)
have h_δm_resid : ∫ ω, δm ω * S.resid ω ∂P.μ = 0 := by
have hcomm : (fun ω => δm ω * S.resid ω)
= fun ω => S.resid ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω)) := by
funext ω; rw [hδm_def]; ring
rw [hcomm]
exact S.integral_condExpZero_mul_comp_factualX hδm_meas
(S.condExp_resid_sigmaX hD) (hV.integrable (by norm_num)) hVΔm
-- Cauchy–Schwarz integrability of the two surviving (`δl·δm`, `δm²`) terms.
haveI : ENNReal.HolderTriple (2 : ENNReal) (2 : ENNReal) (1 : ENNReal) := by
constructor; simpa using ENNReal.inv_two_add_inv_two
have hδlδm_memLp : MemLp (fun ω => δl ω * δm ω) 1 P.μ := MemLp.mul' hδm hδl
have hδmsq_memLp : MemLp (fun ω => δm ω * δm ω) 1 P.μ := MemLp.mul' hδm hδm
have hδlδm_int : Integrable (fun ω => δl ω * δm ω) P.μ :=
hδlδm_memLp.integrable le_rfl
have hδmsq_int : Integrable (fun ω => δm ω * δm ω) P.μ :=
hδmsq_memLp.integrable le_rfl
-- Integrability of every product term in the expansion.
have hUδm_int : Integrable (fun ω => S.U ω * δm ω) P.μ := by
rw [hδm_def]; exact hUΔm
have hδlresid_int : Integrable (fun ω => δl ω * S.resid ω) P.μ := by
rw [hδl_def]; exact hΔlV
have hδmresid_int : Integrable (fun ω => δm ω * S.resid ω) P.μ := by
rw [hδm_def]; simpa [mul_comm] using hVΔm
-- Step 3 (cont.): expand the integral; only `∫δl·δm − θ·∫δm²` survives.
-- Integrability of the grouped sub-expressions, stated in pointwise form so
-- the `integral_add` / `integral_sub` rewrites match the integrand.
have hA1 : Integrable (fun ω => S.U ω * S.resid ω - S.U ω * δm ω) P.μ :=
hUV.sub hUδm_int
have hA2 :
Integrable
(fun ω => S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω) P.μ :=
hA1.sub hδlresid_int
have hA3 :
Integrable
(fun ω => S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω
+ δl ω * δm ω) P.μ :=
hA2.add hδlδm_int
have hB :
Integrable
(fun ω => S.θ * (δm ω * S.resid ω) - S.θ * (δm ω * δm ω)) P.μ :=
(hδmresid_int.const_mul S.θ).sub (hδmsq_int.const_mul S.θ)
have hint_eq :
∫ ω, (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω) ∂P.μ
= ∫ ω, δl ω * δm ω ∂P.μ - S.θ * ∫ ω, δm ω * δm ω ∂P.μ := by
have hexp :
(fun ω => (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω))
= fun ω =>
(S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω
+ δl ω * δm ω)
+ (S.θ * (δm ω * S.resid ω) - S.θ * (δm ω * δm ω)) := by
funext ω; ring
rw [hexp, integral_add hA3 hB, integral_add hA2 hδlδm_int,
integral_sub hA1 hδlresid_int, integral_sub hUV hUδm_int,
integral_sub (hδmresid_int.const_mul S.θ) (hδmsq_int.const_mul S.θ),
integral_const_mul, integral_const_mul,
h_U_resid, h_U_δm, h_δl_resid, h_δm_resid]
ring
rw [hint_eq]
-- Step 4: the bound. Abbreviate the two L²(P_X) nuisance errors.
set a : ℝ := (eLpNorm (fun x => η.lFn x - S.lVal x) 2 S.P_X).toReal with ha_def
set b : ℝ := (eLpNorm (fun x => η.mFn x - S.mVal x) 2 S.P_X).toReal with hb_def
have ha_nonneg : 0 ≤ a := ENNReal.toReal_nonneg
have hb_nonneg : 0 ≤ b := ENNReal.toReal_nonneg
-- The right-hand side is `(1 + |θ₀|)·(max a b)·(max a b)`.
have hrhs1 : ((S.plrGeneralMoment.ρ₁ η S.η₀ : NNReal) : ℝ) = max a b := by
-- `NNReal.coe_mk` no longer fires as a simp rewrite; it is still `rfl`.
simp only [plrGeneralMoment, η₀, ← ha_def, ← hb_def]
rfl
have hrhs2 : ((S.plrGeneralMoment.ρ₂ η S.η₀ : NNReal) : ℝ) = max a b := by
-- `NNReal.coe_mk` no longer fires as a simp rewrite; it is still `rfl`.
simp only [plrGeneralMoment, η₀, ← ha_def, ← hb_def]
rfl
rw [hrhs1, hrhs2]
-- L²(μ) ↔ L²(P_X) bridge for the two pulled-back nuisance errors.
have hbridge_l : (eLpNorm δl 2 P.μ).toReal = a := by
rw [ha_def, hδl_def, P_X,
eLpNorm_map_measure hδl_meas.aestronglyMeasurable
S.measurable_factualX.aemeasurable]
rfl
have hbridge_m : (eLpNorm δm 2 P.μ).toReal = b := by
rw [hb_def, hδm_def, P_X,
eLpNorm_map_measure hδm_meas.aestronglyMeasurable
S.measurable_factualX.aemeasurable]
rfl
-- Cauchy–Schwarz on `δl·δm` and on `δm²` (over `μ`).
have hCS_lm : ∫ ω, |δl ω * δm ω| ∂P.μ ≤ a * b := by
have h := integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := P.μ) hδl hδm
rwa [hbridge_l, hbridge_m] at h
have hCS_mm : ∫ ω, |δm ω * δm ω| ∂P.μ ≤ b * b := by
have h := integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := P.μ) hδm hδm
rwa [hbridge_m] at h
-- `∫ δm² = ∫ |δm·δm| ≥ 0`.
have hδmsq_abs : (fun ω => δm ω * δm ω) = fun ω => |δm ω * δm ω| := by
funext ω; rw [abs_of_nonneg (mul_self_nonneg (δm ω))]
have hδmsq_nonneg : 0 ≤ ∫ ω, δm ω * δm ω ∂P.μ :=
integral_nonneg fun ω => mul_self_nonneg (δm ω)
-- `|∫ δl·δm| ≤ ∫ |δl·δm| ≤ a·b`.
have hbound_lm : |∫ ω, δl ω * δm ω ∂P.μ| ≤ a * b :=
(abs_integral_le_integral_abs).trans hCS_lm
-- `∫ δm² ≤ b²`.
have hbound_mm : ∫ ω, δm ω * δm ω ∂P.μ ≤ b * b := by
calc ∫ ω, δm ω * δm ω ∂P.μ = ∫ ω, |δm ω * δm ω| ∂P.μ := by rw [hδmsq_abs]
_ ≤ b * b := hCS_mm
-- Triangle inequality and the `max` bound.
have hθ : S.θ₀ = S.θ := rfl
have ha_le : a ≤ max a b := le_max_left a b
have hb_le : b ≤ max a b := le_max_right a b
have hmax_nonneg : 0 ≤ max a b := le_trans ha_nonneg ha_le
calc |∫ ω, δl ω * δm ω ∂P.μ - S.θ * ∫ ω, δm ω * δm ω ∂P.μ|
≤ |∫ ω, δl ω * δm ω ∂P.μ| + |S.θ * ∫ ω, δm ω * δm ω ∂P.μ| :=
abs_sub _ _
_ = |∫ ω, δl ω * δm ω ∂P.μ| + |S.θ| * (∫ ω, δm ω * δm ω ∂P.μ) := by
rw [abs_mul, abs_of_nonneg hδmsq_nonneg]
_ ≤ a * b + |S.θ| * (b * b) :=
add_le_add hbound_lm
(mul_le_mul_of_nonneg_left hbound_mm (abs_nonneg _))
_ ≤ max a b * max a b + |S.θ| * (max a b * max a b) := by
gcongr
_ = (1 + |S.θ₀|) * max a b * max a b := by rw [hθ]; ring
1 supporting declaration (lemmas, instances)
-
integral_condExpZero_mul_comp_factualXlemma — Orthogonality of a σ(X)-conditionally-mean-zero variable w to any covariate function h(X): E[w·h(X)] = 0. Mirrors integral_U_resid, but the σ-algebra is σ(X) (so h(X) pulls out of the conditional expectation) instead of σ(X,D). Used to kill the three orthogonal cross terms U·Δm, Δℓ·V, V·Δm in the doubly-robust remainder.hypothesesγ :sharedType u_1w :P.Ω → ℝh :γ → ℝhh :hwz :P.μ[w | S.sigmaX] =ᵐ[P.μ] 0hw :Integrable w P.μhwg :Integrable (fun ω => w ω * h (S.factualX ω)) P.μconclusion∫ ω, w ω * h (S.factualX ω) ∂P.μ = 0Proof (Lean source)
lemma integral_condExpZero_mul_comp_factualX {w : P.Ω → ℝ} {h : γ → ℝ} (hh : Measurable h) (hwz : P.μ[w | S.sigmaX] =ᵐ[P.μ] 0) (hw : Integrable w P.μ) (hwg : Integrable (fun ω => w ω * h (S.factualX ω)) P.μ) : ∫ ω, w ω * h (S.factualX ω) ∂P.μ = 0 := by -- `h(X)` is `σ(X)`-strongly-measurable. have hg_sm : StronglyMeasurable[S.sigmaX] (fun ω => h (S.factualX ω)) := by change StronglyMeasurable[comap S.factualX inferInstance] (fun ω => h (S.factualX ω)) exact (hh.comp (comap_measurable S.factualX)).stronglyMeasurable -- `w·h(X) = h(X)·w` is integrable up to commutativity. have hgw_int : Integrable (fun ω => h (S.factualX ω) * w ω) P.μ := by simpa [mul_comm] using hwg -- Pull `h(X)` out of the conditional expectation, then `E[w|σX] = 0`. have hpull : P.μ[fun ω => h (S.factualX ω) * w ω | S.sigmaX] =ᵐ[P.μ] (fun ω => h (S.factualX ω)) * P.μ[w | S.sigmaX] := MeasureTheory.condExp_mul_of_stronglyMeasurable_left (μ := P.μ) (m := S.sigmaX) hg_sm hgw_int hw have hce_zero : P.μ[fun ω => h (S.factualX ω) * w ω | S.sigmaX] =ᵐ[P.μ] (fun _ => (0 : ℝ)) := by refine hpull.trans ?_ filter_upwards [hwz] with ω hω rw [Pi.mul_apply, hω, Pi.zero_apply, mul_zero] calc ∫ ω, w ω * h (S.factualX ω) ∂P.μ = ∫ ω, h (S.factualX ω) * w ω ∂P.μ := by simp_rw [mul_comm] _ = ∫ ω, P.μ[fun ω => h (S.factualX ω) * w ω | S.sigmaX] ω ∂P.μ := by rw [MeasureTheory.integral_condExp S.sigmaX_le] _ = ∫ _, (0 : ℝ) ∂P.μ := MeasureTheory.integral_congr_ae hce_zero _ = 0 := MeasureTheory.integral_zero _ _
ScoreL2 1 core · 0 supporting This file provides the standalone lemma plr_score_diff_isLittleOp_one, which discharges the score-difference o_p(1) hypothesis of the partially linear DML asymptotic-linearity theorem from boundedness of the truth residu ★ plr_score_diff_isLittleOp_one
Partially linear score L²(P_Z) o_p(1) continuity
This file provides the standalone lemma plr_score_diff_isLittleOp_one, which
discharges the score-difference o_p(1) hypothesis of the partially linear DML
asymptotic-linearity theorem from boundedness of the truth residuals, uniform
boundedness of the nuisance errors, and the two individual L²(P_X) nuisance
rates.
theorem plr_score_diff_isLittleOp_one reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Score-difference L²(P_Z) o_p(1) for the partially linear model. Suppose three nonnegative bounding constants Ca, Cv, Cm satisfy: the residualized outcome is almost surely bounded by Ca under the observed-data law; the true treatment residual is almost surely bounded by Cv; and the treatment-regression estimation error of η_hat is uniformly bounded by Cm at every fold, draw, and covariate value. Suppose further that for the estimated nuisance sequence η_hat on the system S, the outcome- and treatment-regression estimation errors are square-integrable over the covariate law at every fold and draw, and that both regression errors converge to zero in L²(P_X) at rate . Then the L²(P_Z)-seminorm of the Robinson partialling-out score difference between the estimated and the true nuisance is itself .
Formal statement
hypotheses
γ :
Type u_1
S :
PLRSystem P γ
η_hat :
ℕ → P.Ω → PLRNuisance γ
Ca Cv Cm :
ℝ
hCa :
0 ≤ Ca
hCv :
0 ≤ Cv
hCm :
0 ≤ Cm
hA_bdd :
∀ᵐ z ∂S.P_Z, |z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)| ≤ Ca
hv_bdd :
∀ᵐ z ∂S.P_Z, |z.2.1 - S.mVal z.1| ≤ Cv
hΔm_bdd :
∀ n ω x, |S.mVal x - (η_hat n ω).mFn x| ≤ Cm
hΔl_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X
hΔm_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X
h_l_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_m_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
conclusion
IsLittleOp (fun n ω => (eLpNorm (fun z => plrMomentFunctional (η_hat n ω) z S.θ₀ - plrMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ
Proof (Lean source)
theorem plr_score_diff_isLittleOp_one
(S : PLRSystem P γ)
(η_hat : ℕ → P.Ω → PLRNuisance γ)
{Ca Cv Cm : ℝ} (hCa : 0 ≤ Ca) (hCv : 0 ≤ Cv) (hCm : 0 ≤ Cm)
(hA_bdd : ∀ᵐ z ∂S.P_Z,
|z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)| ≤ Ca)
(hv_bdd : ∀ᵐ z ∂S.P_Z, |z.2.1 - S.mVal z.1| ≤ Cv)
(hΔm_bdd : ∀ n ω x, |S.mVal x - (η_hat n ω).mFn x| ≤ Cm)
(hΔl_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X)
(hΔm_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X)
(h_l_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_m_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ) :
IsLittleOp
(fun n ω => (eLpNorm (fun z => plrMomentFunctional (η_hat n ω) z S.θ₀
- plrMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ := by
classical
-- The two L²(P_X) rate functions and their sum.
set rateL : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X).toReal with hrateL
set rateM : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X).toReal with hrateM
have hrateL_nonneg : ∀ n ω, 0 ≤ rateL n ω := fun _ _ => ENNReal.toReal_nonneg
have hrateM_nonneg : ∀ n ω, 0 ≤ rateM n ω := fun _ _ => ENNReal.toReal_nonneg
-- Sum of the two rates is `o_p(1)`.
have hsum_rate :
IsLittleOp (fun n ω => rateL n ω + rateM n ω) (fun _ => (1 : ℝ)) P.μ :=
IsLittleOp.add_one h_l_rate h_m_rate
-- The combined constant.
set Cconst : ℝ := Ca + Cv + Cm + |S.θ₀| * Cv + |S.θ₀| * Cm with hCconst
have hCconst_pos : 0 < Cconst + 1 := by
have : 0 ≤ Cconst := by
have hθ : 0 ≤ |S.θ₀| := abs_nonneg _
have : 0 ≤ |S.θ₀| * Cv := mul_nonneg hθ hCv
have : 0 ≤ |S.θ₀| * Cm := mul_nonneg hθ hCm
positivity
linarith
-- Reduce to a constant multiple of the rate sum, then apply the per-`(n, ω)`
-- quantitative bound.
refine IsLittleOp.of_abs_le_const_mul_one (C := Cconst + 1) hCconst_pos hsum_rate ?_
intro n ω
exact plr_score_diff_abs_le S η_hat n ω hCa hCv hCm Cconst rateL rateM
hrateL hrateM hrateL_nonneg hrateM_nonneg hCconst
hA_bdd hv_bdd hΔm_bdd hΔl_memLp hΔm_memLp