Estimation.OrthogonalMoments.DMLCrossFit
K-fold cross-fitted double machine learning (the DML2 estimator of Chernozhukov et al.
Estimator 3 core · 0 supporting This file defines the K-fold oracle one-step estimator and the feasible one-shot and K-fold estimators for affine scores.
Linear-score DML estimators
This file defines the K-fold oracle one-step estimator and the feasible one-shot and K-fold estimators for affine scores. The feasible estimators solve their cross-fitted empirical moment equations and therefore use only observed samples and fitted nuisances.
def crossFitOneStepOracleDML reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
For a general moment system, an i.i.d. sample, a K-fold split, fold-specific nuisance fits, and a sample-size index, the K-fold oracle one-step DML estimator evaluates every fold's score at the true target and rescales the fold-averaged score by the true supplied linearization scale.
Definition (Lean source)
parameters
H :
Type u_3
M :
GeneralMoment Ω μ Z P_Z H
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
n :
ℕ
def
crossFitOneStepOracleDML M sample split η_hat n :
Ω → ℝ
given by
fun ω
=> M.θ₀
- M.linScaleInv * ((K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m (η_hat n k ω) (sample.Z i ω) M.θ₀)
def feasibleLinearDML reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
For an affine moment system, an i.i.d. sample, a one-shot sample split, a nuisance fit trained on the complementary fold, and a sample-size index, the feasible linear-score DML estimator is minus the inverse empirical coefficient mean times the empirical constant-term mean.
Definition (Lean source)
parameters
H :
Type u_3
M :
LinearMoment Ω μ Z P_Z H
sample :
IIDSample Ω Z μ P_Z
split :
OneShotSplit sample
η_hat :
ℕ → Ω → H
n :
ℕ
def
feasibleLinearDML M sample split η_hat n :
Ω → ℝ
given by
fun ω
=> -((((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω))⁻¹) * (((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_b (η_hat n ω) (sample.Z i ω))
def feasibleCrossFitLinearDML reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
For an affine moment system, an i.i.d. sample, a K-fold split, fold-specific complementary-sample nuisance fits, and a sample-size index, the feasible K-fold DML2 estimator is minus the inverse fold-averaged empirical coefficient times the fold-averaged empirical constant term.
Definition (Lean source)
parameters
H :
Type u_3
M :
LinearMoment Ω μ Z P_Z H
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
n :
ℕ
def
feasibleCrossFitLinearDML M sample split η_hat n :
Ω → ℝ
AsymptoticLinearity 1 core · 3 supporting This file proves the K-fold analogue of the Chernozhukov-form DML theorem. ★ crossFitOneStepOracleDML_isAsymLinear_of_goodSet
Cross-Fitted Double Machine Learning
This file proves the K-fold analogue of the Chernozhukov-form DML theorem.
The estimator crossFitOneStepOracleDML evaluates each fold with a nuisance
learner trained on the complementary data and averages the fold scores. The
main theorem crossFitOneStepOracleDML_isAsymLinear_of_goodSet shows asymptotic linearity with
influence function -linScale⁻¹ · m(η₀, ·, θ₀) under mean-zero,
finite-variance, score-difference, and product-rate hypotheses imposed fold
by fold; crossFitOneStepOracleDML_isAsymLinear_on_highProbEvent is the event form.
theorem crossFitOneStepOracleDML_isAsymLinear_of_goodSet reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
Asymptotic linearity of the oracle K-fold cross-fitted DML estimator on a nuisance good set. Take a moment system with score m, true nuisance η₀, true parameter θ₀, a set 𝒯 of admissible nuisance values, two error gauges ρ₁ and ρ₂, and a nonzero linearization scale J₀ whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, and let η̂_{n,k} be the nuisance fit used on fold k at sample size n. Assume for every η in 𝒯 the population moment of m(η, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η, η₀)·ρ₂(η, η₀); the probability that some fold's fit η̂_{n,k} lies outside 𝒯 is at most Δ_n, where Δ_n is a sequence of bounds that tends to zero; for every n and k the map (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; for every η in 𝒯 the score m(η, ·, θ₀) is integrable and square-integrable under the observation law; for each fold k the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and for each fold k the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). Then the oracle cross-fitted estimator, θ₀ minus J₀⁻¹ times the average over folds of the fold-k sample mean of m(η̂_{n,k}, Z_i, θ₀), is asymptotically linear at θ₀ over the full sample with influence function −J₀⁻¹·m(η₀, z, θ₀).
Formal statement
hypotheses
H :
Type u_3
M :
GeneralMoment Ω μ Z P_Z H
_hMZ :
MeanZero M
_hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
_hK_pos :
1 < K
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
Δ :
ℕ → ℝ≥0∞
Crem :
ℝ
_hBR :
BilinearRemainder M Crem
_hT :
∀ n, μ {ω | ∃ k, η_hat n k ω ∉ M.H_ε} ≤ Δ n
_h_m_meas :
∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)
_h_m_train_uncurry :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)
_h_m_int :
∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z
_h_m_sq_int :
∀ η ∈ M.H_ε, Integrable (fun z => (M.m η z M.θ₀) ^ 2) P_Z
_h_score_diff_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
_h_product_rate :
∀ k,
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
conclusion
IsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)
Proof (Lean source)
theorem crossFitOneStepOracleDML_isAsymLinear_of_goodSet
[StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ]
(M : GeneralMoment Ω μ Z P_Z H)
(_hMZ : MeanZero M)
(_hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z)
(sample : IIDSample Ω Z μ P_Z) {K : ℕ} (_hK_pos : 1 < K)
(split : KFoldSplit sample K)
(η_hat : ℕ → Fin K → Ω → H)
(Δ : ℕ → ℝ≥0∞)
(_hΔ : Tendsto Δ atTop (𝓝 0))
{Crem : ℝ}
(_hBR : BilinearRemainder M Crem)
(_hT : ∀ n, μ {ω | ∃ k, η_hat n k ω ∉ M.H_ε} ≤ Δ n)
(_h_m_meas :
∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀))
(_h_m_train_uncurry :
∀ n k,
Measurable[(comap
(fun ω (i : split.trainComplement n k) => sample.Z i ω)
inferInstance).prod
(inferInstance : MeasurableSpace Z)]
(fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀))
(_h_m_int : ∀ η ∈ M.H_ε,
Integrable (fun z => M.m η z M.θ₀) P_Z)
(_h_m_sq_int : ∀ η ∈ M.H_ε,
Integrable (fun z => (M.m η z M.θ₀) ^ 2) P_Z)
(_h_score_diff_rate :
∀ k, IsLittleOp
(fun n ω =>
(eLpNorm
(fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(_h_product_rate :
∀ k, IsLittleOp
(fun n ω =>
((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) :
IsAsymLinear
(crossFitOneStepOracleDML M sample split η_hat)
M.θ₀
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)
sample
(fun n => range n) := by
classical
apply crossFitOneStepOracleDML_isAsymLinear_on_highProbEvent M _hMZ _hFV sample
_hK_pos split η_hat (fun n => {ω | ∀ k, η_hat n k ω ∈ M.H_ε}) Δ _hΔ
· intro n
calc
μ ({ω | ∀ k, η_hat n k ω ∈ M.H_ε} : Set Ω)ᶜ =
μ {ω | ∃ k, η_hat n k ω ∉ M.H_ε} := by
congr 1
ext ω
simp only [Set.mem_compl_iff, Set.mem_setOf_eq, not_forall]
_ ≤ Δ n := _hT n
· intro n k ω hω
exact _hBR (η_hat n k ω) (hω k)
· exact _h_m_meas
· exact _h_m_train_uncurry
· intro n k ω hω
exact _h_m_int (η_hat n k ω) (hω k)
· intro n k ω hω
exact _h_m_sq_int (η_hat n k ω) (hω k)
· exact _h_score_diff_rate
· exact _h_product_rate
3 supporting declarations (lemmas, instances)
-
crossFitOneStepOracleDML_isAsymLinear_on_highProbEventtheorem — Asymptotic linearity of the oracle K-fold cross-fitted DML estimator, with nuisance conditions on events of probability tending to one. Take a moment system with score m, true nuisance η₀, true parameter θ₀, two error gauges ρ₁ and ρ₂, and a nonzero linearization scale J₀ whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, let η̂_{n,k} be the nuisance fit used on fold k at sample size n, and let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume that for every n, every fold k and every realization in G_n the population moment of m(η̂_{n,k}, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) and m(η̂_{n,k}, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; that for each fold the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that for each fold the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). Then the oracle cross-fitted estimator, θ₀ minus J₀⁻¹ times the average over folds of the fold-k sample mean of m(η̂_{n,k}, Z_i, θ₀), is asymptotically linear at θ₀ over the full sample with influence function −J₀⁻¹·m(η₀, z, θ₀).hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z HhMZ :MeanZero MhFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_ZK :ℕhK_pos :1 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nCrem :ℝhBR_at :h_m_meas :∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_train_uncurry :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Zh_m_sq_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Zh_score_diff_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μh_product_rate :∀ k,IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μconclusionIsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)Proof (Lean source)
theorem crossFitOneStepOracleDML_isAsymLinear_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : GeneralMoment Ω μ Z P_Z H) (hMZ : MeanZero M) (hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) {Crem : ℝ} (hBR_at : ∀ n k ω, ω ∈ goodSet n → |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (h_m_meas : ∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z) (h_m_sq_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z) (h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by classical let ψ₀ : Z → ℝ := fun z => M.m M.η₀ z M.θ₀ have hMZ_int : ∫ z, ψ₀ z ∂P_Z = 0 := hMZ refine ⟨?_, ?_, ?_⟩ · -- Mean zero: multiply `MeanZero M` by the fixed inverse scale. show ∫ z, -M.linScaleInv * M.m M.η₀ z M.θ₀ ∂P_Z = 0 calc ∫ z, -M.linScaleInv * M.m M.η₀ z M.θ₀ ∂P_Z = -M.linScaleInv * ∫ z, ψ₀ z ∂P_Z := by simp only [ψ₀, neg_mul, integral_neg, integral_const_mul] _ = 0 := by rw [hMZ_int]; ring · -- Finite variance: fixed scalar multiplication preserves square -- integrability of the Chernozhukov score. show Integrable (fun z => (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2) P_Z have h_eq : ∀ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 = M.linScaleInv ^ 2 * (M.m M.η₀ z M.θ₀) ^ 2 := by intro z; ring simp_rw [h_eq] exact hFV.const_mul (M.linScaleInv ^ 2) · -- Remainder: separate the K-fold reduction into the -- stochastic fold terms, the population bias terms, and the final -- full-sample reweighting from fold averages. let foldScoreDiff : ℕ → Fin K → Ω → Z → ℝ := fun n k ω z => M.m (η_hat n k ω) z M.θ₀ - ψ₀ z let foldCentered : ℕ → Fin K → Ω → ℝ := fun n k ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, (foldScoreDiff n k ω (sample.Z i ω) - ∫ z, foldScoreDiff n k ω z ∂P_Z) let foldBias : ℕ → Fin K → Ω → ℝ := fun n k ω => sqrt ((split.fold n k).card : ℝ) * ∫ z, foldScoreDiff n k ω z ∂P_Z haveI : IsProbabilityMeasure P_Z := by rw [← sample.law] exact Measure.isProbabilityMeasure_map (sample.meas 0).aemeasurable have htruth_L2 : MemLp (fun z => M.m M.η₀ z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas M.η₀ M.θ₀).aestronglyMeasurable).2 hFV have h_fold_centered : ∀ k, IsLittleOp (fun n ω => foldCentered n k ω) (fun _ => (1 : ℝ)) μ := by intro k let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀ have hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (h_m_meas n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_uncurry_train : ∀ n, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (f n)) := by intro n change Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (h_m_train_uncurry n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (f n ω) 2 P_Z := by intro n ω hω have hsq := h_m_sq_int n k ω hω have hrand_L2 : MemLp (fun z => M.m (η_hat n k ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n k ω) M.θ₀).aestronglyMeasurable).2 hsq simp only [f] exact hrand_L2.sub htruth_L2 have hf_rate_one : IsLittleOp (fun n ω => (eLpNorm (f n ω) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ := by simpa [f] using h_score_diff_rate k simpa [foldCentered, foldScoreDiff, ψ₀, f] using KFoldSplit.fold_centered_sum_isLittleOp_one_of_memLp_on_highProbEvent sample split k f goodSet Δ hΔ hfail hf_meas hf_uncurry_train hf_memLp hf_rate_one have h_fold_bias : ∀ k, IsLittleOp (fun n ω => foldBias n k ω) (fun _ => (1 : ℝ)) μ := by intro k let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀ have hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (h_m_meas n k).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (f n ω) 2 P_Z := by intro n ω hω have hsq := h_m_sq_int n k ω hω have hrand_L2 : MemLp (fun z => M.m (η_hat n k ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n k ω) M.θ₀).aestronglyMeasurable).2 hsq simp only [f] exact hrand_L2.sub htruth_L2 have h_int_eq : ∀ n ω, ω ∈ goodSet n → ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by intro n ω hω have hf_L2 := hf_memLp n ω hω have hm_int := h_m_int n k ω hω have hf_int : Integrable (f n ω) P_Z := hf_L2.integrable (by norm_num : (1 : ENNReal) ≤ 2) have htruth_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z := htruth_L2.integrable (by norm_num : (1 : ENNReal) ≤ 2) have hzero : (∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) = 0 := by simpa [MeanZero] using hMZ calc ∫ z, f n ω z ∂P_Z = ∫ z, (M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) ∂P_Z := by rfl _ = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z := integral_sub hm_int htruth_int _ = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by rw [hzero] ring let mGood : ℕ → Ω → ℝ := fun n ω => if ω ∈ goodSet n then ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z else 0 have h_int_good_rate : IsLittleOp mGood (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ let Kc : ℝ := |Crem| + 1 have hKpos : 0 < Kc := by dsimp [Kc] linarith [abs_nonneg Crem] have htarget := (ENNReal.tendsto_nhds_zero.mp (h_product_rate k (ε / Kc) (div_pos hε hKpos))) δ hδ filter_upwards [htarget, eventually_ge_atTop (1 : ℕ)] with n hn hn_one exact (measure_mono (by intro ω hω change ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) ≤ ‖mGood n ω‖ at hω by_cases hgood : ω ∈ goodSet n · have hbr := hBR_at n k ω hgood rw [show mGood n ω = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z by simp [mGood, hgood]] at hω rw [Real.norm_eq_abs] at hω let prodρ : ℝ := ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ) have hprod_nonneg : 0 ≤ prodρ := by dsimp [prodρ] exact mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _) have hbr0 : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * prodρ := by simpa [prodρ, mul_assoc] using hbr have hle_abs : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ |Crem| * prodρ := hbr0.trans (mul_le_mul_of_nonneg_right (le_abs_self Crem) hprod_nonneg) have hKbound : |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Kc * prodρ := by refine hle_abs.trans ?_ exact mul_le_mul_of_nonneg_right (by dsimp [Kc]; linarith) hprod_nonneg have hthreshold_le_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) ≤ Kc * prodρ := hω.trans hKbound have hdiv_le : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / Kc ≤ prodρ := by rw [div_le_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hthreshold_le_bound have hsmall : (ε / Kc) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) ≤ |prodρ| := by have hdiv_eq : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / Kc = (ε / Kc) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) := by ring rw [← hdiv_eq] simpa [abs_of_nonneg hprod_nonneg] using hdiv_le exact hsmall · have hn_pos : 0 < (n : ℝ) := by exact_mod_cast (lt_of_lt_of_le Nat.zero_lt_one hn_one) have hthreshold_pos : -- … truncated; follow the source link for the rest … -
crossFitOneStepOracleDML_isAsymLinear_of_goodSet_aetheorem — Given the cross-fitted DML setup and uniform deterministic-good-set conditions and the foldwise measurability, integrability, and score and product rates, if every foldwise nuisance fit belongs to the set almost surely at every sample size, then the cross-fitted estimator is asymptotically linear.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_ZK :ℕ_hK_pos :1 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HCrem :ℝ_hBR :BilinearRemainder M Crem_hT :∀ n k, ∀ᵐ ω ∂μ, η_hat n k ω ∈ M.H_ε_h_m_meas :∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)_h_m_train_uncurry :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)_h_m_int :∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z_h_m_sq_int :∀ η ∈ M.H_ε, Integrable (fun z => (M.m η z M.θ₀) ^ 2) P_Z_h_score_diff_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ_h_product_rate :∀ k,IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μconclusionIsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)Proof (Lean source)
theorem crossFitOneStepOracleDML_isAsymLinear_of_goodSet_ae [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : GeneralMoment Ω μ Z P_Z H) (_hMZ : MeanZero M) (_hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (_hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) {Crem : ℝ} (_hBR : BilinearRemainder M Crem) (_hT : ∀ n k, ∀ᵐ ω ∂μ, η_hat n k ω ∈ M.H_ε) (_h_m_meas : ∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_int : ∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z) (_h_m_sq_int : ∀ η ∈ M.H_ε, Integrable (fun z => (M.m η z M.θ₀) ^ 2) P_Z) (_h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (_h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by classical apply crossFitOneStepOracleDML_isAsymLinear_of_goodSet M _hMZ _hFV sample _hK_pos split η_hat (fun _ => 0) tendsto_const_nhds _hBR · intro n have hall : ∀ᵐ ω ∂μ, ∀ k, η_hat n k ω ∈ M.H_ε := by exact Filter.eventually_all.2 fun k => _hT n k have hz : μ {ω | ∃ k, η_hat n k ω ∉ M.H_ε} = 0 := by simpa only [not_forall] using (ae_iff.mp hall) simpa [hz] · exact _h_m_meas · exact _h_m_train_uncurry · exact _h_m_int · exact _h_m_sq_int · exact _h_score_diff_rate · exact _h_product_rate -
crossFitOneStepOracleDML_isAsymLinear_of_everywheretheorem — Everywhere-good cross-fitted DML interface. Under pointwise nuisance regularity and the remaining moment and sampling conditions, joint and uncurried product measurability, and the score and product rates, the cross-fitted estimator is asymptotically linear.hypothesesH :sharedType u_3M :GeneralMoment Ω μ Z P_Z H_hMZ :MeanZero M_hFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_ZK :ℕ_hK_pos :1 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HCrem :ℝ_hBR_at :_h_m_meas :∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)_h_m_train_uncurry :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)_h_m_int :∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z_h_m_sq_int :∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z_h_score_diff_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ_h_product_rate :∀ k,IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μconclusionIsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)Proof (Lean source)
theorem crossFitOneStepOracleDML_isAsymLinear_of_everywhere [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : GeneralMoment Ω μ Z P_Z H) (_hMZ : MeanZero M) (_hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (_hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) {Crem : ℝ} (_hBR_at : ∀ n k ω, |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (_h_m_meas : ∀ n k, Measurable (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun (p : Ω × Z) => M.m (η_hat n k p.1) p.2 M.θ₀)) (_h_m_int : ∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z) (_h_m_sq_int : ∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z) (_h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (_h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) : IsAsymLinear (crossFitOneStepOracleDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by apply crossFitOneStepOracleDML_isAsymLinear_on_highProbEvent M _hMZ _hFV sample _hK_pos split η_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds · simp · exact fun n k ω _ => _hBR_at n k ω · exact _h_m_meas · exact _h_m_train_uncurry · exact fun n k ω _ => _h_m_int n k ω · exact fun n k ω _ => _h_m_sq_int n k ω · exact _h_score_diff_rate · exact _h_product_rate
Feasible 1 core · 7 supporting This file proves the generic one-shot feasible DML theorem for affine scores. ★ feasibleLinearDML_isAsymLinear
Feasible linear-score double machine learning
This file proves the generic one-shot feasible DML theorem for affine scores. It first derives consistency of the empirical score coefficient from the coefficient-level nuisance rates, then transfers the oracle one-step linearization to the estimator that solves the empirical moment equation. It also supplies the normalization by the true asymptotic standard deviation.
The main statements linearDML_jacobianConsistency_on_highProbEvent and
feasibleLinearDML_isAsymLinear_on_highProbEvent impose the bilinear remainder bound and
the integrability conditions only on events of probability tending to one; the
theorems without the suffix are their corollaries for nuisance fits satisfying those
conditions at every realization.
theorem feasibleLinearDML_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
Feasible affine-score DML asymptotic linearity. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share converges to a positive limit, and let η̂_n be the nuisance fit at sample size n. Assume that at every sample size and every realization the population moment of m(η̂_n, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_n, η₀)·ρ₂(η̂_n, η₀) and m(η̂_n, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_n(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the training-fold observations and the σ-algebra on the observation space; that the L² distance between m(η̂_n, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that the product ρ₁(η̂_n, η₀)·ρ₂(η̂_n, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that the increment a(η̂_n, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same training-fold product σ-algebra, square-integrable at every realization, o_p(1) in L², and has a population mean that is o_p(1). Finally assume z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable, the rescaled oracle one-step estimator is almost-everywhere measurable at every sample size, and so is the normalized evaluation-fold sum of −J₀⁻¹·m(η₀, Z_i, θ₀). Then the solution of the evaluation-fold empirical moment equation, minus the evaluation-fold mean of b(η̂_n, ·) divided by the evaluation-fold mean of a(η̂_n, ·), is asymptotically linear at θ₀ along the evaluation fold with influence function −J₀⁻¹·m(η₀, z, θ₀).
Formal statement
hypotheses
H :
Type u_3
M :
LinearMoment Ω μ Z P_Z H
hMZ :
MeanZero M.toGeneralMoment
hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
split :
OneShotSplit sample
c :
ℝ
hc_pos :
0 < c
η_hat :
ℕ → Ω → H
Crem :
ℝ
hBR_at :
h_m_meas :
∀ n, Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)
h_m_foldA_uncurry :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)
h_m_int :
∀ n ω, Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z
h_m_sq_int :
∀ n ω, Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z
h_score_diff_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
h_product_rate :
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
h_a_truth :
MemLp (M.m_a M.η₀) 2 P_Z
hΔa_meas :
∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))
hΔa_uncurry_foldA :
∀ n,
Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))
hΔa_memLp :
∀ n ω, MemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z
hΔa_rate :
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
hΔa_bias_rate :
IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ
hψ_meas :
Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)
hOracle_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μ
hSum_meas :
∀ n,
AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μ
conclusion
IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB
Proof (Lean source)
theorem feasibleLinearDML_isAsymLinear
[StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ]
(M : LinearMoment Ω μ Z P_Z H)
(hMZ : MeanZero M.toGeneralMoment)
(hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z)
(sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample)
{c : ℝ} (hc_pos : 0 < c)
(h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c))
(η_hat : ℕ → Ω → H) {Crem : ℝ}
(hBR_at : ∀ n ω, |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤
Crem * ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ))
(h_m_meas : ∀ n, Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀))
(h_m_foldA_uncurry : ∀ n, Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance]
(fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀))
(h_m_int : ∀ n ω, Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z)
(h_m_sq_int : ∀ n ω, Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z)
(h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm
(fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(h_product_rate : IsLittleOp (fun n ω =>
((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ)
(h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z)
(hΔa_meas : ∀ n, Measurable (uncurry
(fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z)))
(hΔa_uncurry_foldA : ∀ n, Measurable[(comap
(fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance]
(uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z)))
(hΔa_memLp : ∀ n ω, MemLp
(fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z)
(hΔa_rate : IsLittleOp (fun n ω => (eLpNorm
(fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(hΔa_bias_rate : IsLittleOp
(fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z)
(fun _ => (1 : ℝ)) μ)
(hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀))
(hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator
(oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μ)
(hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μ) :
IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by
exact feasibleLinearDML_isAsymLinear_on_highProbEvent M hMZ hFV sample split
hc_pos h_split_rate η_hat (fun _ => univ) (fun _ => 0)
tendsto_const_nhds (by simp) (fun n ω _ => hBR_at n ω) h_m_meas
h_m_foldA_uncurry (fun n ω _ => h_m_int n ω) (fun n ω _ => h_m_sq_int n ω)
h_score_diff_rate h_product_rate h_a_truth
hΔa_meas hΔa_uncurry_foldA (fun n ω _ => hΔa_memLp n ω) hΔa_rate hΔa_bias_rate
hψ_meas hOracle_meas hSum_meas
7 supporting declarations (lemmas, instances)
-
linearDML_jacobianConsistency_on_highProbEventtheorem — Empirical Jacobian consistency for an affine score, with square-integrability on events of probability tending to one. For an affine moment system, an i.i.d. sample, a one-shot split, and a complementary-fold nuisance fit, let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Suppose the true coefficient is square-integrable, the coefficient increment has the joint and uncurried training-fold product measurability used for cross-fitting, at every realization in G_n the increment is square-integrable, its L² norm is o_P(1), and its population mean is o_P(1). Then the evaluation-fold empirical coefficient converges in probability to the population Jacobian.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit sampleη_hat :ℕ → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_uncurry_foldA :∀ n,Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n ωifω ∈ goodSet nthenMemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale)Proof (Lean source)
theorem linearDML_jacobianConsistency_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) (η_hat : ℕ → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale) := by classical haveI : IsProbabilityMeasure P_Z := by rw [← sample.law] exact Measure.isProbabilityMeasure_map (sample.meas 0).aemeasurable let Y : ℕ → Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω) let Y₀ : ℕ → Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a M.η₀ (sample.Z i ω) have hY₀ : Modes.TendstoInProbability (fun _ : ℕ => μ) Y₀ atTop (fun _ _ => M.linScale) := by have h := OneShotSplit.foldB_sampleMean_tendsto_inProb sample split (M.m_a_meas M.η₀) h_a_truth rw [← M.linScale_eq] at h exact h let bias : ℕ → Ω → ℝ := fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z let centered : ℕ → Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, ((M.m_a (η_hat n ω) (sample.Z i ω) - M.m_a M.η₀ (sample.Z i ω)) - bias n ω) have hcentered : IsLittleOp centered (fun _ => (1 : ℝ)) μ := by let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z let G : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ z, f n ω z ∂P_Z) have hG : IsLittleOp G (fun _ => (1 : ℝ)) μ := by simpa [G] using foldB_centered_sum_isLittleOp_one_of_memLp_on_highProbEvent sample split f goodSet Δ hΔ hfail hΔa_meas hΔa_uncurry_foldA hΔa_memLp hΔa_rate have hGbig : IsBigOp G (fun _ => (1 : ℝ)) μ := Modes.TendstoInProbability.isBigOp_one (tendstoInProb_zero_of_isLittleOp_one hG) have hinv : Tendsto (fun n => (sqrt ((split.foldB n).card : ℝ))⁻¹) atTop (𝓝 0) := (Real.tendsto_sqrt_atTop.comp (tendsto_natCast_atTop_atTop.comp split.foldB_card_tendsto)).inv_tendsto_atTop have hprod := IsBigOp.const_mul_tendsto_zero hGbig hinv convert hprod using 1 funext n ω simp only [centered, G, f, bias] rw [← mul_assoc] have hsqrt : ((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 hz | hp · simp [hz] · rw [Real.mul_self_sqrt (by positivity)] rw [hsqrt] let biasEff : ℕ → Ω → ℝ := fun n ω => (((split.foldB n).card : ℝ)⁻¹ * (split.foldB n).card) * bias n ω have hbiasEff : IsLittleOp biasEff (fun _ => (1 : ℝ)) μ := by refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hΔa_bias_rate ?_ intro n ω rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hp · simp [biasEff, hz] · have hne : ((split.foldB n).card : ℝ) ≠ 0 := by positivity simp only [biasEff] rw [inv_mul_cancel₀ hne, one_mul] simpa [bias] have hdiff : (fun n ω => Y n ω - Y₀ n ω) = fun n ω => centered n ω + biasEff n ω := by funext n ω rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hp · simp [Y, Y₀, centered, biasEff, bias, Finset.card_eq_zero.mp hz] · have hne : ((split.foldB n).card : ℝ) ≠ 0 := by positivity simp only [Y, Y₀, centered, biasEff, bias] rw [Finset.sum_sub_distrib, Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul, mul_sub, ← mul_assoc, inv_mul_cancel₀ hne, one_mul] ring have hYsub : IsLittleOp (fun n ω => Y n ω - Y₀ n ω) (fun _ => (1 : ℝ)) μ := by rw [hdiff] exact IsLittleOp.add_one hcentered hbiasEff have hYsubJ : IsLittleOp (fun n ω => Y n ω - M.linScale) (fun _ => (1 : ℝ)) μ := by convert IsLittleOp.add_one hYsub (Modes.TendstoInProbability.isLittleOp_one (Modes.TendstoInProbability.sub_const hY₀)) using 1 funext n ω ring have hzero := tendstoInProb_zero_of_isLittleOp_one hYsubJ have hadd := Modes.TendstoInProbability.comp_continuousAt (h := hzero) (g := fun x : ℝ => x + M.linScale) (continuous_add_const M.linScale).continuousAt simpa [Y] using hadd -
linearDML_jacobianConsistencytheorem — Empirical Jacobian consistency for an affine score. For an affine moment system, an i.i.d. sample, a one-shot split, and a complementary-fold nuisance fit, suppose the true coefficient is square-integrable, the coefficient increment has the joint and uncurried training-fold product measurability used for cross-fitting, each increment is square-integrable, its L² norm is o_P(1), and its population mean is o_P(1). Then the evaluation-fold empirical coefficient converges in probability to the population Jacobian.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit sampleη_hat :ℕ → Ω → Hh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_uncurry_foldA :∀ n,Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n ω, MemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μconclusionModes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale)Proof (Lean source)
theorem linearDML_jacobianConsistency [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) (η_hat : ℕ → Ω → H) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n ω, MemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale) := by exact linearDML_jacobianConsistency_on_highProbEvent M sample split η_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp) h_a_truth hΔa_meas hΔa_uncurry_foldA (fun n ω _ => hΔa_memLp n ω) hΔa_rate hΔa_bias_rate -
feasibleLinearDML_isAsymLinear_of_jacobianConsistencytheorem — Feasible affine-score DML asymptotic linearity, conditional bridge. If the corresponding oracle one-step estimator is asymptotically linear, the empirical coefficient converges to the nonzero population Jacobian, and the influence function, oracle rescaling, and normalized influence sum are measurable, then the solved feasible estimator has the same asymptotic linear expansion.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit sampleη_hat :ℕ → Ω → HhOracle :IsAsymLinear (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBhJ :Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale)hψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)hOracle_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μhSum_meas :∀ n,AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μconclusionIsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem feasibleLinearDML_isAsymLinear_of_jacobianConsistency [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) (η_hat : ℕ → Ω → H) (hOracle : IsAsymLinear (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB) (hJ : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale)) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μ) : IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by let A : ℕ → Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_a (η_hat n ω) (sample.Z i ω) let Sψ : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, M.m (η_hat n ω) (sample.Z i ω) M.θ₀ let X : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB let Y : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB let F : ℕ → Ω → ℝ := fun n ω => M.linScaleInv - (A n ω)⁻¹ have hSψ_eq : Sψ = fun n ω => (-M.linScale) * X n ω := by funext n ω simp only [Sψ, X, IsAsymLinear.rescaledEstimator, oneStepOracleDML, GeneralMoment.linScaleInv] rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hp · simp [Finset.card_eq_zero.mp hz] · have hc : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hp have hs : sqrt ((split.foldB n).card : ℝ) ≠ 0 := by positivity have hj := M.linScale_ne_zero field_simp rw [Real.sq_sqrt (le_of_lt hc)] ring have hXdist := hOracle.tendsto_normal_foldB split hψ_meas hOracle_meas hSum_meas have hSψ_big : IsBigOp Sψ (fun _ => (1 : ℝ)) μ := by rw [hSψ_eq] exact const_mul (-M.linScale) (Modes.TendstoInLaw.tightness hXdist) have hFinProb : Modes.TendstoInProbability (fun _ : ℕ => μ) F atTop (fun _ _ => 0) := by have hi := Modes.TendstoInProbability.inv hJ M.linScale_ne_zero have hs := Modes.TendstoInProbability.sub_const hi have hn := Modes.TendstoInProbability.comp_continuousAt (h := hs) (g := fun x : ℝ => -x) continuous_neg.continuousAt simpa [F, A, GeneralMoment.linScaleInv, one_div] using hn have hprod : IsLittleOp (fun n ω => Sψ n ω * F n ω) (fun _ => (1 : ℝ)) μ := hSψ_big.mul_isLittleOp_one_isLittleOp (Modes.TendstoInProbability.isLittleOp_one hFinProb) have heq : ∀ n ω, A n ω ≠ 0 → Y n ω - X n ω = Sψ n ω * F n ω := by intro n ω hA have hp : 0 < (split.foldB n).card := by rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hp · exact False.elim (hA (by simp [A, Finset.card_eq_zero.mp hz])) · exact hp have hc : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hp have hs : sqrt ((split.foldB n).card : ℝ) ≠ 0 := by positivity let B : ℝ := ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m_b (η_hat n ω) (sample.Z i ω) have hscore : ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m (η_hat n ω) (sample.Z i ω) M.θ₀ = A n ω * M.θ₀ + B := by simp only [A, B, M.m_decomp] rw [Finset.sum_add_distrib, ← Finset.sum_mul, mul_add] ring have hsumscore : (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, M.m (η_hat n ω) (sample.Z i ω) M.θ₀ = sqrt ((split.foldB n).card : ℝ) * (A n ω * M.θ₀ + B) := by have hinv : (sqrt ((split.foldB n).card : ℝ))⁻¹ = sqrt ((split.foldB n).card : ℝ) * ((split.foldB n).card : ℝ)⁻¹ := by field_simp rw [Real.sq_sqrt (le_of_lt hc)] rw [hinv, mul_assoc, hscore] have hfeas : feasibleLinearDML M sample split η_hat n ω = -(A n ω)⁻¹ * B := rfl simp only [Y, X, IsAsymLinear.rescaledEstimator, hfeas, oneStepOracleDML, Sψ, F] rw [show (((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, M.m (η_hat n ω) (sample.Z i ω) M.θ₀) = A n ω * M.θ₀ + B from hscore, hsumscore] field_simp [hA] ring have hbad : Tendsto (fun n => μ {ω | Y n ω - X n ω ≠ Sψ n ω * F n ω}) atTop (𝓝 0) := by have hsub : ∀ n, {ω | Y n ω - X n ω ≠ Sψ n ω * F n ω} ⊆ {ω | |M.linScale| ≤ |A n ω - M.linScale|} := by intro n ω hw simp only [Set.mem_setOf_eq] at hw ⊢ by_contra hlt push_neg at hlt have hne : A n ω ≠ 0 := by intro hz rw [hz, zero_sub, abs_neg] at hlt exact (lt_irrefl _ hlt) exact hw (heq n ω hne) have hjp : 0 < |M.linScale| := abs_pos.mpr M.linScale_ne_zero have ht := hJ rw [Tendsto_inProb_iff] at ht rw [tendstoInMeasure_iff_norm] at ht have htail := ht |M.linScale| hjp refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htail (fun _ => zero_le) ?_ intro n exact measure_mono (hsub n) have hYX : IsLittleOp (fun n ω => Y n ω - X n ω) (fun _ => (1 : ℝ)) μ := IsLittleOp.of_eq_on_asymptotic hbad hprod refine ⟨hOracle.mean_zero, hOracle.finite_var, ?_⟩ have hsum := IsLittleOp.add_one hYX hOracle.remainder convert hsum using 1 funext n ω simp only [Y, X, IsAsymLinear.rescaledEstimator] ring -
feasibleLinearDML_isAsymLinear_on_highProbEventtheorem — Feasible affine-score DML asymptotic linearity, with nuisance conditions on events of probability tending to one. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split once into a training fold and an evaluation fold whose evaluation-fold share converges to a positive limit, let η̂_n be the nuisance fit at sample size n, and let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume that at every sample size and every realization in G_n the population moment of m(η̂_n, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_n, η₀)·ρ₂(η̂_n, η₀) and m(η̂_n, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_n(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the training-fold observations and the σ-algebra on the observation space; that the L² distance between m(η̂_n, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that the product ρ₁(η̂_n, η₀)·ρ₂(η̂_n, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that the increment a(η̂_n, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same training-fold product σ-algebra, square-integrable at every realization in G_n, o_p(1) in L², and has a population mean that is o_p(1). Finally assume z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable, the rescaled oracle one-step estimator is almost-everywhere measurable at every sample size, and so is the normalized evaluation-fold sum of −J₀⁻¹·m(η₀, Z_i, θ₀). Then the solution of the evaluation-fold empirical moment equation, minus the evaluation-fold mean of b(η̂_n, ·) divided by the evaluation-fold mean of a(η̂_n, ·), is asymptotically linear at θ₀ along the evaluation fold with influence function −J₀⁻¹·m(η₀, z, θ₀).hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z HhMZ :MeanZero M.toGeneralMomenthFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit samplec :ℝhc_pos :0 < cη_hat :ℕ → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nCrem :ℝhBR_at :h_m_meas :∀ n, Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)h_m_foldA_uncurry :∀ n,Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)h_m_int :∀ n ωifω ∈ goodSet nthenIntegrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Zh_m_sq_int :∀ n ωifω ∈ goodSet nthenIntegrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Zh_score_diff_rate :IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μh_product_rate :IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_uncurry_foldA :∀ n,Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n ωifω ∈ goodSet nthenMemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μhψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)hOracle_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μhSum_meas :∀ n,AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μconclusionIsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBProof (Lean source)
theorem feasibleLinearDML_isAsymLinear_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (hMZ : MeanZero M.toGeneralMoment) (hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) {Crem : ℝ} (hBR_at : ∀ n ω, ω ∈ goodSet n → |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (h_m_meas : ∀ n, Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀)) (h_m_int : ∀ n ω, ω ∈ goodSet n → Integrable (fun z => M.m (η_hat n ω) z M.θ₀) P_Z) (h_m_sq_int : ∀ n ω, ω ∈ goodSet n → Integrable (fun z => (M.m (η_hat n ω) z M.θ₀) ^ 2) P_Z) (h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (h_product_rate : IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n, Measurable (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod inferInstance] (uncurry (fun ω z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n ω, ω ∈ goodSet n → MemLp (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (oneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ split.foldB n) μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μ) : IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB := by have hOracle := oneStepOracleDML_isAsymLinear_on_highProbEvent M.toGeneralMoment hMZ hFV sample split hc_pos h_split_rate η_hat goodSet Δ hΔ hfail hBR_at h_m_meas h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate have hJ := linearDML_jacobianConsistency_on_highProbEvent M sample split η_hat goodSet Δ hΔ hfail h_a_truth hΔa_meas hΔa_uncurry_foldA hΔa_memLp hΔa_rate hΔa_bias_rate exact feasibleLinearDML_isAsymLinear_of_jacobianConsistency M sample split η_hat hOracle hJ hψ_meas hOracle_meas hSum_meas -
feasibleLinearDML_tendstoStandardNormal_of_isAsymLineartheorem — True-σ standardized feasible DML limit. If the feasible affine-score estimator is asymptotically linear with the reference influence function, that influence function is measurable, its true standard deviation σ is positive and has the defining squared-value identity, and the numerator, its empirical sum, and standardized statistic are measurable, then the true-σ standardized feasible estimator converges to the standard normal law.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_Zsplit :OneShotSplit sampleη_hat :ℕ → Ω → HhAL :IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldBhψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)σ :ℝhσ_pos :0 < σhσ_sq :σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_ZhNum_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n) μhSum_meas :∀ n,AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μhStud_meas :∀ n,AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n ω / σ) μconclusionModes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n ω / σ) atTop (gaussianMeasure 0 1)Proof (Lean source)
theorem feasibleLinearDML_tendstoStandardNormal_of_isAsymLinear [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) (η_hat : ℕ → Ω → H) (hAL : IsAsymLinear (feasibleLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample split.foldB) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (σ : ℝ) (hσ_pos : 0 < σ) (hσ_sq : σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_Z) (hNum_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n) μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) split.foldB n) μ) (hStud_meas : ∀ n, AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n ω / σ) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB n ω / σ) atTop (gaussianMeasure 0 1) := by have hN := hAL.tendsto_normal_foldB split hψ_meas hNum_meas hSum_meas rw [← hσ_sq] at hN have hscaled := Modes.TendstoInLaw.const_mul_tendsto_gaussian (Xn := IsAsymLinear.rescaledEstimator (feasibleLinearDML M sample split η_hat) M.θ₀ split.foldB) (a := fun _ : ℕ => 1 / σ) (a₀ := 1 / σ) (v := σ ^ 2) hN tendsto_const_nhds have hvar : (1 / σ) ^ 2 * σ ^ 2 = 1 := by field_simp [ne_of_gt hσ_pos] rw [hvar] at hscaled simpa [div_eq_mul_inv, mul_comm] using hscaled -
feasibleCrossFitLinearDML_isAsymLinear_of_jacobianConsistencytheorem — K-fold feasible affine-score DML transfer. Given an affine moment system, an i.i.d. sample and K-fold split, and fold-specific complementary-sample nuisance fits, if the K-fold oracle one-step object is asymptotically linear, the fold-averaged empirical coefficient converges to the population Jacobian, and the influence function and oracle rescaling are measurable, then the feasible DML2 empirical-moment solution has the same full-sample asymptotic linear expansion.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_ZK :ℕsplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HhOracle :IsAsymLinear (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)hJ :hψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)hOracle_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μconclusionIsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)Proof (Lean source)
theorem feasibleCrossFitLinearDML_isAsymLinear_of_jacobianConsistency [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (hOracle : IsAsymLinear (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)) (hJ : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale)) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μ) : IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by let A : ℕ → Ω → ℝ := fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω) let B : ℕ → Ω → ℝ := fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_b (η_hat n k ω) (sample.Z i ω) let Q : ℕ → Ω → ℝ := fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m (η_hat n k ω) (sample.Z i ω) M.θ₀ let Sψ : ℕ → Ω → ℝ := fun n ω => sqrt (n : ℝ) * Q n ω let X : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) let Y : ℕ → Ω → ℝ := IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) let F : ℕ → Ω → ℝ := fun n ω => M.linScaleInv - (A n ω)⁻¹ have hSψ_eq : Sψ = fun n ω => (-M.linScale) * X n ω := by funext n ω simp only [Sψ, Q, X, IsAsymLinear.rescaledEstimator, crossFitOneStepOracleDML, Finset.card_range, GeneralMoment.linScaleInv] field_simp [M.linScale_ne_zero] ring have hXdist := hOracle.tendsto_normal hψ_meas hOracle_meas have hSψ_big : IsBigOp Sψ (fun _ => (1 : ℝ)) μ := by rw [hSψ_eq] exact const_mul (-M.linScale) (Modes.TendstoInLaw.tightness hXdist) have hFinProb : Modes.TendstoInProbability (fun _ : ℕ => μ) F atTop (fun _ _ => 0) := by have hi := Modes.TendstoInProbability.inv hJ M.linScale_ne_zero have hn := Modes.TendstoInProbability.comp_continuousAt (h := Modes.TendstoInProbability.sub_const hi) (g := fun x : ℝ => -x) continuous_neg.continuousAt simpa [F, A, GeneralMoment.linScaleInv, one_div] using hn have hprod : IsLittleOp (fun n ω => Sψ n ω * F n ω) (fun _ => (1 : ℝ)) μ := hSψ_big.mul_isLittleOp_one_isLittleOp (Modes.TendstoInProbability.isLittleOp_one hFinProb) have hQ : ∀ n ω, Q n ω = A n ω * M.θ₀ + B n ω := by intro n ω simp only [Q, A, B, M.m_decomp] simp_rw [Finset.sum_add_distrib, ← Finset.sum_mul, mul_add] rw [Finset.sum_add_distrib] have hfold : ∀ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ((∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω)) * M.θ₀) = (((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω)) * M.θ₀ := by intro k ring simp_rw [hfold, ← Finset.sum_mul] ring have heq : ∀ n ω, A n ω ≠ 0 → Y n ω - X n ω = Sψ n ω * F n ω := by intro n ω hA have hfeas : feasibleCrossFitLinearDML M sample split η_hat n ω = -(A n ω)⁻¹ * B n ω := rfl simp only [Y, X, IsAsymLinear.rescaledEstimator, Finset.card_range, hfeas, crossFitOneStepOracleDML, Sψ, F, Q] rw [show ((K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m (η_hat n k ω) (sample.Z i ω) M.θ₀) = A n ω * M.θ₀ + B n ω from hQ n ω] field_simp [hA] ring have hbad : Tendsto (fun n => μ {ω | Y n ω - X n ω ≠ Sψ n ω * F n ω}) atTop (𝓝 0) := by have hsub : ∀ n, {ω | Y n ω - X n ω ≠ Sψ n ω * F n ω} ⊆ {ω | |M.linScale| ≤ |A n ω - M.linScale|} := by intro n ω hw simp only [Set.mem_setOf_eq] at hw ⊢ by_contra hlt push_neg at hlt have hne : A n ω ≠ 0 := by intro hz rw [hz, zero_sub, abs_neg] at hlt exact lt_irrefl _ hlt exact hw (heq n ω hne) have ht := hJ rw [Tendsto_inProb_iff] at ht rw [tendstoInMeasure_iff_norm] at ht have htail := ht |M.linScale| (abs_pos.mpr M.linScale_ne_zero) refine tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds htail (fun _ => zero_le) ?_ intro n exact measure_mono (hsub n) have hYX : IsLittleOp (fun n ω => Y n ω - X n ω) (fun _ => (1 : ℝ)) μ := IsLittleOp.of_eq_on_asymptotic hbad hprod refine ⟨hOracle.mean_zero, hOracle.finite_var, ?_⟩ convert IsLittleOp.add_one hYX hOracle.remainder using 1 funext n ω simp only [Y, X, IsAsymLinear.rescaledEstimator] ring -
feasibleCrossFitLinearDML_tendstoStandardNormal_of_isAsymLineartheorem — True-σ standardized K-fold feasible DML limit. For an affine moment system, i.i.d. sample, K-fold split, and fold-specific nuisance fits, if the feasible DML2 estimator has the reference asymptotic linear expansion, its influence function is measurable, the true standard deviation σ is positive and its square equals the influence-function second moment, and the numerator and standardized statistic are measurable, then the true-σ standardized full-sample statistic converges to the standard normal law.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_ZK :ℕsplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HhAL :IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)hψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)σ :ℝhσ_pos :0 < σhσ_sq :σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_ZhNum_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n) μhStud_meas :∀ n,AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) μconclusionModes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1)Proof (Lean source)
theorem feasibleCrossFitLinearDML_tendstoStandardNormal_of_isAsymLinear [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (hAL : IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (σ : ℝ) (hσ_pos : 0 < σ) (hσ_sq : σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_Z) (hNum_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n) μ) (hStud_meas : ∀ n, AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1) := by have hN := hAL.tendsto_normal hψ_meas hNum_meas rw [← hσ_sq] at hN have hscaled := Modes.TendstoInLaw.const_mul_tendsto_gaussian (Xn := IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n)) (a := fun _ : ℕ => 1 / σ) (a₀ := 1 / σ) (v := σ ^ 2) hN tendsto_const_nhds have hvar : (1 / σ) ^ 2 * σ ^ 2 = 1 := by field_simp [ne_of_gt hσ_pos] rw [hvar] at hscaled simpa [div_eq_mul_inv, mul_comm] using hscaled
Helpers 1 core · 6 supporting This helper module proves fold-normalized sum bounds and closure properties for stochastic little-o and big-O relations used in the K-fold asymptotic-linearity proof. ★ deterministic_tendsto_isBigOp
Cross-Fitted Double Machine Learning
This helper module proves fold-normalized sum bounds and closure properties for stochastic
little-o and big-O relations used in the K-fold asymptotic-linearity proof. The estimator-level
assembly and headline theorem are in AsymptoticLinearity.lean.
lemma deterministic_tendsto_isBigOp reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
For a finite-measure population space, a deterministic real sequence and its proposed limit, if the sequence converges to that limit, then viewing the sequence as constant random variables makes it bounded in probability.
Formal statement
hypotheses
conclusion
IsBigOp (fun n (_ : Ω) => a n) (fun _ => (1 : ℝ)) μ
Proof (Lean source)
lemma deterministic_tendsto_isBigOp
{Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ]
{a : ℕ → ℝ} {c : ℝ} (ha : Tendsto a atTop (𝓝 c)) :
IsBigOp (fun n (_ : Ω) => a n) (fun _ => (1 : ℝ)) μ := by
intro ε hε
refine ⟨|c| + 2, by positivity, ?_⟩
have hbound : ∀ᶠ n in atTop, |a n| ≤ |c| + 1 := by
have hdist := (Metric.tendsto_nhds.mp ha) (1 : ℝ) zero_lt_one
filter_upwards [hdist] with n hn
have habs_sub : |a n - c| < 1 := by
simpa [Real.dist_eq] using hn
calc
|a n| = |(a n - c) + c| := by ring_nf
_ ≤ |a n - c| + |c| := abs_add_le (a n - c) c
_ ≤ |c| + 1 := by linarith
filter_upwards [hbound] with n hn
have hempty :
{ω : Ω | (|c| + 2) * (fun _ => (1 : ℝ)) n ≤ ‖a n‖} = ∅ := by
ext ω
simp only [Set.mem_setOf_eq, mul_one, Real.norm_eq_abs,
Set.mem_empty_iff_false, iff_false]
linarith
rw [hempty]
simp
6 supporting declarations (lemmas, instances)
-
foldNormalizedSum_isBigOplemma — Foldwise normalized-sum tightness. For an i.i.d. sample, a measurable mean-zero square-integrable transform, a K-fold split, and a fixed fold, the transform's fold-normalized partial sum is bounded in probability.hypothesessample :IIDSample Ω Z μ P_Zψ :Z → ℝhψ_meas :hψ_mean :∫ z, ψ z ∂P_Z = 0hψ_sq :Integrable (fun z => ψ z ^ 2) P_ZK :ℕsplit :KFoldSplit sample Kk :Fin KProof (Lean source)
lemma foldNormalizedSum_isBigOp [IsProbabilityMeasure μ] [IsProbabilityMeasure P_Z] (sample : IIDSample Ω Z μ P_Z) (ψ : Z → ℝ) (hψ_meas : Measurable ψ) (hψ_mean : ∫ z, ψ z ∂P_Z = 0) (hψ_sq : Integrable (fun z => ψ z ^ 2) P_Z) {K : ℕ} (split : KFoldSplit sample K) (k : Fin K) : IsBigOp (fun n ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) (fun _ => (1 : ℝ)) μ := by have hψ_memLp : MemLp ψ 2 P_Z := (memLp_two_iff_integrable_sq hψ_meas.aestronglyMeasurable).2 hψ_sq -- `N²` is the square of the L² norm of ψ. let N : ℝ := (eLpNorm ψ 2 P_Z).toReal have hN_nonneg : 0 ≤ N := ENNReal.toReal_nonneg -- iid product law for fold n k. have hiid : ∀ n, μ.map (fun ω (i : split.fold n k) => sample.Z i ω) = Measure.pi (fun _ : split.fold n k => P_Z) := by intro n have hindep_s : iIndepFun (fun i : split.fold n k => sample.Z i) μ := by exact sample.indep.precomp val_injective have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : split.fold n k => (sample.meas i).aemeasurable)).mp hindep_s calc μ.map (fun ω (i : split.fold n k) => sample.Z i ω) = Measure.pi (fun i : split.fold n k => μ.map (sample.Z i)) := hmap _ = Measure.pi (fun _ : split.fold n k => P_Z) := by congr with i rw [← (sample.identDist i).map_eq, sample.law] -- Independence with the trivial σ-algebra ⊥. have hindep : ∀ n, Indep (⊥ : MeasurableSpace Ω) (comap (fun ω (i : split.fold n k) => sample.Z i ω) inferInstance) μ := by intro n exact ProbabilityTheory.indep_bot_left _ -- Apply the iid centered sum bound with g(ω, x) := ψ(x) (constant in ω). have hbound : ∀ n, 0 < (split.fold n k).card → ∫⁻ ω, ofReal (((sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ ≤ ofReal (N ^ 2) := by intro n hn have hraw := iid_centered_sum_sq_lintegral_le (s := split.fold n k) hn (W := sample.Z) (fun i _ => sample.meas i) (⊥ : MeasurableSpace Ω) bot_le (hindep n) (hiid n) (fun _ z => ψ z) (by change Measurable[(⊥ : MeasurableSpace Ω).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => ψ p.2) exact hψ_meas.comp measurable_snd) (fun _ => hψ_memLp) -- Simplify the lambda `fun _ z => ψ z` to ψ in hraw. simp only [hψ_mean, sub_zero] at hraw -- RHS: ∫ N² ∂μ = N² (μ is probability). refine hraw.trans ?_ simp [N] have hbound_all : ∀ n : ℕ, ∫⁻ ω, ofReal (((sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ ≤ ofReal (N ^ 2 + 1) := by intro n rcases Nat.eq_zero_or_pos ((split.fold n k).card) with hzero | hpos · have hfold_empty : split.fold n k = ∅ := Finset.card_eq_zero.mp hzero simp [hfold_empty] · exact (hbound n hpos).trans (ENNReal.ofReal_le_ofReal (by linarith)) have hY_aemeas : ∀ n : ℕ, AEMeasurable (fun ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) μ := by intro n exact (measurable_const.mul (Finset.measurable_sum _ (fun i _ => hψ_meas.comp (sample.meas i)))).aemeasurable have hbig : IsBigOp (fun n ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) (fun _ => sqrt (N ^ 2 + 1)) μ := IsBigOp.of_sq_lintegral_le hY_aemeas (fun _ => by positivity) (Eventually.of_forall fun _ => by positivity) hbound_all exact hbig.const_rate_collapse (Real.sqrt_nonneg _) -
foldNormalizedSumOverN_isBigOplemma — Helper. Variant of foldNormalizedSum_isBigOp with the full-sample normalization (1/√n) instead of (1/√|fold n k|). Since (split.fold n k).card ≤ n (from cover + partition), the second moment is still bounded by ∫ ψ² dP_Z, and the same Markov argument applies.hypothesessample :IIDSample Ω Z μ P_Zψ :Z → ℝhψ_meas :hψ_mean :∫ z, ψ z ∂P_Z = 0hψ_sq :Integrable (fun z => ψ z ^ 2) P_ZK :ℕsplit :KFoldSplit sample Kk :Fin KProof (Lean source)
lemma foldNormalizedSumOverN_isBigOp [IsProbabilityMeasure μ] [IsProbabilityMeasure P_Z] (sample : IIDSample Ω Z μ P_Z) (ψ : Z → ℝ) (hψ_meas : Measurable ψ) (hψ_mean : ∫ z, ψ z ∂P_Z = 0) (hψ_sq : Integrable (fun z => ψ z ^ 2) P_Z) {K : ℕ} (split : KFoldSplit sample K) (k : Fin K) : IsBigOp (fun n ω => (sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) (fun _ => (1 : ℝ)) μ := by have hψ_memLp : MemLp ψ 2 P_Z := (memLp_two_iff_integrable_sq hψ_meas.aestronglyMeasurable).2 hψ_sq let N : ℝ := (eLpNorm ψ 2 P_Z).toReal have hN_nonneg : 0 ≤ N := ENNReal.toReal_nonneg -- iid product law for fold n k. have hiid : ∀ n, μ.map (fun ω (i : split.fold n k) => sample.Z i ω) = Measure.pi (fun _ : split.fold n k => P_Z) := by intro n have hindep_s : iIndepFun (fun i : split.fold n k => sample.Z i) μ := by exact sample.indep.precomp val_injective have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : split.fold n k => (sample.meas i).aemeasurable)).mp hindep_s calc μ.map (fun ω (i : split.fold n k) => sample.Z i ω) = Measure.pi (fun i : split.fold n k => μ.map (sample.Z i)) := hmap _ = Measure.pi (fun _ : split.fold n k => P_Z) := by congr with i rw [← (sample.identDist i).map_eq, sample.law] have hindep : ∀ n, Indep (⊥ : MeasurableSpace Ω) (comap (fun ω (i : split.fold n k) => sample.Z i ω) inferInstance) μ := by intro n exact ProbabilityTheory.indep_bot_left _ -- |fold n k| ≤ n via cover. have hfold_le_n : ∀ n, (split.fold n k).card ≤ n := by intro n have h_cov := split.cover n have hsub : split.fold n k ⊆ range n := by have : split.fold n k ⊆ (Finset.univ : Finset (Fin K)).biUnion (split.fold n) := Finset.subset_biUnion_of_mem _ (Finset.mem_univ k) rw [h_cov] at this exact this calc (split.fold n k).card ≤ (range n).card := Finset.card_le_card hsub _ = n := Finset.card_range n -- Second-moment bound. have hbound : ∀ n, 0 < (split.fold n k).card → ∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ ≤ ofReal (N ^ 2) := by intro n hn_fold have hraw := iid_centered_sum_sq_lintegral_le (s := split.fold n k) hn_fold (W := sample.Z) (fun i _ => sample.meas i) (⊥ : MeasurableSpace Ω) bot_le (hindep n) (hiid n) (fun _ z => ψ z) (by change Measurable[(⊥ : MeasurableSpace Ω).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => ψ p.2) exact hψ_meas.comp measurable_snd) (fun _ => hψ_memLp) simp only [hψ_mean, sub_zero] at hraw -- The original bound is on (1/√|fold|) Σ. We want (1/√n) Σ. Since |fold|/n ≤ 1, -- (1/√n)² Σ² ≤ (1/√|fold|)² Σ² (because (1/n) ≤ (1/|fold|)). have hn_pos : 0 < n := lt_of_lt_of_le hn_fold (hfold_le_n n) have hn_R : 0 < (n : ℝ) := by exact_mod_cast hn_pos have hfold_R : 0 < ((split.fold n k).card : ℝ) := by exact_mod_cast hn_fold have hfold_le_n_R : ((split.fold n k).card : ℝ) ≤ (n : ℝ) := by exact_mod_cast hfold_le_n n have hinv_le : (n : ℝ)⁻¹ ≤ ((split.fold n k).card : ℝ)⁻¹ := by rw [inv_le_inv₀ hn_R hfold_R] exact hfold_le_n_R -- Pointwise: (1/√n)² ≤ (1/√|fold|)². have hpoint : ∀ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ≤ ofReal (((sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) := by intro ω apply ENNReal.ofReal_le_ofReal set S := ∑ i ∈ split.fold n k, ψ (sample.Z i ω) have h_sqr_n : (sqrt (n : ℝ))⁻¹ ^ 2 = (n : ℝ)⁻¹ := by rw [inv_pow, Real.sq_sqrt hn_R.le] have h_sqr_fold : (sqrt ((split.fold n k).card : ℝ))⁻¹ ^ 2 = ((split.fold n k).card : ℝ)⁻¹ := by rw [inv_pow, Real.sq_sqrt hfold_R.le] have hL : ((sqrt (n : ℝ))⁻¹ * S) ^ 2 = (n : ℝ)⁻¹ * S ^ 2 := by rw [mul_pow, h_sqr_n] have hR : ((sqrt ((split.fold n k).card : ℝ))⁻¹ * S) ^ 2 = ((split.fold n k).card : ℝ)⁻¹ * S ^ 2 := by rw [mul_pow, h_sqr_fold] rw [hL, hR] exact mul_le_mul_of_nonneg_right hinv_le (sq_nonneg _) have hint_le : ∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ ≤ ∫⁻ ω, ofReal (((sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ := lintegral_mono hpoint refine hint_le.trans ?_ refine hraw.trans ?_ simp [N] have hbound_all : ∀ n : ℕ, ∫⁻ ω, ofReal (((sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) ^ 2) ∂μ ≤ ofReal (N ^ 2 + 1) := by intro n rcases Nat.eq_zero_or_pos ((split.fold n k).card) with hzero | hpos · have hfold_empty : split.fold n k = ∅ := Finset.card_eq_zero.mp hzero simp [hfold_empty] · exact (hbound n hpos).trans (ENNReal.ofReal_le_ofReal (by linarith)) have hY_aemeas : ∀ n : ℕ, AEMeasurable (fun ω => (sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) μ := by intro n exact (measurable_const.mul (Finset.measurable_sum _ (fun i _ => hψ_meas.comp (sample.meas i)))).aemeasurable have hbig : IsBigOp (fun n ω => (sqrt (n : ℝ))⁻¹ * ∑ i ∈ split.fold n k, ψ (sample.Z i ω)) (fun _ => sqrt (N ^ 2 + 1)) μ := IsBigOp.of_sq_lintegral_le hY_aemeas (fun _ => by positivity) (Eventually.of_forall fun _ => by positivity) hbound_all exact hbig.const_rate_collapse (Real.sqrt_nonneg _) -
IsLittleOp_congr_eventuallylemma — Given two random sequences, a deterministic rate, and a measure, if the first sequence is little-o in probability at that rate and the sequences are pointwise equal for all sufficiently large indices, then the second has the same little-o property.hypothesesconclusionIsLittleOp Y r μProof (Lean source)
lemma IsLittleOp_congr_eventually {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X Y : ℕ → Ω → ℝ} {r : ℕ → ℝ} (hX : IsLittleOp X r μ) (hXY : ∀ᶠ n in atTop, ∀ ω, Y n ω = X n ω) : IsLittleOp Y r μ := by intro ε hε exact (hX ε hε).congr' (hXY.mono fun n hn => by congr 1 ext ω simp [hn ω]) -
IsLittleOp_add_onelemma — Given two random sequences and a measure, if each sequence is little-o in probability relative to one, then their sum is also little-o relative to one.hypothesesconclusionIsLittleOp (fun n ω => X n ω + Y n ω) (fun _ => (1 : ℝ)) μProof (Lean source)
lemma IsLittleOp_add_one {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {X Y : ℕ → Ω → ℝ} (hX : IsLittleOp X (fun _ => (1 : ℝ)) μ) (hY : IsLittleOp Y (fun _ => (1 : ℝ)) μ) : IsLittleOp (fun n ω => X n ω + Y n ω) (fun _ => (1 : ℝ)) μ := add_one hX hY -
IsLittleOp_const_mul_onelemma — Given a real constant, random sequence, and measure, if the sequence is little-o in probability relative to one, then its constant multiple is too.hypothesesconclusionIsLittleOp (fun n ω => a * X n ω) (fun _ => (1 : ℝ)) μProof (Lean source)
lemma IsLittleOp_const_mul_one {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (a : ℝ) {X : ℕ → Ω → ℝ} (hX : IsLittleOp X (fun _ => (1 : ℝ)) μ) : IsLittleOp (fun n ω => a * X n ω) (fun _ => (1 : ℝ)) μ := by intro ε hε by_cases ha : a = 0 · subst a have hzero : (fun n => μ {ω | ε * (fun _ => (1 : ℝ)) n ≤ ‖0 * X n ω‖}) = fun _ => (0 : ENNReal) := by funext n simp [not_le.mpr hε] rw [hzero] exact tendsto_const_nhds · have hscale_pos : 0 < ε / |a| := div_pos hε (abs_pos.mpr ha) have hXt := hX (ε / |a|) hscale_pos refine hXt.congr' ?_ filter_upwards with n congr 1 ext ω simp only [Set.mem_setOf_eq, mul_one, norm_mul, Real.norm_eq_abs] rw [div_le_iff₀ (abs_pos.mpr ha)] ring_nf -
IsLittleOp_finset_sum_onelemma — Given a finite index set, a family of random sequences, and a measure, if every selected sequence is little-o in probability relative to one, then their finite sum is also little-o relative to one.hypothesesconclusionIsLittleOp (fun n ω => ∑ i ∈ s, f i n ω) (fun _ => (1 : ℝ)) μProof (Lean source)
lemma IsLittleOp_finset_sum_one {Ω ι : Type*} [MeasurableSpace Ω] {μ : Measure Ω} (s : Finset ι) (f : ι → ℕ → Ω → ℝ) (h : ∀ i ∈ s, IsLittleOp (f i) (fun _ => (1 : ℝ)) μ) : IsLittleOp (fun n ω => ∑ i ∈ s, f i n ω) (fun _ => (1 : ℝ)) μ := by classical revert h refine Finset.induction_on s ?base ?step · intro h simpa using (IsLittleOp_zero_one (Ω := Ω) (μ := μ)) · intro a s has ih h have ha : IsLittleOp (f a) (fun _ => (1 : ℝ)) μ := h a (Finset.mem_insert_self a s) have hs : IsLittleOp (fun n ω => ∑ i ∈ s, f i n ω) (fun _ => (1 : ℝ)) μ := by apply ih intro i hi exact h i (Finset.mem_insert_of_mem hi) have hadd := IsLittleOp_add_one ha hs simpa [Finset.sum_insert, has, add_comm, add_left_comm, add_assoc] using hadd
JacobianConsistency 2 core · 4 supporting This file derives consistency of the fold-averaged affine-score coefficient from foldwise coefficient nuisance rates. ★ feasibleCrossFitLinearDML_isAsymLinear★ feasibleCrossFitLinearDML_tendstoStandardNormal
K-fold empirical Jacobian consistency
This file derives consistency of the fold-averaged affine-score coefficient from foldwise coefficient nuisance rates. It closes the probabilistic premise used by the algebraic feasible-DML2 transfer theorem, and states the feasible DML2 asymptotic-linearity and normal-limit theorems.
The theorems with the _on_highProbEvent suffix impose the bilinear remainder bound and
the integrability conditions only on events of probability tending to one; the
theorems without the suffix are their corollaries for nuisance fits satisfying those
conditions at every realization.
theorem feasibleCrossFitLinearDML_isAsymLinear reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
Feasible K-fold affine-score DML asymptotic linearity. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, and let η̂_{n,k} be the nuisance fit used on fold k at sample size n. Assume that for every n, every fold k and every realization the population moment of m(η̂_{n,k}, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) and m(η̂_{n,k}, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; that for each fold the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that for each fold the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that for each fold the increment a(η̂_{n,k}, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same out-of-fold product σ-algebra, square-integrable at every realization, o_p(1) in L², and has a population mean that is o_p(1). Assume also z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable and the rescaled oracle cross-fitted estimator is almost-everywhere measurable at every sample size. Then the feasible cross-fitted (DML2) estimator, minus the fold-averaged empirical mean of b(η̂_{n,k}, ·) divided by the fold-averaged empirical mean of a(η̂_{n,k}, ·), is asymptotically linear at θ₀ over the full sample with influence function −J₀⁻¹·m(η₀, z, θ₀).
Formal statement
hypotheses
H :
Type u_3
M :
LinearMoment Ω μ Z P_Z H
hMZ :
MeanZero M.toGeneralMoment
hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
hK_pos :
1 < K
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
Crem :
ℝ
hBR_at :
h_m_meas :
∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)
h_m_train_uncurry :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)
h_m_int :
∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z
h_m_sq_int :
∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z
h_score_diff_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
h_product_rate :
∀ k,
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
h_a_truth :
MemLp (M.m_a M.η₀) 2 P_Z
hΔa_meas :
∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))
hΔa_uncurry_train :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))
hΔa_memLp :
∀ n k ω, MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z
hΔa_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
hΔa_bias_rate :
∀ k,
IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ
hψ_meas :
Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)
hOracle_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μ
conclusion
IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)
Proof (Lean source)
theorem feasibleCrossFitLinearDML_isAsymLinear
[StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ]
(M : LinearMoment Ω μ Z P_Z H)
(hMZ : MeanZero M.toGeneralMoment)
(hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z)
(sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 1 < K)
(split : KFoldSplit sample K)
(η_hat : ℕ → Fin K → Ω → H) {Crem : ℝ}
(hBR_at : ∀ n k ω,
|∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤
Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ))
(h_m_meas : ∀ n k, Measurable
(fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀))
(h_m_train_uncurry : ∀ n k,
Measurable[(comap
(fun ω (i : split.trainComplement n k) => sample.Z i ω)
inferInstance).prod (inferInstance : MeasurableSpace Z)]
(fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀))
(h_m_int : ∀ n k ω,
Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z)
(h_m_sq_int : ∀ n k ω,
Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z)
(h_score_diff_rate : ∀ k, IsLittleOp
(fun n ω => (eLpNorm
(fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀)
2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(h_product_rate : ∀ k, IsLittleOp
(fun n ω =>
((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ)
(h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z)
(hΔa_meas : ∀ n k, Measurable (uncurry
(fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)))
(hΔa_uncurry_train : ∀ n k,
Measurable[(comap
(fun ω (i : split.trainComplement n k) => sample.Z i ω)
inferInstance).prod (inferInstance : MeasurableSpace Z)]
(uncurry
(fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)))
(hΔa_memLp : ∀ n k ω,
MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z)
(hΔa_rate : ∀ k, IsLittleOp
(fun n ω => (eLpNorm
(fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(hΔa_bias_rate : ∀ k, IsLittleOp
(fun n ω => ∫ z,
(M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z)
(fun _ => (1 : ℝ)) μ)
(hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀))
(hOracle_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat)
M.θ₀ (fun n => range n) n) μ) :
IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀
(fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)
sample (fun n => range n) := by
exact feasibleCrossFitLinearDML_isAsymLinear_on_highProbEvent M hMZ hFV sample
hK_pos split η_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp)
(fun n k ω _ => hBR_at n k ω) h_m_meas h_m_train_uncurry
(fun n k ω _ => h_m_int n k ω) (fun n k ω _ => h_m_sq_int n k ω)
h_score_diff_rate h_product_rate h_a_truth hΔa_meas hΔa_uncurry_train
(fun n k ω _ => hΔa_memLp n k ω) hΔa_rate hΔa_bias_rate hψ_meas hOracle_meas
theorem feasibleCrossFitLinearDML_tendstoStandardNormal reviewed
⚑ flagged
Causalean.Estimation.OrthogonalMoments
Pointwise scalar DML2 specialization of Chernozhukov et al. (2018), Theorem 3.1. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, and let η̂_{n,k} be the nuisance fit used on fold k at sample size n. Assume that for every n, every fold k and every realization the population moment of m(η̂_{n,k}, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) and m(η̂_{n,k}, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; that for each fold the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that for each fold the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that for each fold the increment a(η̂_{n,k}, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same out-of-fold product σ-algebra, square-integrable at every realization, o_p(1) in L², and has a population mean that is o_p(1). Assume also z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable and the rescaled oracle cross-fitted estimator is almost-everywhere measurable at every sample size. Let σ be a real number that is positive and whose square is the second moment of −J₀⁻¹·m(η₀, Z, θ₀), and assume √n times the estimation error of the feasible cross-fitted estimator and the same quantity divided by σ are almost-everywhere measurable at every sample size. Then √n times the error of the feasible cross-fitted (DML2) estimator, divided by σ, converges in distribution to the standard normal law.
Formal statement
hypotheses
H :
Type u_3
M :
LinearMoment Ω μ Z P_Z H
hMZ :
MeanZero M.toGeneralMoment
hFV :
Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z
sample :
IIDSample Ω Z μ P_Z
K :
ℕ
hK_pos :
1 < K
split :
KFoldSplit sample K
η_hat :
ℕ → Fin K → Ω → H
Crem :
ℝ
hBR_at :
h_m_meas :
∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)
h_m_train_uncurry :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)
h_m_int :
∀ n k ω, Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z
h_m_sq_int :
∀ n k ω, Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z
h_score_diff_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
h_product_rate :
∀ k,
IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ
h_a_truth :
MemLp (M.m_a M.η₀) 2 P_Z
hΔa_meas :
∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))
hΔa_uncurry_train :
∀ n k,
Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))
hΔa_memLp :
∀ n k ω, MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z
hΔa_rate :
∀ k,
IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ
hΔa_bias_rate :
∀ k,
IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ
hψ_meas :
Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)
hOracle_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μ
σ :
ℝ
hσ_pos :
0 < σ
hσ_sq :
σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_Z
hNum_meas :
∀ n,
AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n) μ
hStud_meas :
∀ n,
AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) μ
conclusion
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1)
Proof (Lean source)
theorem feasibleCrossFitLinearDML_tendstoStandardNormal
[StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ]
(M : LinearMoment Ω μ Z P_Z H)
(hMZ : MeanZero M.toGeneralMoment)
(hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z)
(sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 1 < K)
(split : KFoldSplit sample K)
(η_hat : ℕ → Fin K → Ω → H) {Crem : ℝ}
(hBR_at : ∀ n k ω,
|∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤
Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ))
(h_m_meas : ∀ n k, Measurable
(fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀))
(h_m_train_uncurry : ∀ n k,
Measurable[(comap
(fun ω (i : split.trainComplement n k) => sample.Z i ω)
inferInstance).prod (inferInstance : MeasurableSpace Z)]
(fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀))
(h_m_int : ∀ n k ω,
Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z)
(h_m_sq_int : ∀ n k ω,
Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z)
(h_score_diff_rate : ∀ k, IsLittleOp
(fun n ω => (eLpNorm
(fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀)
2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(h_product_rate : ∀ k, IsLittleOp
(fun n ω =>
((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) *
((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ))
(fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ)
(h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z)
(hΔa_meas : ∀ n k, Measurable (uncurry
(fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)))
(hΔa_uncurry_train : ∀ n k,
Measurable[(comap
(fun ω (i : split.trainComplement n k) => sample.Z i ω)
inferInstance).prod (inferInstance : MeasurableSpace Z)]
(uncurry
(fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z)))
(hΔa_memLp : ∀ n k ω,
MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z)
(hΔa_rate : ∀ k, IsLittleOp
(fun n ω => (eLpNorm
(fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal)
(fun _ => (1 : ℝ)) μ)
(hΔa_bias_rate : ∀ k, IsLittleOp
(fun n ω => ∫ z,
(M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z)
(fun _ => (1 : ℝ)) μ)
(hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀))
(hOracle_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat)
M.θ₀ (fun n => range n) n) μ)
(σ : ℝ) (hσ_pos : 0 < σ)
(hσ_sq : σ ^ 2 =
∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_Z)
(hNum_meas : ∀ n, AEMeasurable
(IsAsymLinear.rescaledEstimator
(feasibleCrossFitLinearDML M sample split η_hat) M.θ₀
(fun n => range n) n) μ)
(hStud_meas : ∀ n, AEMeasurable (fun ω =>
IsAsymLinear.rescaledEstimator
(feasibleCrossFitLinearDML M sample split η_hat) M.θ₀
(fun n => range n) n ω / σ) μ) :
Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω =>
IsAsymLinear.rescaledEstimator
(feasibleCrossFitLinearDML M sample split η_hat) M.θ₀
(fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1) := by
exact feasibleCrossFitLinearDML_tendstoStandardNormal_on_highProbEvent M hMZ hFV sample
hK_pos split η_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp)
(fun n k ω _ => hBR_at n k ω) h_m_meas h_m_train_uncurry
(fun n k ω _ => h_m_int n k ω) (fun n k ω _ => h_m_sq_int n k ω)
h_score_diff_rate h_product_rate h_a_truth hΔa_meas hΔa_uncurry_train
(fun n k ω _ => hΔa_memLp n k ω) hΔa_rate hΔa_bias_rate hψ_meas hOracle_meas
σ hσ_pos hσ_sq hNum_meas hStud_meas
4 supporting declarations (lemmas, instances)
-
crossFitLinearDML_jacobianConsistency_on_highProbEventtheorem — K-fold empirical Jacobian consistency for an affine score, with square-integrability on events of probability tending to one. For an affine moment system, an i.i.d. sample, a nonempty K-fold split, and fold-specific complementary-sample nuisance fits, let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Suppose the true coefficient is square-integrable, and, on every fold, the coefficient increment is jointly and uncurried product-measurable, square-integrable at every realization in G_n, has vanishing L² norm, and has vanishing population mean. Then the fold-averaged empirical score coefficient converges in probability to the population Jacobian.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_ZK :ℕhK_pos :0 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_uncurry_train :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n k ωifω ∈ goodSet nthenMemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :∀ k,IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem crossFitLinearDML_jacobianConsistency_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 0 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_train : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n k ω, ω ∈ goodSet n → MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : ∀ k, IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale) := by classical haveI : IsProbabilityMeasure P_Z := by rw [← sample.law] exact Measure.isProbabilityMeasure_map (sample.meas 0).aemeasurable let Y : Fin K → ℕ → Ω → ℝ := fun k n ω => ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω) have hfold : ∀ k, IsLittleOp (fun n ω => Y k n ω - M.linScale) (fun _ => (1 : ℝ)) μ := by intro k let truthCentered : Z → ℝ := fun z => M.m_a M.η₀ z - M.linScale have htc_meas : Measurable truthCentered := (M.m_a_meas M.η₀).sub measurable_const have htc_mean : ∫ z, truthCentered z ∂P_Z = 0 := by rw [integral_sub (h_a_truth.integrable (by norm_num)) (integrable_const M.linScale), M.linScale_eq] simp have htc_sq : Integrable (fun z => truthCentered z ^ 2) P_Z := by exact (h_a_truth.sub (memLp_const M.linScale)).integrable_sq let truthFluct : ℕ → Ω → ℝ := fun n ω => ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, truthCentered (sample.Z i ω) have hnorm : IsBigOp (fun n ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, truthCentered (sample.Z i ω)) (fun _ => (1 : ℝ)) μ := foldNormalizedSum_isBigOp sample truthCentered htc_meas htc_mean htc_sq split k have hinv : Tendsto (fun n => (sqrt ((split.fold n k).card : ℝ))⁻¹) atTop (𝓝 0) := (Real.tendsto_sqrt_atTop.comp (tendsto_natCast_atTop_atTop.comp (split.grow k))).inv_tendsto_atTop have htruth : IsLittleOp truthFluct (fun _ => (1 : ℝ)) μ := by have hp := IsBigOp.const_mul_tendsto_zero hnorm hinv convert hp using 1 funext n ω simp only [truthFluct] rw [← mul_assoc] have hsqrt : ((split.fold n k).card : ℝ)⁻¹ = (sqrt ((split.fold n k).card : ℝ))⁻¹ * (sqrt ((split.fold n k).card : ℝ))⁻¹ := by rw [← mul_inv] rcases Nat.eq_zero_or_pos (split.fold n k).card with hz | hp · simp [hz] · rw [Real.mul_self_sqrt (by positivity)] rw [hsqrt] let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z let centered : ℕ → Ω → ℝ := fun n ω => ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, (f n ω (sample.Z i ω) - ∫ z, f n ω z ∂P_Z) have hcentered : IsLittleOp centered (fun _ => (1 : ℝ)) μ := by let G : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.fold n k).card : ℝ))⁻¹ * ∑ i ∈ split.fold n k, (f n ω (sample.Z i ω) - ∫ z, f n ω z ∂P_Z) have hG : IsLittleOp G (fun _ => (1 : ℝ)) μ := by simpa [G, f] using KFoldSplit.fold_centered_sum_isLittleOp_one_of_memLp_on_highProbEvent sample split k f goodSet Δ hΔ hfail (fun n => hΔa_meas n k) (fun n => hΔa_uncurry_train n k) (fun n ω hω => hΔa_memLp n k ω hω) (hΔa_rate k) have hGbig : IsBigOp G (fun _ => (1 : ℝ)) μ := Modes.TendstoInProbability.isBigOp_one (tendstoInProb_zero_of_isLittleOp_one' hG) have hp := IsBigOp.const_mul_tendsto_zero hGbig hinv convert hp using 1 funext n ω simp only [centered, G] rw [← mul_assoc] have hsqrt : ((split.fold n k).card : ℝ)⁻¹ = (sqrt ((split.fold n k).card : ℝ))⁻¹ * (sqrt ((split.fold n k).card : ℝ))⁻¹ := by rw [← mul_inv] rcases Nat.eq_zero_or_pos (split.fold n k).card with hz | hp · simp [hz] · rw [Real.mul_self_sqrt (by positivity)] rw [hsqrt] let biasEff : ℕ → Ω → ℝ := fun n ω => (((split.fold n k).card : ℝ)⁻¹ * (split.fold n k).card) * ∫ z, f n ω z ∂P_Z have hbias : IsLittleOp biasEff (fun _ => (1 : ℝ)) μ := by refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos (hΔa_bias_rate k) ?_ intro n ω rcases Nat.eq_zero_or_pos (split.fold n k).card with hz | hp · simp [biasEff, hz] · have hne : ((split.fold n k).card : ℝ) ≠ 0 := by positivity simp only [biasEff] rw [inv_mul_cancel₀ hne, one_mul] simpa [f] have hcombined : IsLittleOp (fun n ω => truthFluct n ω + centered n ω + biasEff n ω) (fun _ => (1 : ℝ)) μ := IsLittleOp.add_one (IsLittleOp.add_one htruth hcentered) hbias refine isLittleOp_congr_eventually hcombined ?_ have hpos : ∀ᶠ n in atTop, 0 < (split.fold n k).card := (split.grow k) (eventually_gt_atTop 0) filter_upwards [hpos] with n hp funext ω have hne : ((split.fold n k).card : ℝ) ≠ 0 := by positivity simp only [Y, truthFluct, centered, biasEff, f, truthCentered] rw [Finset.sum_sub_distrib, Finset.sum_sub_distrib, Finset.sum_sub_distrib, Finset.sum_const, Finset.sum_const, nsmul_eq_mul, nsmul_eq_mul, mul_sub, ← mul_assoc, inv_mul_cancel₀ hne, one_mul] field_simp [hne] ring let A : ℕ → Ω → ℝ := fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, Y k n ω have hA : IsLittleOp (fun n ω => A n ω - M.linScale) (fun _ => (1 : ℝ)) μ := by have hsum := IsLittleOp_finset_sum_one (Finset.univ : Finset (Fin K)) (fun k n ω => Y k n ω - M.linScale) (fun k _ => hfold k) have hscaled := IsLittleOp_const_mul_one (K : ℝ)⁻¹ hsum convert hscaled using 1 funext n ω simp only [A, Finset.sum_sub_distrib, Finset.sum_const, Finset.card_fin, nsmul_eq_mul] have hKne : (K : ℝ) ≠ 0 := by exact_mod_cast (ne_of_gt hK_pos) rw [mul_sub, ← mul_assoc, inv_mul_cancel₀ hKne, one_mul] have hzero := tendstoInProb_zero_of_isLittleOp_one' hA have hadd := Modes.TendstoInProbability.comp_continuousAt (h := hzero) (g := fun x : ℝ => x + M.linScale) (continuous_add_const M.linScale).continuousAt simpa [A, Y] using hadd -
crossFitLinearDML_jacobianConsistencytheorem — K-fold empirical Jacobian consistency for an affine score. For an affine moment system, an i.i.d. sample, a nonempty K-fold split, and fold-specific complementary-sample nuisance fits, suppose the true coefficient is square-integrable, and, on every fold, the coefficient increment is jointly and uncurried product-measurable, square-integrable, has vanishing L² norm, and has vanishing population mean. Then the fold-averaged empirical score coefficient converges in probability to the population Jacobian.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z Hsample :IIDSample Ω Z μ P_ZK :ℕhK_pos :0 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → Hh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_uncurry_train :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n k ω, MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :∀ k,IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μProof (Lean source)
theorem crossFitLinearDML_jacobianConsistency [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 0 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_train : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n k ω, MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : ∀ k, IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) : Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => (K : ℝ)⁻¹ * ∑ k : Fin K, ((split.fold n k).card : ℝ)⁻¹ * ∑ i ∈ split.fold n k, M.m_a (η_hat n k ω) (sample.Z i ω)) atTop (fun _ _ => M.linScale) := by exact crossFitLinearDML_jacobianConsistency_on_highProbEvent M sample hK_pos split η_hat (fun _ => univ) (fun _ => 0) tendsto_const_nhds (by simp) h_a_truth hΔa_meas hΔa_uncurry_train (fun n k ω _ => hΔa_memLp n k ω) hΔa_rate hΔa_bias_rate -
feasibleCrossFitLinearDML_isAsymLinear_on_highProbEventtheorem — Feasible K-fold affine-score DML asymptotic linearity, with nuisance conditions on events of probability tending to one. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, let η̂_{n,k} be the nuisance fit used on fold k at sample size n, and let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume that for every n, every fold k and every realization in G_n the population moment of m(η̂_{n,k}, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) and m(η̂_{n,k}, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; that for each fold the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that for each fold the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that for each fold the increment a(η̂_{n,k}, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same out-of-fold product σ-algebra, square-integrable at every realization in G_n, o_p(1) in L², and has a population mean that is o_p(1). Assume also z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable and the rescaled oracle cross-fitted estimator is almost-everywhere measurable at every sample size. Then the feasible cross-fitted (DML2) estimator, minus the fold-averaged empirical mean of b(η̂_{n,k}, ·) divided by the fold-averaged empirical mean of a(η̂_{n,k}, ·), is asymptotically linear at θ₀ over the full sample with influence function −J₀⁻¹·m(η₀, z, θ₀).hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z HhMZ :MeanZero M.toGeneralMomenthFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_ZK :ℕhK_pos :1 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nCrem :ℝhBR_at :h_m_meas :∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_train_uncurry :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Zh_m_sq_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Zh_score_diff_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μh_product_rate :∀ k,IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_uncurry_train :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n k ωifω ∈ goodSet nthenMemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :∀ k,IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μhψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)hOracle_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μconclusionIsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n)Proof (Lean source)
theorem feasibleCrossFitLinearDML_isAsymLinear_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (hMZ : MeanZero M.toGeneralMoment) (hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) {Crem : ℝ} (hBR_at : ∀ n k ω, ω ∈ goodSet n → |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (h_m_meas : ∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z) (h_m_sq_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z) (h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_train : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n k ω, ω ∈ goodSet n → MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : ∀ k, IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μ) : IsAsymLinear (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by have hOracle := crossFitOneStepOracleDML_isAsymLinear_on_highProbEvent M.toGeneralMoment hMZ hFV sample hK_pos split η_hat goodSet Δ hΔ hfail hBR_at h_m_meas h_m_train_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate have hJ := crossFitLinearDML_jacobianConsistency_on_highProbEvent M sample (Nat.zero_lt_of_lt hK_pos) split η_hat goodSet Δ hΔ hfail h_a_truth hΔa_meas hΔa_uncurry_train hΔa_memLp hΔa_rate hΔa_bias_rate exact feasibleCrossFitLinearDML_isAsymLinear_of_jacobianConsistency M sample split η_hat hOracle hJ hψ_meas hOracle_meas -
feasibleCrossFitLinearDML_tendstoStandardNormal_on_highProbEventtheorem — Scalar DML2 specialization of Chernozhukov et al. (2018), Theorem 3.1, with nuisance conditions on events of probability tending to one. Take a moment system whose score is affine in the parameter, m(η, z, θ) = a(η, z)·θ + b(η, z), with true nuisance η₀, true parameter θ₀, error gauges ρ₁ and ρ₂, and linearization scale J₀ equal to the population mean of a(η₀, ·), whose score has mean zero at the truth and finite second moment at the truth. Let an i.i.d. sample be split into K folds with K at least two, let η̂_{n,k} be the nuisance fit used on fold k at sample size n, and let G_n be events whose complements have probability at most Δ_n for a sequence Δ_n that tends to zero. Assume that for every n, every fold k and every realization in G_n the population moment of m(η̂_{n,k}, ·, θ₀) is bounded in absolute value by a fixed constant times ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) and m(η̂_{n,k}, ·, θ₀) is integrable and square-integrable under the observation law; that (ω, z) ↦ m(η̂_{n,k}(ω), z, θ₀) is jointly measurable and is measurable with respect to the product of the σ-algebra generated by the observations outside fold k and the σ-algebra on the observation space; that for each fold the L² distance between m(η̂_{n,k}, ·, θ₀) and m(η₀, ·, θ₀) is o_p(1); and that for each fold the product ρ₁(η̂_{n,k}, η₀)·ρ₂(η̂_{n,k}, η₀) is o_p(n^(−1/2)). For the coefficient, assume a(η₀, ·) is square-integrable and that for each fold the increment a(η̂_{n,k}, ·) − a(η₀, ·) is jointly measurable in (ω, z), measurable with respect to the same out-of-fold product σ-algebra, square-integrable at every realization in G_n, o_p(1) in L², and has a population mean that is o_p(1). Assume also z ↦ −J₀⁻¹·m(η₀, z, θ₀) is measurable and the rescaled oracle cross-fitted estimator is almost-everywhere measurable at every sample size. Let σ be a real number that is positive and whose square is the second moment of −J₀⁻¹·m(η₀, Z, θ₀), and assume √n times the estimation error of the feasible cross-fitted estimator and the same quantity divided by σ are almost-everywhere measurable at every sample size. Then √n times the error of the feasible cross-fitted (DML2) estimator, divided by σ, converges in distribution to the standard normal law.hypothesesH :sharedType u_3M :LinearMoment Ω μ Z P_Z HhMZ :MeanZero M.toGeneralMomenthFV :Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Zsample :IIDSample Ω Z μ P_ZK :ℕhK_pos :1 < Ksplit :KFoldSplit sample Kη_hat :ℕ → Fin K → Ω → HgoodSet :ℕ → Set ΩΔ :ℕ → ℝ≥0∞hfail :∀ n, μ (goodSet n)ᶜ ≤ Δ nCrem :ℝhBR_at :h_m_meas :∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_train_uncurry :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)h_m_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Zh_m_sq_int :∀ n k ωifω ∈ goodSet nthenIntegrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Zh_score_diff_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μh_product_rate :∀ k,IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μh_a_truth :MemLp (M.m_a M.η₀) 2 P_ZhΔa_meas :∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_uncurry_train :∀ n k,Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))hΔa_memLp :∀ n k ωifω ∈ goodSet nthenMemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_ZhΔa_rate :∀ k,IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μhΔa_bias_rate :∀ k,IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μhψ_meas :Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)hOracle_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μσ :ℝhσ_pos :0 < σhσ_sq :σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_ZhNum_meas :∀ n,AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n) μhStud_meas :∀ n,AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) μconclusionModes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1)Proof (Lean source)
theorem feasibleCrossFitLinearDML_tendstoStandardNormal_on_highProbEvent [StandardBorelSpace Ω] [IsFiniteMeasure μ] [IsProbabilityMeasure μ] (M : LinearMoment Ω μ Z P_Z H) (hMZ : MeanZero M.toGeneralMoment) (hFV : Integrable (fun z => (M.m M.η₀ z M.θ₀) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) {K : ℕ} (hK_pos : 1 < K) (split : KFoldSplit sample K) (η_hat : ℕ → Fin K → Ω → H) (goodSet : ℕ → Set Ω) (Δ : ℕ → ℝ≥0∞) (hΔ : Tendsto Δ atTop (𝓝 0)) (hfail : ∀ n, μ (goodSet n)ᶜ ≤ Δ n) {Crem : ℝ} (hBR_at : ∀ n k ω, ω ∈ goodSet n → |∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z| ≤ Crem * ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (h_m_meas : ∀ n k, Measurable (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_train_uncurry : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n k p.1) p.2 M.θ₀)) (h_m_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => M.m (η_hat n k ω) z M.θ₀) P_Z) (h_m_sq_int : ∀ n k ω, ω ∈ goodSet n → Integrable (fun z => (M.m (η_hat n k ω) z M.θ₀) ^ 2) P_Z) (h_score_diff_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (h_product_rate : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ) (h_a_truth : MemLp (M.m_a M.η₀) 2 P_Z) (hΔa_meas : ∀ n k, Measurable (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_uncurry_train : ∀ n k, Measurable[(comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (fun ω z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z))) (hΔa_memLp : ∀ n k ω, ω ∈ goodSet n → MemLp (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z) (hΔa_rate : ∀ k, IsLittleOp (fun n ω => (eLpNorm (fun z => M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) 2 P_Z).toReal) (fun _ => (1 : ℝ)) μ) (hΔa_bias_rate : ∀ k, IsLittleOp (fun n ω => ∫ z, (M.m_a (η_hat n k ω) z - M.m_a M.η₀ z) ∂P_Z) (fun _ => (1 : ℝ)) μ) (hψ_meas : Measurable (fun z => -M.linScaleInv * M.m M.η₀ z M.θ₀)) (hOracle_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (crossFitOneStepOracleDML M.toGeneralMoment sample split η_hat) M.θ₀ (fun n => range n) n) μ) (σ : ℝ) (hσ_pos : 0 < σ) (hσ_sq : σ ^ 2 = ∫ z, (-M.linScaleInv * M.m M.η₀ z M.θ₀) ^ 2 ∂P_Z) (hNum_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n) μ) (hStud_meas : ∀ n, AEMeasurable (fun ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) μ) : Modes.TendstoInLaw (fun _ : ℕ => μ) (fun n ω => IsAsymLinear.rescaledEstimator (feasibleCrossFitLinearDML M sample split η_hat) M.θ₀ (fun n => range n) n ω / σ) atTop (gaussianMeasure 0 1) := by have hAL := feasibleCrossFitLinearDML_isAsymLinear_on_highProbEvent M hMZ hFV sample hK_pos split η_hat goodSet Δ hΔ hfail hBR_at h_m_meas h_m_train_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate h_a_truth hΔa_meas hΔa_uncurry_train hΔa_memLp hΔa_rate hΔa_bias_rate hψ_meas hOracle_meas exact feasibleCrossFitLinearDML_tendstoStandardNormal_of_isAsymLinear M sample split η_hat hAL hψ_meas σ hσ_pos hσ_sq hNum_meas hStud_meas