Estimation.Orthogonal­Moments

theorem dml_chernozhukov_asymptoticLinear [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) (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 : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n ω) z M.θ₀)) (_h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (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 : ℝ))) μ) : IsAsymLinear (dmlChernozhukovEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample split.foldB := by refine ⟨?_, ?_, ?_⟩ · -- mean_zero rw [integral_const_mul] rw [show (∫ a, M.m M.η₀ a M.θ₀ ∂P_Z) = 0 by simpa [MeanZero] using _hMZ] ring · -- finite_var simpa [mul_pow, mul_assoc, mul_left_comm, mul_comm] using (_hFV.const_mul (M.J₀_inv ^ 2)) · -- remainder: centered fold-B fluctuation plus population remainder. let f : ℕ → Ω → Z → ℝ := fun n ω z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀ let G : ℕ → Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ z, f n ω z ∂P_Z) let B : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * ∫ z, f n ω z ∂P_Z let R : ℕ → Ω → ℝ := fun n ω => sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split η_hat n ω - M.θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (-M.J₀_inv * M.m M.η₀ (sample.Z i ω) M.θ₀) 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 hf_meas : ∀ n, Measurable (uncurry (f n)) := by intro n change Measurable (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_meas n).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω => f n ω) := by intro n change Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n ω) z M.θ₀ - M.m M.η₀ z M.θ₀) exact (_h_m_foldA n).sub measurable_const have hf_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (uncurry (f n)) := by intro n change Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace Z)] (fun p : Ω × Z => M.m (η_hat n p.1) p.2 M.θ₀ - M.m M.η₀ p.2 M.θ₀) exact (_h_m_foldA_uncurry n).sub ((M.m_meas M.η₀ M.θ₀).comp measurable_snd) have hf_memLp : ∀ n ω, MemLp (f n ω) 2 P_Z := by intro n ω have hrand_L2 : MemLp (fun z => M.m (η_hat n ω) z M.θ₀) 2 P_Z := (memLp_two_iff_integrable_sq (M.m_meas (η_hat n ω) M.θ₀).aestronglyMeasurable).2 (_h_m_sq_int n ω) 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 have hG : IsLittleOp G (fun _ => (1 : ℝ)) μ := by simpa [G] using foldB_centered_sum_isLittleOp_one sample split f hf_meas hf_uncurry_foldA hf_memLp hf_rate_one have h_int_eq : ∀ n ω, ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by intro n ω have hf_int : Integrable (f n ω) P_Z := (hf_memLp n ω).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 ω) z M.θ₀ - M.m M.η₀ z M.θ₀) ∂P_Z := by rfl _ = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z := integral_sub (_h_m_int n ω) htruth_int _ = ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z := by rw [hzero] ring have h_int_raw_rate : IsLittleOp (fun n ω => ∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ let K : ℝ := |Crem| + 1 have hKpos : 0 < K := by dsimp [K] linarith [abs_nonneg Crem] have htarget := (ENNReal.tendsto_nhds_zero.mp (_h_product_rate (ε / K) (div_pos hε hKpos))) δ hδ exact htarget.mono fun n hn => (measure_mono (by intro ω hω let prodρ : ℝ := ((M.ρ₁ (η_hat n ω) M.η₀ : NNReal) : ℝ) * ((M.ρ₂ (η_hat n ω) M.η₀ : NNReal) : ℝ) have hprod_nonneg : 0 ≤ prodρ := by dsimp [prodρ] exact mul_nonneg (NNReal.coe_nonneg _) (NNReal.coe_nonneg _) have hbr := _hBR_at n ω have hbr0 : |∫ z, M.m (η_hat n ω) z M.θ₀ ∂P_Z| ≤ Crem * prodρ := by simpa [prodρ, mul_assoc] using hbr have hle_abs : |∫ z, M.m (η_hat n ω) 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 ω) z M.θ₀ ∂P_Z| ≤ K * prodρ := by refine hle_abs.trans ?_ exact mul_le_mul_of_nonneg_right (by dsimp [K]; linarith) hprod_nonneg have hlt_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < K * prodρ := lt_of_lt_of_le hω hKbound have hdiv_lt : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / K < prodρ := by rw [div_lt_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hlt_bound have hsmall : (ε / K) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < |prodρ| := by have hdiv_eq : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / K = (ε / K) * ((n : ℝ) ^ (-(1 / 2 : ℝ))) := by ring rw [← hdiv_eq] simpa [abs_of_nonneg hprod_nonneg] using hdiv_lt exact hsmall)).trans hn have h_int_rate : IsLittleOp (fun n ω => ∫ z, f n ω z ∂P_Z) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) μ := by convert h_int_raw_rate using 1 funext n ω exact h_int_eq n ω have hB : IsLittleOp B (fun _ => (1 : ℝ)) μ := by intro ε' hε' rw [ENNReal.tendsto_nhds_zero] intro δ hδ let C : ℝ := sqrt c + 1 have hCpos : 0 < C := by dsimp [C] linarith [Real.sqrt_nonneg c] have hCnonneg : 0 ≤ C := le_of_lt hCpos have hC2 : c < C ^ 2 := by dsimp [C] nlinarith [Real.sq_sqrt (le_of_lt _hc_pos), Real.sqrt_nonneg c] have hratio_event : ∀ᶠ n in atTop, ((split.foldB n).card : ℝ) / n < C ^ 2 := by exact _h_split_rate.eventually_lt_const hC2 have hn_event : ∀ᶠ n : ℕ in atTop, n ≠ 0 := by exact eventually_ne_atTop 0 have hint_event := (ENNReal.tendsto_nhds_zero.mp (h_int_rate (ε' / C) (div_pos hε' hCpos))) δ hδ -- … truncated; follow the source link for the rest …

theorem integratedMoment_diffQuotient_tendsto_zero (M : GeneralMoment Ω μ Z P_Z H) (D : HasDirDeriv M) (hNO : NeymanOrthogonal M D) (hEnv : DiffQuotientEnvelope M) {η : H} (hη : η ∈ M.H_ε) (hMt_int : ∀ t ≠ (0 : ℝ), Integrable (fun z => M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀) P_Z) (hM0_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z) : Tendsto (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) (𝓝[≠] 0) (𝓝 0) := by rcases hEnv η hη with ⟨δ, hδ_pos, g, hg_int, hg_bound⟩ let F : ℝ → Z → ℝ := fun t z => (M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀) / t have hIoo : Ioo (-δ) δ ∈ 𝓝[≠] (0 : ℝ) := by have hIoo_nhds : Ioo (-δ) δ ∈ 𝓝 (0 : ℝ) := by exact Ioo_mem_nhds (by linarith) hδ_pos exact nhdsWithin_le_nhds hIoo_nhds have h_ne : {t : ℝ | t ≠ 0} ∈ 𝓝[≠] (0 : ℝ) := self_mem_nhdsWithin have hlim_integral : Tendsto (fun t : ℝ => ∫ z, F t z ∂P_Z) (𝓝[≠] 0) (𝓝 (∫ z, D.dM η z ∂P_Z)) := by apply MeasureTheory.tendsto_integral_filter_of_dominated_convergence g · exact Filter.Eventually.of_forall (fun t => (((M.m_meas (M.η₀ + t • (η - M.η₀)) M.θ₀).sub (M.m_meas M.η₀ M.θ₀)).div_const t).aestronglyMeasurable) · filter_upwards [hIoo, h_ne] with t htIoo ht_ne exact hg_bound.mono (fun z hz => by simpa [F] using hz t htIoo ht_ne) · exact hg_int · exact Filter.Eventually.of_forall (fun z => by simpa [F] using D.pointwise_tendsto η hη z) have h_eq : (fun t : ℝ => ∫ z, F t z ∂P_Z) =ᶠ[𝓝[≠] (0 : ℝ)] (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) := by filter_upwards [h_ne] with t ht_ne calc ∫ z, F t z ∂P_Z = (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ - M.m M.η₀ z M.θ₀ ∂P_Z) / t := by simp [F, MeasureTheory.integral_div] _ = (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t := by rw [MeasureTheory.integral_sub (hMt_int t ht_ne) hM0_int] have hlim_to_deriv : Tendsto (fun t : ℝ => (∫ z, M.m (M.η₀ + t • (η - M.η₀)) z M.θ₀ ∂P_Z - ∫ z, M.m M.η₀ z M.θ₀ ∂P_Z) / t) (𝓝[≠] 0) (𝓝 (∫ z, D.dM η z ∂P_Z)) := hlim_integral.congr' h_eq simpa [NeymanOrthogonal, hNO η hη] using hlim_to_deriv

theorem bilinear_remainder_of_smoothness (M : GeneralMoment Ω μ Z P_Z H) (D : HasDirDeriv M) (hNO : NeymanOrthogonal M D) {K : ℝ} {g : Z → ℝ} (hg_int : Integrable g P_Z) (hSecond : ∀ η ∈ M.H_ε, ∀ᵐ z ∂P_Z, |M.m η z M.θ₀ - M.m M.η₀ z M.θ₀ - D.dM η z| ≤ K * ((M.ρ₁ η M.η₀ : ℝ)) * ((M.ρ₂ η M.η₀ : ℝ)) * g z) (hdM_int : ∀ η ∈ M.H_ε, Integrable (fun z => D.dM η z) P_Z) (hM0_int : Integrable (fun z => M.m M.η₀ z M.θ₀) P_Z) (hMη_int : ∀ η ∈ M.H_ε, Integrable (fun z => M.m η z M.θ₀) P_Z) (hMZ : MeanZero M) : ∃ C, BilinearRemainder M C := by refine ⟨|K| * ∫ z, |g z| ∂P_Z, ?_⟩ intro η hη let r₁ : ℝ := M.ρ₁ η M.η₀ let r₂ : ℝ := M.ρ₂ η M.η₀ let rem : Z → ℝ := fun z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀ - D.dM η z have hr₁_nonneg : 0 ≤ r₁ := by dsimp [r₁] exact NNReal.coe_nonneg _ have hr₂_nonneg : 0 ≤ r₂ := by dsimp [r₂] exact NNReal.coe_nonneg _ have hrem_int : Integrable rem P_Z := by dsimp [rem] exact ((hMη_int η hη).sub hM0_int).sub (hdM_int η hη) have hrem_abs_int : Integrable (fun z => |rem z|) P_Z := by simpa [Real.norm_eq_abs] using hrem_int.norm have hbound_int : Integrable (fun z => |K| * r₁ * r₂ * |g z|) P_Z := by simpa [Real.norm_eq_abs, mul_assoc] using (hg_int.norm.const_mul (|K| * r₁ * r₂)) have hpoint : ∀ᵐ z ∂P_Z, |rem z| ≤ |K| * r₁ * r₂ * |g z| := by filter_upwards [hSecond η hη] with z hz dsimp [rem, r₁, r₂] at hz ⊢ refine hz.trans ?_ calc K * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * g z ≤ |K * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * g z| := le_abs_self _ _ = |K| * (M.ρ₁ η M.η₀ : ℝ) * (M.ρ₂ η M.η₀ : ℝ) * |g z| := by rw [abs_mul, abs_mul, abs_mul] simp [abs_of_nonneg (NNReal.coe_nonneg (M.ρ₁ η M.η₀)), abs_of_nonneg (NNReal.coe_nonneg (M.ρ₂ η M.η₀)), mul_assoc] have hrem_integral : ∫ z, rem z ∂P_Z = ∫ z, M.m η z M.θ₀ ∂P_Z := by have hdiff_int : Integrable (fun z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀) P_Z := by exact (hMη_int η hη).sub hM0_int dsimp [rem] change ∫ z, ((fun z : Z => M.m η z M.θ₀ - M.m M.η₀ z M.θ₀) z - (fun z : Z => D.dM η z) z) ∂P_Z = ∫ z, M.m η z M.θ₀ ∂P_Z rw [integral_sub hdiff_int (hdM_int η hη)] rw [integral_sub (hMη_int η hη) hM0_int] rw [hMZ, hNO η hη] ring calc |∫ z, M.m η z M.θ₀ ∂P_Z| = |∫ z, rem z ∂P_Z| := by rw [hrem_integral] _ ≤ ∫ z, |rem z| ∂P_Z := MeasureTheory.abs_integral_le_integral_abs _ ≤ ∫ z, |K| * r₁ * r₂ * |g z| ∂P_Z := integral_mono_ae hrem_abs_int hbound_int hpoint _ = |K| * r₁ * r₂ * (∫ z, |g z| ∂P_Z) := by rw [integral_const_mul] _ = (|K| * ∫ z, |g z| ∂P_Z) * r₁ * r₂ := by ring

theorem rieszScore_meanZero {H_γ : Type*} [AddCommGroup H_γ] [Module ℝ H_γ] {γ_target : H_γ → X → ℝ} {L : H_γ → ℝ} {P_X : Measure X} [IsProbabilityMeasure P_Z] (rep : RieszRepresentation H_γ γ_target L P_X) (γ₀ : H_γ) (proj_X : Z → X) (Y_obs : Z → ℝ) (h_orthog : ∫ z, rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) ∂P_Z = 0) : ∫ z, rieszScore γ_target L proj_X Y_obs γ₀ rep.α₀ (L γ₀) z ∂P_Z = 0 := by unfold rieszScore have h1 : (fun z => L γ₀ + rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) - L γ₀) = fun z => rep.α₀ (proj_X z) * (Y_obs z - γ_target γ₀ (proj_X z)) := by funext z ring rw [h1, h_orthog]

theorem aipw_dml_isAsymLinear (S : BackdoorEstimationSystem P γ) {ε : ℝ} (hη₀_mem : S.η₀ ∈ H_ε_aeL2 S ε) (h_overlap : S.StrictOverlap ε) (hA : S.toPOBackdoorSystem.Assumptions) (h_y2 : Integrable (fun ω => (S.toPOBackdoorSystem.factualY ω) ^ 2) P.μ) (h_yd2 : ∀ d : Bool, Integrable (fun ω => (S.toPOBackdoorSystem.YofD d ω) ^ 2) P.μ) (sample : IIDSample P.Ω (γ × Bool × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → P.Ω → NuisanceVec γ) (h_in_Hε : ∀ n ω, η_hat n ω ∈ H_ε_aeL2 S ε) (h_mu_diff_memLp : ∀ n ω a, MemLp (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X) (h_e_diff_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X) (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => aipwMomentFunctional (η_hat n ω) z S.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × Bool × ℝ))] (fun (p : P.Ω × (γ × Bool × ℝ)) => aipwMomentFunctional (η_hat n p.1) p.2 S.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => aipwMomentFunctional (η_hat n ω) z S.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (aipwMomentFunctional (η_hat n ω) z S.θ₀) ^ 2) S.P_Z) (h_indiv_rate_ρ₁ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_indiv_rate_ρ₂ : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (dmlChernozhukovEstimator (aipwGeneralMoment S hη₀_mem) sample split η_hat) S.θ₀ (fun z => -(aipwGeneralMoment S hη₀_mem).J₀_inv * aipwMomentFunctional S.η₀ z S.θ₀) sample split.foldB := by have hMZ := aipw_meanZero S hη₀_mem h_overlap hA h_y2 h_yd2 have hFV : Integrable (fun z => ((aipwGeneralMoment S hη₀_mem).m (aipwGeneralMoment S hη₀_mem).η₀ z (aipwGeneralMoment S hη₀_mem).θ₀) ^ 2) S.P_Z := by simpa [aipwGeneralMoment, BackdoorEstimationSystem.ψ_AIPW, BackdoorEstimationSystem.η₀, aipwMomentFunctional] using BackdoorEstimationSystem.aipw_finite_var_of_counterfactual_sq S h_overlap hA h_y2 h_yd2 -- Per-η̂_n bilinear remainder, built directly from `aipw_remainder_bound`. -- Replaces the ∀-quantified `aipw_bilinearRem` route. have hBR_at : ∀ n ω, |∫ z, (aipwGeneralMoment S hη₀_mem).m (η_hat n ω) z (aipwGeneralMoment S hη₀_mem).θ₀ ∂S.P_Z| ≤ aipw_rem_const ε * (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) (aipwGeneralMoment S hη₀_mem).η₀ : NNReal) : ℝ) * (((aipwGeneralMoment S hη₀_mem).ρ₂ (η_hat n ω) (aipwGeneralMoment S hη₀_mem).η₀ : NNReal) : ℝ) := by intro n ω have h := BackdoorEstimationSystem.aipw_remainder_bound S h_overlap hA h_y2 h_yd2 (η_hat n ω) (h_in_Hε n ω) (h_mu_diff_memLp n ω) (h_e_diff_memLp n ω) -- Convert `Σ_a (‖Δμ_a‖ * ‖Δe‖)` into `(‖Δμ_T‖ + ‖Δμ_F‖) * ‖Δe‖`. have hsum : ∑ a : Bool, (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal = ((eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal := by rw [Fintype.sum_bool, add_mul] rw [hsum] at h -- Unfold `M = aipwGeneralMoment` (η₀.μ_fn = S.μ_val, η₀.e_fn = S.e_val). change |∫ z, aipwMomentFunctional (η_hat n ω) z S.θ₀ ∂(S.P_Z)| ≤ aipw_rem_const ε * ((eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal) * (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal linarith [h] -- Translate aggregated `ρ₁` rate into per-arm `μ_hat - μ_val` L² rate. have h_mu_rate : ∀ a : Bool, IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by intro a δ hδ rw [ENNReal.tendsto_nhds_zero] intro κ hκ have hsum_event := (ENNReal.tendsto_nhds_zero.mp (h_indiv_rate_ρ₁ δ hδ)) κ hκ filter_upwards [hsum_event] with n hn refine (measure_mono ?_).trans hn intro ω hω have hcoord_le : |(eLpNorm (fun x => (η_hat n ω).μ_fn a x - S.μ_val a x) 2 S.P_X).toReal| ≤ |(((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ)| := by -- `ρ₁` is an `NNReal` structure literal; unfolding it in the goal blocks -- every later rewrite, so bridge to its real value with a `rfl` equation. have hval : (((aipwGeneralMoment S hη₀_mem).ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) = (eLpNorm (fun x => (η_hat n ω).μ_fn true x - S.μ_val true x) 2 S.P_X).toReal + (eLpNorm (fun x => (η_hat n ω).μ_fn false x - S.μ_val false x) 2 S.P_X).toReal := rfl by_cases ha : a = true · subst a rw [hval, abs_of_nonneg ENNReal.toReal_nonneg] exact (le_add_of_nonneg_right ENNReal.toReal_nonneg).trans (le_abs_self _) · have ha_false : a = false := by cases a <;> simp_all subst a rw [hval, abs_of_nonneg ENNReal.toReal_nonneg] exact (le_add_of_nonneg_left ENNReal.toReal_nonneg).trans (le_abs_self _) exact lt_of_lt_of_le hω hcoord_le have h_e_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).e_fn x - S.e_val x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ := by exact h_indiv_rate_ρ₂ have h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => (aipwGeneralMoment S hη₀_mem).m (η_hat n ω) z (aipwGeneralMoment S hη₀_mem).θ₀ - (aipwGeneralMoment S hη₀_mem).m (aipwGeneralMoment S hη₀_mem).η₀ z (aipwGeneralMoment S hη₀_mem).θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by simpa [aipwGeneralMoment] using BackdoorEstimationSystem.aipw_score_diff_isLittleOp_one S h_overlap hA h_y2 h_yd2 η_hat h_in_Hε h_mu_diff_memLp h_e_diff_memLp h_mu_rate h_e_rate simpa [aipwGeneralMoment] using (dml_chernozhukov_asymptoticLinear (aipwGeneralMoment S hη₀_mem) hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := aipw_rem_const ε) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)

theorem dml_crossFit_asymptoticLinear [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 : ∀ n k, Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n k ω) z 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_indiv_rate_ρ₁ : ∀ k, IsLittleOp (fun n ω => ((M.ρ₁ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (fun _ => (1 : ℝ)) μ) (_h_indiv_rate_ρ₂ : ∀ k, IsLittleOp (fun n ω => ((M.ρ₂ (η_hat n k ω) M.η₀ : NNReal) : ℝ)) (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 (dmlCrossFitEstimator M sample split η_hat) M.θ₀ (fun z => -M.J₀_inv * M.m M.η₀ z M.θ₀) sample (fun n => range n) := by 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 scalar `-J₀⁻¹`. show ∫ z, -M.J₀_inv * M.m M.η₀ z M.θ₀ ∂P_Z = 0 calc ∫ z, -M.J₀_inv * M.m M.η₀ z M.θ₀ ∂P_Z = -M.J₀_inv * ∫ 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.J₀_inv * M.m M.η₀ z M.θ₀) ^ 2) P_Z have h_eq : ∀ z, (-M.J₀_inv * M.m M.η₀ z M.θ₀) ^ 2 = M.J₀_inv ^ 2 * (M.m M.η₀ z M.θ₀) ^ 2 := by intro z; ring simp_rw [h_eq] exact _hFV.const_mul (M.J₀_inv ^ 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_train : ∀ n, Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω => f n ω) := by intro n change Measurable[comap (fun ω (i : split.trainComplement n k) => sample.Z i ω) inferInstance] (fun ω z => M.m (η_hat n k ω) z M.θ₀ - M.m M.η₀ z M.θ₀) exact (_h_m_train n k).sub measurable_const 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 ω, MemLp (f n ω) 2 P_Z := by intro n ω 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 (_h_m_sq_int n k ω) 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 sample split k f 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 ω, MemLp (f n ω) 2 P_Z := by intro n ω 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 (_h_m_sq_int n k ω) simp only [f] exact hrand_L2.sub htruth_L2 have h_int_eq : ∀ n ω, ∫ z, f n ω z ∂P_Z = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by intro n ω have hf_int : Integrable (f n ω) P_Z := (hf_memLp n ω).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 (_h_m_int n k ω) htruth_int _ = ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z := by rw [hzero] ring have h_int_raw_rate : IsLittleOp (fun n ω => ∫ z, M.m (η_hat n k ω) z M.θ₀ ∂P_Z) (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δ exact htarget.mono fun n hn => (measure_mono (by intro ω 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 hbr := _hBR_at n k ω 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 hlt_bound : ε * ((n : ℝ) ^ (-(1 / 2 : ℝ))) < Kc * prodρ := lt_of_lt_of_le hω hKbound have hdiv_lt : (ε * ((n : ℝ) ^ (-(1 / 2 : ℝ)))) / Kc < prodρ := by rw [div_lt_iff₀ hKpos] simpa [mul_comm, mul_left_comm, mul_assoc] using hlt_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] -- … truncated; follow the source link for the rest …

theorem smoother_bias_holder {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {γ : Type*} [MeasurableSpace γ] {ι : Type*} (op : LinearSmootherOp Ω μ γ) (n : ℕ) (ω : Ω) (x : γ) (g : γ → ℝ) (B : Finset ι) (w : ι → ℝ) (xs : ι → γ × Bool × ℝ) (c_n : ℝ) (hLin : LinearSmootherOp.IsLinearSmoother op n ω x B w xs) (hWeights : ∑ i ∈ B, |w i| ≤ c_n) : |op.evalAt n ω (fun z => g z.1) x| ≤ c_n * WeightedNorm B w (fun i => g (xs i).1) 1 := by let S : ℝ := ∑ j ∈ B, |w j| have hS_nonneg : 0 ≤ S := by dsimp [S] exact sum_nonneg fun _ _ => abs_nonneg _ have hNorm_nonneg : 0 ≤ WeightedNorm B w (fun i => g (xs i).1) 1 := WeightedNorm_nonneg B w (fun i => g (xs i).1) 1 by_cases hS : S = 0 · have hw_zero : ∀ i ∈ B, w i = 0 := by intro i hi have h_abs_zero : |w i| = 0 := by have h_each := (Finset.sum_eq_zero_iff_of_nonneg (s := B) (f := fun i => |w i|) (fun _ _ => abs_nonneg _)).mp hS exact h_each i hi exact abs_eq_zero.mp h_abs_zero have hEval_zero : op.evalAt n ω (fun z => g z.1) x = 0 := by rw [hLin (fun z => g z.1)] apply Finset.sum_eq_zero intro i hi simp [hw_zero i hi] rw [hEval_zero, abs_zero] exact mul_nonneg (le_trans (by simpa [S] using hS_nonneg) hWeights) hNorm_nonneg · have hS_pos : 0 < S := lt_of_le_of_ne hS_nonneg (Ne.symm hS) have hAbsEval : |op.evalAt n ω (fun z => g z.1) x| ≤ ∑ i ∈ B, |w i| * |g (xs i).1| := by rw [hLin (fun z => g z.1)] calc |∑ i ∈ B, w i * g (xs i).1| ≤ ∑ i ∈ B, |w i * g (xs i).1| := Finset.abs_sum_le_sum_abs (fun i => w i * g (xs i).1) B _ = ∑ i ∈ B, |w i| * |g (xs i).1| := by apply Finset.sum_congr rfl intro i hi rw [abs_mul] have hWeighted : ∑ i ∈ B, |w i| * |g (xs i).1| = S * WeightedNorm B w (fun i => g (xs i).1) 1 := by unfold WeightedNorm simp only [Real.rpow_one, div_one] calc ∑ i ∈ B, |w i| * |g (xs i).1| = ∑ i ∈ B, S * (|w i| / S * |g (xs i).1|) := by apply Finset.sum_congr rfl intro i hi field_simp [hS] _ = S * ∑ i ∈ B, |w i| / S * |g (xs i).1| := by rw [Finset.mul_sum] calc |op.evalAt n ω (fun z => g z.1) x| ≤ S * WeightedNorm B w (fun i => g (xs i).1) 1 := by simpa [hWeighted] using hAbsEval _ ≤ c_n * WeightedNorm B w (fun i => g (xs i).1) 1 := mul_le_mul_of_nonneg_right (by simpa [S] using hWeights) hNorm_nonneg

theorem smoother_bias_product_holder {Ω : Type*} [MeasurableSpace Ω] {μ : Measure Ω} {γ : Type*} [MeasurableSpace γ] {ι : Type*} (op : LinearSmootherOp Ω μ γ) (n : ℕ) (ω : Ω) (x : γ) (g₁ g₂ : γ → ℝ) (B : Finset ι) (w : ι → ℝ) (xs : ι → γ × Bool × ℝ) (c_n p q : ℝ) (hLin : LinearSmootherOp.IsLinearSmoother op n ω x B w xs) (hWeights : ∑ i ∈ B, |w i| ≤ c_n) (hConj : HolderConjugate p q) : |op.evalAt n ω (fun z => g₁ z.1 * g₂ z.1) x| ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by let S : ℝ := ∑ j ∈ B, |w j| let α : ι → ℝ := fun i => |w i| / S have hS_nonneg : 0 ≤ S := by dsimp [S] exact sum_nonneg fun _ _ => abs_nonneg _ have hc_nonneg : 0 ≤ c_n := le_trans (by simpa [S] using hS_nonneg) hWeights have hα_nonneg : ∀ i ∈ B, 0 ≤ α i := by intro i hi exact div_nonneg (abs_nonneg _) hS_nonneg have hpq_one : 1 / p + 1 / q = 1 := by simpa using hConj.one_div_add_one_div have hNormHolder : WeightedNorm B w (fun i => g₁ (xs i).1 * g₂ (xs i).1) 1 ≤ WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by have hHolder := Real.inner_le_Lp_mul_Lq_of_nonneg (s := B) (f := fun i => (α i) ^ (1 / p) * |g₁ (xs i).1|) (g := fun i => (α i) ^ (1 / q) * |g₂ (xs i).1|) hConj (by intro i hi exact mul_nonneg (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)) (by intro i hi exact mul_nonneg (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)) have hLeft : (∑ i ∈ B, ((α i) ^ (1 / p) * |g₁ (xs i).1|) * ((α i) ^ (1 / q) * |g₂ (xs i).1|)) = ∑ i ∈ B, α i * |g₁ (xs i).1 * g₂ (xs i).1| := by apply Finset.sum_congr rfl intro i hi rw [abs_mul] calc ((α i) ^ (1 / p) * |g₁ (xs i).1|) * ((α i) ^ (1 / q) * |g₂ (xs i).1|) = ((α i) ^ (1 / p) * (α i) ^ (1 / q)) * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by ring _ = (α i) ^ (1 / p + 1 / q) * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by rw [Real.rpow_add_of_nonneg (hα_nonneg i hi) hConj.one_div_nonneg hConj.symm.one_div_nonneg] _ = α i * (|g₁ (xs i).1| * |g₂ (xs i).1|) := by rw [hpq_one, Real.rpow_one] have hRight₁ : (∑ i ∈ B, ((α i) ^ (1 / p) * |g₁ (xs i).1|) ^ p) = ∑ i ∈ B, α i * |g₁ (xs i).1| ^ p := by apply Finset.sum_congr rfl intro i hi rw [Real.mul_rpow (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)] rw [one_div, Real.rpow_inv_rpow (hα_nonneg i hi) hConj.ne_zero] have hRight₂ : (∑ i ∈ B, ((α i) ^ (1 / q) * |g₂ (xs i).1|) ^ q) = ∑ i ∈ B, α i * |g₂ (xs i).1| ^ q := by apply Finset.sum_congr rfl intro i hi rw [Real.mul_rpow (Real.rpow_nonneg (hα_nonneg i hi) _) (abs_nonneg _)] rw [one_div, Real.rpow_inv_rpow (hα_nonneg i hi) hConj.symm.ne_zero] unfold WeightedNorm simp only [Real.rpow_one, div_one] change (∑ i ∈ B, α i * |g₁ (xs i).1 * g₂ (xs i).1|) ≤ (∑ i ∈ B, α i * |g₁ (xs i).1| ^ p) ^ (1 / p) * (∑ i ∈ B, α i * |g₂ (xs i).1| ^ q) ^ (1 / q) rw [← hLeft, ← hRight₁, ← hRight₂] simpa [mul_assoc] using hHolder calc |op.evalAt n ω (fun z => g₁ z.1 * g₂ z.1) x| ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1 * g₂ (xs i).1) 1 := smoother_bias_holder op n ω x (fun y => g₁ y * g₂ y) B w xs c_n hLin hWeights _ ≤ c_n * WeightedNorm B w (fun i => g₁ (xs i).1) p * WeightedNorm B w (fun i => g₂ (xs i).1) q := by have := mul_le_mul_of_nonneg_left hNormHolder hc_nonneg simpa [mul_assoc] using this

theorem parametric_asymptoticLinear (m_par : ℝ → Z → ℝ) (θ₀ : ℝ) (J₀ : ℝ) (hJ : J₀ ≠ 0) (m_meas : ∀ θ, Measurable (m_par θ)) (h_mean_zero : ∫ z, m_par θ₀ z ∂P_Z = 0) (h_finite_var : Integrable (fun z => (m_par θ₀ z) ^ 2) P_Z) (sample : IIDSample Ω Z μ P_Z) (split : OneShotSplit sample) : IsAsymLinear (dmlChernozhukovEstimator (parametricMoment (Ω := Ω) (μ := μ) (P_Z := P_Z) m_par θ₀ J₀ hJ m_meas) sample split (fun _ _ => ())) θ₀ (fun z => -(J₀⁻¹) * m_par θ₀ z) sample split.foldB := by set M : GeneralMoment Ω μ Z P_Z Unit := parametricMoment m_par θ₀ J₀ hJ m_meas with hM refine ⟨?_, ?_, ?_⟩ · -- mean_zero rw [integral_const_mul, h_mean_zero, mul_zero] · -- finite_var refine (h_finite_var.const_mul (J₀⁻¹ ^ 2)).congr ?_ filter_upwards with z ring · -- remainder: identically zero, since the parametric one-step exactly -- equals the influence-function partial sum. have h_pointwise : ∀ n ω, sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω) = 0 := by intro n ω set S : ℝ := ∑ i ∈ split.foldB n, m_par θ₀ (sample.Z i ω) with hS set c : ℝ := ((split.foldB n).card : ℝ) with hc have h_sum_eq : ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω) = -(J₀⁻¹) * S := by rw [hS, ← Finset.mul_sum] have h_est : dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω = θ₀ - J₀⁻¹ * (c⁻¹ * S) := by simp [dmlChernozhukovEstimator, M, parametricMoment, GeneralMoment.J₀_inv, hS, hc] rw [h_est, h_sum_eq] by_cases hc0 : c = 0 · -- |B(n)| = 0: all sums vanish. have hcard : (split.foldB n).card = 0 := by have hcard_real : ((split.foldB n).card : ℝ) = 0 := by rw [← hc]; exact hc0 exact_mod_cast hcard_real have hS0 : S = 0 := by rw [hS] exact Finset.sum_eq_zero (fun i hi => absurd (Finset.card_pos.mpr ⟨i, hi⟩) (by rw [hcard]; exact lt_irrefl 0)) rw [hc0, hS0] simp · have hc_nn : 0 ≤ c := by rw [hc]; exact Nat.cast_nonneg _ have hc_pos : 0 < c := lt_of_le_of_ne hc_nn (Ne.symm hc0) have hsqrt_pos : 0 < sqrt c := Real.sqrt_pos.mpr hc_pos have hsqrt_ne : sqrt c ≠ 0 := ne_of_gt hsqrt_pos have h_sqrt_sq : sqrt c * sqrt c = c := Real.mul_self_sqrt hc_nn have hsqrt_inv : sqrt c * c⁻¹ = (sqrt c)⁻¹ := by field_simp rw [sq, h_sqrt_sq] calc sqrt c * (θ₀ - J₀⁻¹ * (c⁻¹ * S) - θ₀) - (sqrt c)⁻¹ * (-(J₀⁻¹) * S) = -J₀⁻¹ * (sqrt c * c⁻¹) * S + J₀⁻¹ * (sqrt c)⁻¹ * S := by ring _ = -J₀⁻¹ * (sqrt c)⁻¹ * S + J₀⁻¹ * (sqrt c)⁻¹ * S := by rw [hsqrt_inv] _ = 0 := by ring -- The remainder function equals zero everywhere, so it is `o_p(1)`. intro ε hε have h_zero_set : ∀ n, {ω : Ω | ε * (fun _ => (1 : ℝ)) n < |sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω)|} = ∅ := by intro n ext ω simp only [Set.mem_setOf_eq, Set.mem_empty_iff_false, iff_false, not_lt] rw [h_pointwise n ω] simpa using le_of_lt hε have h_meas_zero : ∀ n, μ {ω : Ω | ε * (fun _ => (1 : ℝ)) n < |sqrt ((split.foldB n).card : ℝ) * (dmlChernozhukovEstimator M sample split (fun _ _ => ()) n ω - θ₀) - (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, -(J₀⁻¹) * m_par θ₀ (sample.Z i ω)|} = 0 := by intro n rw [h_zero_set n] exact MeasureTheory.measure_empty simp_rw [h_meas_zero] exact tendsto_const_nhds

theorem oracle_expansion (op : SecondStageOperator Ω μ γ) (target : γ → ℝ) (x : γ) (d_n : ℕ → Ω → ℝ) (fHat_n : ℕ → Ω → γ × Bool × ℝ → ℝ) (f : γ × Bool × ℝ → ℝ) (bHat_n : ℕ → Ω → γ → ℝ) (BiasIdent : (ℕ → Ω → γ × Bool × ℝ → ℝ) → (γ × Bool × ℝ → ℝ) → (ℕ → Ω → γ → ℝ) → Prop) (hStab : Stable op target d_n x BiasIdent) (hCons : Tendsto_inProb d_n (fun _ => 0) μ) (hBias : BiasIdent fHat_n f bHat_n) : IsLittleOp (fun n ω => op.evalAt n ω (fHat_n n ω) x - op.evalAt n ω f x - op.evalAt n ω (fun z => bHat_n n ω z.1) x) (fun n => SecondStageOperator.oracleRiskScale op f target x n) μ := by exact hStab fHat_n f bHat_n hCons hBias