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 3neg := negclause 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
Neyman-orthogonal second-order 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
linScale := -S.residSecondMoment
clause 10
linScale_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 1 core · 1 supporting This file delivers pointwise asymptotic linearity and √|B|-asymptotic normality for a one-shot, fold-B estimator of the structural slope in the partially linear model. ★ plr_oneStepOracleDML_tendstoNormal
Oracle one-step partially linear DML theorems
This file delivers pointwise asymptotic linearity and √|B|-asymptotic normality for a one-shot, fold-B estimator of the structural slope in the partially linear model. It composes the abstract one-shot engine with the three model-specific analytic facts (mean zero, finite variance, and a second-order remainder) and the generic asymptotic-linearity ⇒ normality bridge. It is not a K-fold DML1 or DML2 limit theorem.
theorem plr_oneStepOracleDML_tendstoNormal reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Oracle one-step 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 in the nuisance-training fold jointly with the observation, and integrable and square-integrable at every fold and draw; the residual factors have finite fourth moments, the nuisance errors have finite fourth moments, a common envelope is nonnegative, that envelope bounds both fourth moments, and both fourth-moment errors are , implying L² score convergence; 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_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
hA_memLp :
MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z
hv_memLp :
MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z
B :
ℝ
hB :
0 ≤ B
hΔl4_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X
hΔm4_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X
h_l_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_m_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)
hθn_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n,
AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ
conclusion
Modes.TendstoInLaw (fun _ => P.μ) (IsAsymLinear.rescaledEstimator (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z))
Proof (Lean source)
theorem plr_oneStepOracleDML_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_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)
(hA_memLp : MemLp
(fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z)
(hv_memLp : MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z)
{B : ℝ} (hB : 0 ≤ B)
(hΔl4_memLp : ∀ n ω,
MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X)
(hΔm4_memLp : ∀ n ω,
MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X)
(hΔl4_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal ≤ B)
(hΔm4_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).toReal ≤ B)
(h_l_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_m_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀))
(hθn_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(oneStepOracleDML S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => -S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)
split.foldB n) P.μ) :
Modes.TendstoInLaw (fun _ => P.μ)
(IsAsymLinear.rescaledEstimator
(oneStepOracleDML S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB)
atTop (gaussianMeasure 0
(∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2
∂S.P_Z)) := by
have hAL :=
S.plr_oneStepOracleDML_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_uncurry h_m_int h_m_sq_int
hA_memLp hv_memLp hB hΔl4_memLp hΔm4_memLp hΔl4_bound hΔm4_bound
h_l_rate h_m_rate h_product_rate
exact hAL.tendsto_normal_foldB split hψ_meas hθn_meas hSum_meas
1 supporting declaration (lemmas, instances)
-
plr_oneStepOracleDML_isAsymLineartheorem — Oracle one-step 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, measurable in the training fold jointly with the observation, and integrable/square-integrable at every fold; the true residual factors have finite fourth moments, the nuisance errors have finite fourth moments bounded almost surely by a common nonnegative envelope, and both fourth-moment nuisance errors are $o_p(1)$; and the product of the two nuisance-error seminorms is $o_p(n^{-1/2})$; then the one-step double-machine-learning estimator of the structural slope is asymptotically linear at the true slope, with influence function $-J_0^{-1}\psi(\eta_0,\cdot,\theta_0)$ — the inverse-Jacobian-scaled Robinson partialling-out score at the truth.hypothesesγ :sharedType u_1S :PLRSystem P γsample :IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Zsplit :OneShotSplit samplec :ℝ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, ω)` second-order 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_XhΔm :∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_XhUΔ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 `oneStepOracleDML_isAsymLinear_of_ae` 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_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_Zh_m_sq_int :∀ n ω,Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_ZhA_memLp :MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Zhv_memLp :MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_ZB :ℝhB :0 ≤ BhΔl4_memLp :∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_XhΔm4_memLp :∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_Xh_l_rate :IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μh_m_rate :IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.μconclusionIsAsymLinear (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ (fun z => -S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) sample split.foldBProof (Lean source)
theorem plr_oneStepOracleDML_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, ω)` second-order 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 -- `oneStepOracleDML_isAsymLinear_of_ae` 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_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) (hA_memLp : MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z) (hv_memLp : MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z) {B : ℝ} (hB : 0 ≤ B) (hΔl4_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X) (hΔm4_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X) (hΔl4_bound : ∀ n, ∀ᵐ ω ∂P.μ, (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal ≤ B) (hΔm4_bound : ∀ n, ∀ᵐ ω ∂P.μ, (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).toReal ≤ B) (h_l_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_m_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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 (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ (fun z => -S.plrGeneralMoment.linScaleInv * 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 have h_score_diff_rate := S.plr_score_diff_isLittleOp_one η_hat hA_memLp hv_memLp hB hΔl4_memLp hΔm4_memLp hΔl4_bound hΔm4_bound h_l_rate h_m_rate simpa [plrGeneralMoment] using (oneStepOracleDML_isAsymLinear_of_ae S.plrGeneralMoment hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := Crem) (fun n => Eventually.of_forall (hBR_at n)) h_m_meas h_m_foldA_uncurry (fun n => Eventually.of_forall (h_m_int n)) (fun n => Eventually.of_forall (h_m_sq_int n)) h_score_diff_rate h_product_rate)
Feasible 2 core · 1 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_of_rates
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 lemma
plr_dml_feasible_tendstoNormal_of_jacobianConsistency reduces its pointwise
√|B|-asymptotic normality, conditional on empirical Jacobian consistency, to
the one-step normality theorem plr_oneStepOracleDML_tendstoNormal by the
standard asymptotic-equivalence argument. The final theorem
plr_dml_feasible_tendstoNormal_of_rates derives that consistency from
explicit nuisance-rate, Jacobian-increment-rate, moment, and fold-measurability
conditions. Neither theorem is a K-fold DML1/DML2 result.
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_of_rates reviewed
⚑ flagged
Causalean.Estimation.PLR.PLRSystem
Feasible one-shot partially linear asymptotic normality from nuisance and Jacobian-increment rates. For a partially linear system on a probability space with measurable covariates, an i.i.d. observed-data sample, an evaluation split whose share of the sample converges to a positive limit c, and training-fold outcome- and treatment-regression estimates, 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; at every sample size and realization the outcome- and treatment-regression errors are square-integrable under the covariate law, and their cross-products with the structural error and the treatment residual are integrable; the estimated score at the true slope is jointly measurable in the realization and the observation, and measurable with respect to the product of the σ-algebra generated by the training-fold observations and the observation σ-algebra, and is integrable and square-integrable at every realization; the outcome residual net of the true slope times the treatment residual, and the treatment residual, have finite fourth moments; both regression errors have finite fourth moments under the covariate law, a constant B ≥ 0 bounds both fourth-moment norms almost surely at every sample size, and both fourth-moment norms are o_p(1); the L² treatment-regression error times the sum of the L² outcome- and treatment-regression errors is o_p(n^(−1/2)); the influence function is measurable and the rescaled oracle estimator, the normalized influence sum, and the rescaled feasible estimator are almost-everywhere measurable at every sample size; minus the squared true treatment residual is square-integrable under the observed-data law; at every realization the treatment-regression error is square-integrable, both under the population law and under the covariate law, and its product with the true treatment residual is integrable; the L² treatment-regression error is o_p(1); and the change in minus the squared treatment residual caused by replacing the true treatment regression with the estimated one is jointly measurable, measurable with respect to the same training-fold product σ-algebra, square-integrable, and o_p(1) in L². Then the feasible partialling-out estimator, the evaluation-fold sum of estimated outcome residual times estimated treatment residual divided by the evaluation-fold sum of squared estimated treatment residuals, centered at the true slope and scaled by the square root of the evaluation-fold size, converges in distribution to the centered Gaussian whose variance is the second moment of the true orthogonal score divided by the square of the mean squared treatment residual.
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_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
hA_memLp :
MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z
hv_memLp :
MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z
B :
ℝ
hB :
0 ≤ B
hΔl4_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X
hΔm4_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X
h_l_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_m4_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)
hθn_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ
hSum_meas :
∀ n,
AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ
hθn_feas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ
hg0_memLp :
MemLp (plrMomentA S.η₀) 2 S.P_Z
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.μ
hΔm_memLp :
∀ n ω, MemLp (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X
h_m_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
hΔa_meas :
∀ n,
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))
hΔa_memLp :
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
Modes.TendstoInLaw (fun _ => P.μ) (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z))
Proof (Lean source)
theorem plr_dml_feasible_tendstoNormal_of_rates
(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_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)
(hA_memLp : MemLp
(fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z)
(hv_memLp : MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z)
{B : ℝ} (hB : 0 ≤ B)
(hΔl4_memLp : ∀ n ω,
MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X)
(hΔm4_memLp : ∀ n ω,
MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X)
(hΔl4_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal ≤ B)
(hΔm4_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).toReal ≤ B)
(h_l_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_m4_rate : IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀))
(hθn_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(oneStepOracleDML S.plrGeneralMoment sample split η_hat)
S.θ₀ split.foldB n) P.μ)
(hSum_meas : ∀ n, AEMeasurable
(IsAsymLinear.normalizedSum sample
(fun z => -S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)
split.foldB n) P.μ)
(hθn_feas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ)
(hg0_memLp : MemLp (plrMomentA S.η₀) 2 S.P_Z)
(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.μ)
(hΔm_memLp : ∀ n ω,
MemLp (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X)
(h_m_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(hΔa_meas :
∀ n, Measurable (uncurry
(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)))
(hΔa_memLp : ∀ n ω,
MemLp (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z)
(hΔa_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z)
2 S.P_Z).toReal)
(fun _ => (1 : ℝ)) P.μ) :
Modes.TendstoInLaw (fun _ => P.μ)
(IsAsymLinear.rescaledEstimator
(plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB)
atTop (gaussianMeasure 0
(∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2
∂S.P_Z)) := by
have hJ_consist := S.plr_jacobian_consistency sample split η_hat hD
hg0_memLp hΔm_sq hcross hΔm_memLp h_m_rate
hΔa_meas hΔa_uncurry_foldA hΔa_memLp hΔa_rate
exact S.plr_dml_feasible_tendstoNormal_of_jacobianConsistency 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_uncurry h_m_int h_m_sq_int
hA_memLp hv_memLp hB hΔl4_memLp hΔm4_memLp hΔl4_bound hΔm4_bound
h_l_rate h_m4_rate h_product_rate hψ_meas hθn_meas hSum_meas hJ_consist hθn_feas
1 supporting declaration (lemmas, instances)
-
plr_dml_feasible_tendstoNormal_of_jacobianConsistencytheorem — Conditional feasible partially linear DML asymptotic-normality lemma. For a partially linear estimation system on a finite probability space with measurable covariates, an i.i.d. sample of covariate-treatment-outcome triples, and a sample split whose evaluation-fold share converges to a fixed positive limit c, 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 in the nuisance-training fold jointly with the observation, and integrable and square-integrable at every fold and draw; the true residual factors and nuisance errors satisfy the fourth-moment, almost-sure envelope, and individual $o_p(1)$ conditions that imply L² score convergence, the product of the two nuisance-error seminorms is $o_p(n^{-1/2})$; 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.hypothesesγ :sharedType u_1S :PLRSystem P γsample :IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Zsplit :OneShotSplit samplec :ℝ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_XhΔm :∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_XhUΔ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_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_Zh_m_sq_int :∀ n ω,Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_ZhA_memLp :MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Zhv_memLp :MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_ZB :ℝhB :0 ≤ BhΔl4_memLp :∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_XhΔm4_memLp :∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_Xh_l_rate :IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μh_m_rate :IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)hθn_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μhSum_meas :∀ n,AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.linScaleInv * 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 :Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => S.plrGeneralMoment.linScale)hθn_feas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μconclusionModes.TendstoInLaw (fun _ => P.μ) (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z))Proof (Lean source)
theorem plr_dml_feasible_tendstoNormal_of_jacobianConsistency (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_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) (hA_memLp : MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z) (hv_memLp : MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z) {B : ℝ} (hB : 0 ≤ B) (hΔl4_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X) (hΔm4_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X) (hΔl4_bound : ∀ n, ∀ᵐ ω ∂P.μ, (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal ≤ B) (hΔm4_bound : ∀ n, ∀ᵐ ω ∂P.μ, (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).toReal ≤ B) (h_l_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_m_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).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.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀)) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.linScaleInv * 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 : Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => S.plrGeneralMoment.linScale)) (hθn_feas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ) : Modes.TendstoInLaw (fun _ => P.μ) (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB) atTop (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.linScaleInv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)) := by -- Step 1: the one-step rescaled estimator converges to the Gaussian target. have hOS := S.plr_oneStepOracleDML_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_uncurry h_m_int h_m_sq_int hA_memLp hv_memLp hB hΔl4_memLp hΔm4_memLp hΔl4_bound hΔm4_bound h_l_rate h_m_rate h_product_rate hψ_meas hθn_meas hSum_meas -- Abbreviations. set J₀ : ℝ := S.plrGeneralMoment.linScale with hJ₀_def have hJ₀_ne : J₀ ≠ 0 := S.plrGeneralMoment.linScale_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 (oneStepOracleDML 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.linScaleInv - (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, oneStepOracleDML, GeneralMoment.linScaleInv, 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, Nat.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₀) (Modes.TendstoInLaw.tightness hOS) -- Step 3: `(Pₙmₐ)⁻¹ →ₚ J₀⁻¹`, hence `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ →ₚ 0`, i.e. `o_p(1)`. have hPmₐ_inv : Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => 1 / Pmₐ n ω) atTop (fun _ _ => 1 / J₀) := by have := inv hJ_consist hJ₀_ne simpa [hPmₐ_def, hJ₀_def] using this have hFn_inProb : Modes.TendstoInProbability (fun _ => P.μ) Fn atTop (fun _ _ => 0) := by -- `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ = (1/J₀) − (1/Pₙmₐ)`; it converges to `0`. have hconv : Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => (fun n ω => 1 / Pmₐ n ω) n ω - 1 / J₀) atTop (fun _ _ => 0) := sub_const hPmₐ_inv -- Rewrite `1/x = x⁻¹` and flip the sign to match `Fn`. have hneg : Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => -(fun n ω => 1 / Pmₐ n ω - 1 / J₀) n ω) atTop (fun _ _ => 0) := by have hcont : ContinuousAt (fun x : ℝ => -x) (0 : ℝ) := (continuous_neg).continuousAt have := Causalean.Stat.Modes.TendstoInProbability.comp_continuousAt hcont hconv 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.linScaleInv, hJ₀_def, one_div] ring rw [hFn_eq] exact hneg have hFn_littleO : IsLittleOp Fn (fun _ => (1 : ℝ)) P.μ := isLittleOp_one hFn_inProb -- 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 -- … 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; 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, measurable in the training fold jointly with the observation, 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.
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_uncurry`-style hypotheses of `plr_oneStepOracleDML_isAsymLinear`: `η̂` is fold-A trained).
hΔa_meas :
∀ n,
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
Modes.TendstoInProbability (fun _ => P.μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => S.plrGeneralMoment.linScale)
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.
(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_uncurry`-style hypotheses of `plr_oneStepOracleDML_isAsymLinear`: `η̂` is fold-A trained).
(hΔa_meas :
∀ n, Measurable (uncurry
(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.μ) :
Modes.TendstoInProbability (fun _ => P.μ)
(fun n ω => ((split.foldB n).card : ℝ)⁻¹ *
∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω))
atTop (fun _ _ => S.plrGeneralMoment.linScale) := 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.linScale with hJ₀_def
-- STEP 2: `Y₀ →ₚ J₀` by the fold-B WLLN, with the limit rewritten by step 1.
have hY₀_lim : Modes.TendstoInProbability (fun _ => P.μ) Y₀ atTop
(fun _ _ => J₀) := 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 (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 : Modes.TendstoInProbability (fun _ => P.μ) rateM atTop
(fun _ _ => 0) := tendstoInProbability_zero_of_isLittleOp_one hrateM_lo
have hrateMsq_inProb : Modes.TendstoInProbability (fun _ => P.μ)
(fun n ω => (rateM n ω) ^ 2) atTop (fun _ _ => 0) := by
have hcont : ContinuousAt (fun x : ℝ => x ^ 2) (0 : ℝ) :=
(continuous_pow 2).continuousAt
have := Causalean.Stat.Modes.TendstoInProbability.comp_continuousAt hcont hrateM_inProb
simpa using this
have hbias_inProb : Modes.TendstoInProbability (fun _ => P.μ) bias atTop
(fun _ _ => 0) := 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 := Causalean.Stat.Modes.TendstoInProbability.comp_continuousAt hcont hrateMsq_inProb
simpa using this
have hbias_lo : IsLittleOp bias (fun _ => (1 : ℝ)) P.μ :=
isLittleOp_one hbias_inProb
-- 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.μ :=
isBigOp_one
(tendstoInProbability_zero_of_isLittleOp_one hsqrt_centered)
-- 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,
Nat.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)`; return to convergence in probability.
have hY₀_sub_lo : IsLittleOp (fun n ω => Y₀ n ω - J₀) (fun _ => (1 : ℝ)) P.μ :=
isLittleOp_one
(sub_const hY₀_lim)
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 convergence in probability.
have hYn_sub_inProb : Modes.TendstoInProbability (fun _ => P.μ)
(fun n ω => Yn n ω - J₀) atTop (fun _ _ => 0) :=
tendstoInProbability_zero_of_isLittleOp_one hYn_sub_J₀_lo
-- `Yn = (Yn − J₀) + J₀`, so `Yn →ₚ J₀`.
have hfinal : Modes.TendstoInProbability (fun _ => P.μ) Yn atTop
(fun _ _ => J₀) := by
have hcont : ContinuousAt (fun x : ℝ => x + J₀) (0 : ℝ) :=
(continuous_add_const J₀).continuousAt
have := Causalean.Stat.Modes.TendstoInProbability.comp_continuousAt hcont hYn_sub_inProb
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.linScaleProof (Lean source)
lemma integral_plrMomentA_η₀_eq_J₀ (S : PLRSystem P γ) : ∫ z, plrMomentA S.η₀ z ∂S.P_Z = S.plrGeneralMoment.linScale := 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.μ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.μ) (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 a second-order bound on the population moment at an estimated nuisance, the analytic heart of the partially linear DML guarantee. ★ plr_remainder_bound
Neyman-orthogonal second-order remainder for the partially linear score
This file proves a second-order 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
Neyman-orthogonal second-order remainder. For a candidate nuisance pair η, suppose treatment is integrable, the baseline covariate term is integrable, the structural error is integrable, the outcome-regression error is square-integrable, the treatment-regression error is square-integrable, the true treatment residual is square-integrable, and the four products of structural error with treatment error, of outcome error with treatment residual, of treatment residual with treatment error, and of structural error with treatment residual are integrable. Then the population Robinson score obeys the displayed second-order L² bound:
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.
have : 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 uses `ρ₁ = b` and `ρ₂ = a + b`.
have hrhs1 : ((S.plrGeneralMoment.ρ₁ η S.η₀ : NNReal) : ℝ) = b := by
-- `NNReal.coe_mk` no longer fires as a simp rewrite; it is still `rfl`.
simp only [plrGeneralMoment, η₀, ← hb_def]
rfl
have hrhs2 : ((S.plrGeneralMoment.ρ₂ η S.η₀ : NNReal) : ℝ) = 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 stage-matched product bound.
have hθ : S.θ₀ = S.θ := rfl
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 _))
_ ≤ (a * b + |S.θ| * (b * b)) + (b * b + |S.θ| * (b * a)) := by
apply le_add_of_nonneg_right
positivity
_ = (1 + |S.θ₀|) * b * (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 Neyman-orthogonal second-order 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 L⁴ moment conditions on the tru ★ 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 L⁴ moment conditions on the truth residuals,
almost-sure L⁴ envelopes for 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) under moment conditions. For a PLR system and estimated nuisance sequence, suppose the true outcome residual and true treatment residual have finite fourth moments. Suppose the two nuisance errors have finite fourth moments, their fourth-moment norms are uniformly bounded by a nonnegative constant, and those norms converge to zero in probability. 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 γ
hA_memLp :
MemLp (fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z
hv_memLp :
MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z
B :
ℝ
hB :
0 ≤ B
hΔl_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X
hΔm_memLp :
∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X
h_l_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ
h_m_rate :
IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 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 γ)
(hA_memLp : MemLp
(fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z)
(hv_memLp : MemLp (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z)
{B : ℝ} (hB : 0 ≤ B)
(hΔl_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X)
(hΔm_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X)
(hΔl_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal ≤ B)
(hΔm_bound : ∀ n, ∀ᵐ ω ∂P.μ,
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 S.P_X).toReal ≤ B)
(h_l_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal)
(fun _ => (1 : ℝ)) P.μ)
(h_m_rate :
IsLittleOp
(fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 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
set rateL : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 4 S.P_X).toReal with hrateL
set rateM : ℕ → P.Ω → ℝ := fun n ω =>
(eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 4 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
have hsum_rate :
IsLittleOp (fun n ω => rateL n ω + rateM n ω) (fun _ => (1 : ℝ)) P.μ :=
IsLittleOp.add_one h_l_rate h_m_rate
let A4 := (eLpNorm
(fun z => z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)) 4 S.P_Z).toReal
let V4 := (eLpNorm (fun z => z.2.1 - S.mVal z.1) 4 S.P_Z).toReal
set Cconst : ℝ := A4 + V4 + B + |S.θ₀| * (V4 + B) with hCconst
have hCconst_pos : 0 < Cconst + 1 := by
have : 0 ≤ Cconst := by rw [hCconst]; positivity
linarith
refine IsLittleOp.of_ae_abs_le_const_mul_one (C := Cconst + 1)
hCconst_pos hsum_rate ?_
intro n
filter_upwards [hΔl_bound n, hΔm_bound n] with ω hL hM
let A : (γ × ℝ × ℝ) → ℝ := fun z =>
z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)
let v : (γ × ℝ × ℝ) → ℝ := fun z => z.2.1 - S.mVal z.1
let dL : (γ × ℝ × ℝ) → ℝ := fun z => S.lVal z.1 - (η_hat n ω).lFn z.1
let dM : (γ × ℝ × ℝ) → ℝ := fun z => S.mVal z.1 - (η_hat n ω).mFn z.1
let t1 := A * dM
let t2 := dL * v
let t3 := dL * dM
let t4 := S.θ₀ • (dM * v)
let t5 := S.θ₀ • (dM * dM)
have hdL4 : MemLp dL 4 S.P_Z := by
have heq := eLpNorm_comp_projX S
(g := fun x => S.lVal x - (η_hat n ω).lFn x)
(S.lVal_meas.sub (η_hat n ω).lMeas) (p := 4)
refine ⟨((S.lVal_meas.sub (η_hat n ω).lMeas).comp measurable_fst).aestronglyMeasurable, ?_⟩
rw [show dL = fun z => S.lVal z.1 - (η_hat n ω).lFn z.1 from rfl, heq]
have hfun : (fun x => S.lVal x - (η_hat n ω).lFn x) =
-(fun x => (η_hat n ω).lFn x - S.lVal x) := by
funext x
simp
rw [hfun, eLpNorm_neg]
exact (hΔl_memLp n ω).2
have hdM4 : MemLp dM 4 S.P_Z := by
have heq := eLpNorm_comp_projX S
(g := fun x => S.mVal x - (η_hat n ω).mFn x)
(S.mVal_meas.sub (η_hat n ω).mMeas) (p := 4)
refine ⟨((S.mVal_meas.sub (η_hat n ω).mMeas).comp measurable_fst).aestronglyMeasurable, ?_⟩
rw [show dM = fun z => S.mVal z.1 - (η_hat n ω).mFn z.1 from rfl, heq]
have hfun : (fun x => S.mVal x - (η_hat n ω).mFn x) =
-(fun x => (η_hat n ω).mFn x - S.mVal x) := by
funext x
simp
rw [hfun, eLpNorm_neg]
exact (hΔm_memLp n ω).2
have hdL_norm : (eLpNorm dL 4 S.P_Z).toReal = rateL n ω := by
change (eLpNorm (fun z => S.lVal z.1 - (η_hat n ω).lFn z.1) 4 S.P_Z).toReal = _
have heq := eLpNorm_comp_projX S
(g := fun x => S.lVal x - (η_hat n ω).lFn x)
(S.lVal_meas.sub (η_hat n ω).lMeas) (p := 4)
rw [heq]
have hneg : (fun x => S.lVal x - (η_hat n ω).lFn x) =
-(fun x => (η_hat n ω).lFn x - S.lVal x) := by
funext x
simp
rw [hneg, eLpNorm_neg]
have hdM_norm : (eLpNorm dM 4 S.P_Z).toReal = rateM n ω := by
change (eLpNorm (fun z => S.mVal z.1 - (η_hat n ω).mFn z.1) 4 S.P_Z).toReal = _
have heq := eLpNorm_comp_projX S
(g := fun x => S.mVal x - (η_hat n ω).mFn x)
(S.mVal_meas.sub (η_hat n ω).mMeas) (p := 4)
rw [heq]
have hneg : (fun x => S.mVal x - (η_hat n ω).mFn x) =
-(fun x => (η_hat n ω).mFn x - S.mVal x) := by
funext x
simp
rw [hneg, eLpNorm_neg]
have ht1 := eLpNorm_mul_four_toReal_le hA_memLp hdM4
have ht2 := eLpNorm_mul_four_toReal_le hdL4 hv_memLp
have ht3 := eLpNorm_mul_four_toReal_le hdL4 hdM4
have ht4base := eLpNorm_mul_four_toReal_le hdM4 hv_memLp
have ht5base := eLpNorm_mul_four_toReal_le hdM4 hdM4
let : ENNReal.HolderTriple 4 4 2 := by
change ENNReal.HolderTriple ((4 : NNReal) : ENNReal) ((4 : NNReal) : ENNReal)
((2 : NNReal) : ENNReal)
exact NNReal.HolderTriple.coe_ennreal (by norm_num)
(by constructor <;> norm_num : NNReal.HolderTriple 4 4 2)
have ht1mem : MemLp t1 2 S.P_Z := hdM4.mul hA_memLp
have ht2mem : MemLp t2 2 S.P_Z := hv_memLp.mul hdL4
have ht3mem : MemLp t3 2 S.P_Z := hdM4.mul hdL4
have ht4mem : MemLp t4 2 S.P_Z := (hv_memLp.mul hdM4).const_smul S.θ₀
have ht5mem : MemLp t5 2 S.P_Z := (hdM4.mul hdM4).const_smul S.θ₀
have hscore_eq :
(fun z => plrMomentFunctional (η_hat n ω) z S.θ₀ -
plrMomentFunctional S.η₀ z S.θ₀) = t1 + t2 + t3 + (-t4) + (-t5) := by
funext z
rw [S.score_diff_expand]
simp [t1, t2, t3, t4, t5, A, v, dL, dM, Pi.add_apply, Pi.neg_apply,
Pi.mul_apply, Pi.smul_apply, smul_eq_mul]
ring
have htri :
(eLpNorm (t1 + t2 + t3 + (-t4) + (-t5)) 2 S.P_Z).toReal ≤
(eLpNorm t1 2 S.P_Z).toReal + (eLpNorm t2 2 S.P_Z).toReal +
(eLpNorm t3 2 S.P_Z).toReal + (eLpNorm t4 2 S.P_Z).toReal +
(eLpNorm t5 2 S.P_Z).toReal := by
calc
_ ≤ (eLpNorm (t1 + t2 + t3 + (-t4)) 2 S.P_Z).toReal +
(eLpNorm (-t5) 2 S.P_Z).toReal :=
eLpNorm_add_two_toReal_le
(((ht1mem.add ht2mem).add ht3mem).add ht4mem.neg) ht5mem.neg
_ ≤ ((eLpNorm (t1 + t2 + t3) 2 S.P_Z).toReal +
(eLpNorm (-t4) 2 S.P_Z).toReal) + (eLpNorm (-t5) 2 S.P_Z).toReal := by
gcongr
exact eLpNorm_add_two_toReal_le ((ht1mem.add ht2mem).add ht3mem) ht4mem.neg
_ ≤ (((eLpNorm (t1 + t2) 2 S.P_Z).toReal + (eLpNorm t3 2 S.P_Z).toReal) +
(eLpNorm (-t4) 2 S.P_Z).toReal) + (eLpNorm (-t5) 2 S.P_Z).toReal := by
gcongr
exact eLpNorm_add_two_toReal_le (ht1mem.add ht2mem) ht3mem
_ ≤ ((((eLpNorm t1 2 S.P_Z).toReal + (eLpNorm t2 2 S.P_Z).toReal) +
(eLpNorm t3 2 S.P_Z).toReal) + (eLpNorm (-t4) 2 S.P_Z).toReal) +
(eLpNorm (-t5) 2 S.P_Z).toReal := by
gcongr
exact eLpNorm_add_two_toReal_le ht1mem ht2mem
_ = _ := by simp only [eLpNorm_neg]
rw [hscore_eq, abs_of_nonneg ENNReal.toReal_nonneg,
abs_of_nonneg (add_nonneg (hrateL_nonneg n ω) (hrateM_nonneg n ω))]
calc
_ ≤ (eLpNorm t1 2 S.P_Z).toReal + (eLpNorm t2 2 S.P_Z).toReal +
(eLpNorm t3 2 S.P_Z).toReal + (eLpNorm t4 2 S.P_Z).toReal +
(eLpNorm t5 2 S.P_Z).toReal := htri
_ ≤ A4 * rateM n ω + rateL n ω * V4 + rateL n ω * rateM n ω +
|S.θ₀| * (rateM n ω * V4) + |S.θ₀| * (rateM n ω * rateM n ω) := by
rw [show (eLpNorm t4 2 S.P_Z).toReal =
|S.θ₀| * (eLpNorm (dM * v) 2 S.P_Z).toReal by
simp [t4, eLpNorm_const_smul, Real.norm_eq_abs, ENNReal.toReal_mul],
show (eLpNorm t5 2 S.P_Z).toReal =
|S.θ₀| * (eLpNorm (dM * dM) 2 S.P_Z).toReal by
simp [t5, eLpNorm_const_smul, Real.norm_eq_abs, ENNReal.toReal_mul]]
have ht1' : (eLpNorm t1 2 S.P_Z).toReal ≤ A4 * rateM n ω := by
simpa [t1, A, A4, hdM_norm] using ht1
have ht2' : (eLpNorm t2 2 S.P_Z).toReal ≤ rateL n ω * V4 := by
simpa [t2, v, V4, hdL_norm] using ht2
have ht3' : (eLpNorm t3 2 S.P_Z).toReal ≤ rateL n ω * rateM n ω := by
simpa [t3, hdL_norm, hdM_norm] using ht3
have ht4' : |S.θ₀| * (eLpNorm (dM * v) 2 S.P_Z).toReal ≤
|S.θ₀| * (rateM n ω * V4) := by
apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
simpa [v, V4, hdM_norm] using ht4base
have ht5' : |S.θ₀| * (eLpNorm (dM * dM) 2 S.P_Z).toReal ≤
|S.θ₀| * (rateM n ω * rateM n ω) := by
apply mul_le_mul_of_nonneg_left _ (abs_nonneg _)
simpa [hdM_norm] using ht5base
exact add_le_add (add_le_add (add_le_add (add_le_add ht1' ht2') ht3') ht4') ht5'
_ ≤ (Cconst + 1) * (rateL n ω + rateM n ω) := by
change rateL n ω ≤ B at hL
change rateM n ω ≤ B at hM
have hLM : rateL n ω * rateM n ω ≤ B * rateL n ω := by
nlinarith [hrateL_nonneg n ω]
have hMM : rateM n ω * rateM n ω ≤ B * rateM n ω := by
nlinarith [hrateM_nonneg n ω]
calc
_ ≤ A4 * rateM n ω + rateL n ω * V4 + B * rateL n ω +
|S.θ₀| * (rateM n ω * V4) + |S.θ₀| * (B * rateM n ω) := by
gcongr
_ ≤ (A4 * rateM n ω + rateL n ω * V4 + B * rateL n ω +
|S.θ₀| * (rateM n ω * V4) + |S.θ₀| * (B * rateM n ω)) +
(A4 * rateL n ω + V4 * rateM n ω + B * rateM n ω +
|S.θ₀| * (V4 * rateL n ω) + |S.θ₀| * (B * rateL n ω) +
rateL n ω + rateM n ω) := by
apply le_add_of_nonneg_right
dsimp [A4, V4]
positivity
_ = (Cconst + 1) * (rateL n ω + rateM n ω) := by
rw [hCconst]
ring