Estimation.PLR

@[ext] theorem ext {η η' : PLRNuisance γ} (hl : ∀ x, η.lFn x = η'.lFn x) (hm : ∀ x, η.mFn x = η'.mFn x) : η = η' := by cases η cases η' simp only at hl hm congr · funext x exact hl x · funext x exact hm x

lemma plrMomentFunctional_factualZ (ω : P.Ω) : plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀ = (S.factualY ω - S.lVal (S.factualX ω) - S.θ * (S.factualD ω - S.mVal (S.factualX ω))) * (S.factualD ω - S.mVal (S.factualX ω)) := by rfl

theorem plr_dml_isAsymLinear (S : PLRSystem P γ) (sample : IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → P.Ω → PLRNuisance γ) -- Model-level integrability facts feeding the three PLR lemmas. (hU : Integrable S.U P.μ) (hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ) (hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ) (hD : Integrable S.factualD P.μ) (hV : MemLp S.resid 2 P.μ) (hsq : Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ) -- Per-`(n, ω)` remainder regularity, so `plr_remainder_bound` applies at -- each estimated nuisance `η_hat n ω`. (hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X) (hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X) (hUΔm : ∀ n ω, Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) (hΔlV : ∀ n ω, Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ) (hVΔm : ∀ n ω, Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) -- The abstract engine's measurability and rate bundle (copied verbatim from -- `dml_chernozhukov_asymptoticLinear` with `M := S.plrGeneralMoment`). (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z) (h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) : IsAsymLinear (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) sample split.foldB := by set Crem : ℝ := 1 + |S.θ₀| with hCrem_def have hMZ := S.plr_meanZero hU hUV hbX hD have hFV := S.plr_finite_var hsq have hBR_at : ∀ n ω, |∫ z, plrMomentFunctional (η_hat n ω) z S.θ₀ ∂S.P_Z| ≤ Crem * ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.η₀ : NNReal) : ℝ) := fun n ω => S.plr_remainder_bound (η_hat n ω) hD hbX hU (hΔl n ω) (hΔm n ω) hV (hUΔm n ω) (hΔlV n ω) (hVΔm n ω) hUV simpa [plrGeneralMoment] using (dml_chernozhukov_asymptoticLinear S.plrGeneralMoment hMZ hFV sample split hc_pos h_split_rate η_hat (Crem := Crem) hBR_at h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate)

theorem plr_dml_tendstoNormal (S : PLRSystem P γ) (sample : IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → P.Ω → PLRNuisance γ) (hU : Integrable S.U P.μ) (hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ) (hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ) (hD : Integrable S.factualD P.μ) (hV : MemLp S.resid 2 P.μ) (hsq : Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ) (hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X) (hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X) (hUΔm : ∀ n ω, Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) (hΔlV : ∀ n ω, Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ) (hVΔm : ∀ n ω, Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z) (h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) (hψ_meas : Measurable (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ) : Tendsto_dist (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)) P.μ hθn_meas := by have hAL := S.plr_dml_isAsymLinear sample split hc_pos h_split_rate η_hat hU hUV hbX hD hV hsq hΔl hΔm hUΔm hΔlV hVΔm h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate exact hAL.tendsto_normal_foldB split hψ_meas hθn_meas hSum_meas

theorem plr_dml_feasible_tendstoNormal (S : PLRSystem P γ) (sample : IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) {c : ℝ} (hc_pos : 0 < c) (h_split_rate : Tendsto (fun n => ((split.foldB n).card : ℝ) / n) atTop (𝓝 c)) (η_hat : ℕ → P.Ω → PLRNuisance γ) (hU : Integrable S.U P.μ) (hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ) (hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ) (hD : Integrable S.factualD P.μ) (hV : MemLp S.resid 2 P.μ) (hsq : Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ) (hΔl : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X) (hΔm : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X) (hUΔm : ∀ n ω, Integrable (fun ω' => S.U ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) (hΔlV : ∀ n ω, Integrable (fun ω' => ((η_hat n ω).lFn (S.factualX ω') - S.lVal (S.factualX ω')) * S.resid ω') P.μ) (hVΔm : ∀ n ω, Integrable (fun ω' => S.resid ω' * ((η_hat n ω).mFn (S.factualX ω') - S.mVal (S.factualX ω'))) P.μ) (h_m_meas : ∀ n, Measurable (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀)) (h_m_foldA_uncurry : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (fun (p : P.Ω × (γ × ℝ × ℝ)) => S.plrGeneralMoment.m (η_hat n p.1) p.2 S.plrGeneralMoment.θ₀)) (h_m_int : ∀ n ω, Integrable (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) S.P_Z) (h_m_sq_int : ∀ n ω, Integrable (fun z => (S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀) ^ 2) S.P_Z) (h_score_diff_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => S.plrGeneralMoment.m (η_hat n ω) z S.plrGeneralMoment.θ₀ - S.plrGeneralMoment.m S.plrGeneralMoment.η₀ z S.plrGeneralMoment.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ) (h_product_rate : IsLittleOp (fun n ω => ((S.plrGeneralMoment.ρ₁ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ (η_hat n ω) S.plrGeneralMoment.η₀ : NNReal) : ℝ)) (fun n => (n : ℝ) ^ (-(1 / 2 : ℝ))) P.μ) (hψ_meas : Measurable (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀)) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB n) P.μ) (hSum_meas : ∀ n, AEMeasurable (IsAsymLinear.normalizedSum sample (fun z => -S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) split.foldB n) P.μ) -- The single new probabilistic hypothesis: in-probability consistency of the -- empirical partialling-out Jacobian over fold B to its population value. (hJ_consist : Tendsto_inProb (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) (fun _ => S.plrGeneralMoment.J₀) P.μ) (hθn_feas : ∀ n, AEMeasurable (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB n) P.μ) : Tendsto_dist (IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB) (gaussianMeasure 0 (∫ z, (-S.plrGeneralMoment.J₀_inv * plrMomentFunctional S.η₀ z S.θ₀) ^ 2 ∂S.P_Z)) P.μ hθn_feas := by -- Step 1: the one-step rescaled estimator converges to the Gaussian target. have hOS := S.plr_dml_tendstoNormal sample split hc_pos h_split_rate η_hat hU hUV hbX hD hV hsq hΔl hΔm hUΔm hΔlV hVΔm h_m_meas h_m_foldA h_m_foldA_uncurry h_m_int h_m_sq_int h_score_diff_rate h_product_rate hψ_meas hθn_meas hSum_meas -- Abbreviations. set J₀ : ℝ := S.plrGeneralMoment.J₀ with hJ₀_def have hJ₀_ne : J₀ ≠ 0 := S.plrGeneralMoment.J₀_ne_zero -- The empirical partialling-out Jacobian `Pₙ mₐ = |B|⁻¹ Σ mₐ`. set Pmₐ : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω) with hPmₐ_def -- The normalized influence sum `(√|B|)⁻¹ Σ ψ`. set Sψ : ℕ → P.Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, plrMomentFunctional (η_hat n ω) (sample.Z i ω) S.θ₀ with hSψ_def -- The one-step rescaled estimator (the `Xn` of the Slutsky step). set Xn : ℕ → P.Ω → ℝ := IsAsymLinear.rescaledEstimator (dmlChernozhukovEstimator S.plrGeneralMoment sample split η_hat) S.θ₀ split.foldB with hXn_def -- The feasible rescaled estimator (the `Yn`). set Yn : ℕ → P.Ω → ℝ := IsAsymLinear.rescaledEstimator (plrFeasibleEstimator S sample split η_hat) S.θ₀ split.foldB with hYn_def -- The factor that turns out to be `o_p(1)`: `J₀⁻¹ − (Pₙmₐ)⁻¹`. set Fn : ℕ → P.Ω → ℝ := fun n ω => S.plrGeneralMoment.J₀_inv - (Pmₐ n ω)⁻¹ with hFn_def -- Step 4: `(√|B|)⁻¹ Σ ψ = −J₀ · (one-step rescaled estimator)` pointwise, -- hence `O_p(1)` by tightness of the one-step Gaussian limit. have hSψ_eq : Sψ = fun n ω => (-J₀) * Xn n ω := by funext n ω -- Abbreviate the influence sum `Σ ψ`; `m(η̂, z, θ₀) = plrMomentFunctional` -- definitionally, so this is also the empirical-moment sum of `Xn`. set Sumψ : ℝ := ∑ i ∈ split.foldB n, plrMomentFunctional (η_hat n ω) (sample.Z i ω) S.θ₀ with hSumψ_def -- The one-step empirical-moment sum is `Sumψ` (definitional projection -- equalities `m = plrMomentFunctional`, `θ₀ = S.θ₀`). have hθ₀_proj : S.plrGeneralMoment.θ₀ = S.θ₀ := rfl have hsum_m : (∑ i ∈ split.foldB n, S.plrGeneralMoment.m (η_hat n ω) (sample.Z i ω) S.θ₀) = Sumψ := rfl have hXn_val : Xn n ω = sqrt ((split.foldB n).card : ℝ) * (-(J₀⁻¹ * (((split.foldB n).card : ℝ)⁻¹ * Sumψ))) := by simp only [hXn_def, IsAsymLinear.rescaledEstimator, dmlChernozhukovEstimator, GeneralMoment.J₀_inv, hJ₀_def, hθ₀_proj, hsum_m] ring have hSψ_val : Sψ n ω = (sqrt ((split.foldB n).card : ℝ))⁻¹ * Sumψ := rfl rw [hSψ_val, hXn_val] rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard · -- Empty fold: both sides vanish. simp only [hcard, cast_zero, Real.sqrt_zero, inv_zero, zero_mul, mul_zero, neg_zero] · -- Nonempty fold: use `√|B| · |B|⁻¹ = (√|B|)⁻¹` and `J₀ · J₀⁻¹ = 1`. have hcard_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard have hcard_ne : ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hcard_pos have hsqrt_ne : sqrt ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hcard_pos) have hsqrt_sq : sqrt ((split.foldB n).card : ℝ) * sqrt ((split.foldB n).card : ℝ) = ((split.foldB n).card : ℝ) := Real.mul_self_sqrt (le_of_lt hcard_pos) -- `(√|B|)⁻¹ = √|B| · |B|⁻¹` since `|B| = √|B| · √|B|`. have hsqrt_inv : (sqrt ((split.foldB n).card : ℝ))⁻¹ = sqrt ((split.foldB n).card : ℝ) * ((split.foldB n).card : ℝ)⁻¹ := by field_simp linarith [hsqrt_sq] rw [hsqrt_inv] field_simp -- `(√|B|)⁻¹ Σ ψ = O_p(1)`. have hSψ_bigO : IsBigOp Sψ (fun _ => (1 : ℝ)) P.μ := by rw [hSψ_eq] exact const_mul (-J₀) (Tendsto_dist.tightness hθn_meas hOS) -- Step 3: `(Pₙmₐ)⁻¹ →ₚ J₀⁻¹`, hence `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ →ₚ 0`, i.e. `o_p(1)`. have hPmₐ_inv : Tendsto_inProb (fun n ω => 1 / Pmₐ n ω) (fun _ => 1 / J₀) P.μ := by have := (hJ_consist).inv hJ₀_ne simpa [hPmₐ_def, hJ₀_def] using this have hFn_inProb : Tendsto_inProb Fn (fun _ => 0) P.μ := by -- `Fn = J₀⁻¹ − (Pₙmₐ)⁻¹ = (1/J₀) − (1/Pₙmₐ)`; it converges to `0`. have hconv : Tendsto_inProb (fun n ω => (fun n ω => 1 / Pmₐ n ω) n ω - 1 / J₀) (fun _ => 0) P.μ := hPmₐ_inv.sub_const -- Rewrite `1/x = x⁻¹` and flip the sign to match `Fn`. have hneg : Tendsto_inProb (fun n ω => -(fun n ω => 1 / Pmₐ n ω - 1 / J₀) n ω) (fun _ => 0) P.μ := by have hcont : ContinuousAt (fun x : ℝ => -x) (0 : ℝ) := (continuous_neg).continuousAt have := hconv.comp_continuousAt (g := fun x : ℝ => -x) hcont simpa using this have hFn_eq : Fn = fun n ω => -((fun n ω => 1 / Pmₐ n ω) n ω - 1 / J₀) := by funext n ω simp only [hFn_def, GeneralMoment.J₀_inv, hJ₀_def, one_div] ring rw [hFn_eq] exact hneg have hFn_littleO : IsLittleOp Fn (fun _ => (1 : ℝ)) P.μ := hFn_inProb.isLittleOp_one -- Step 5: the product `Fn · Sψ = o_p(1)`. have hprod_littleO : IsLittleOp (fun n ω => Sψ n ω * Fn n ω) (fun _ => (1 : ℝ)) P.μ := hSψ_bigO.mul_isLittleOp_one_isLittleOp hFn_littleO -- Step 2 + 6: off the null event `{Pₙmₐ = 0}`, the rescaled difference equals -- `Fn · Sψ`. The null event has vanishing measure, so the rescaled difference -- is itself `o_p(1)`. -- (a) The algebraic identity on `{Pₙmₐ ≠ 0}`. have hdiff_eq : ∀ n ω, Pmₐ n ω ≠ 0 → Yn n ω - Xn n ω = Sψ n ω * Fn n ω := by intro n ω hPne -- On a nonempty fold (forced by `Pₙmₐ ≠ 0`), expand both estimators. have hcard_pos : 0 < (split.foldB n).card := by rcases Nat.eq_zero_or_pos (split.foldB n).card with hz | hpos · exact absurd (by simp only [hPmₐ_def, Finset.card_eq_zero.mp hz, Finset.sum_empty, mul_zero]) hPne · exact hpos have hcardR_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard_pos have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hcardR_pos have hsqrt_pos : (0 : ℝ) < sqrt ((split.foldB n).card : ℝ) := Real.sqrt_pos.mpr hcardR_pos have hsqrt_ne : sqrt ((split.foldB n).card : ℝ) ≠ 0 := ne_of_gt hsqrt_pos have hsqrt_sq : sqrt ((split.foldB n).card : ℝ) * sqrt ((split.foldB n).card : ℝ) = ((split.foldB n).card : ℝ) := Real.mul_self_sqrt (le_of_lt hcardR_pos) -- Denominator of the feasible estimator: `D := Σ residual²`. set D : ℝ := ∑ i ∈ split.foldB n, (plrResidual (η_hat n ω) (sample.Z i ω)) ^ 2 with hD_def -- `Σ mₐ = −D`. -- … truncated; follow the source link for the rest …

theorem plr_jacobian_consistency (S : PLRSystem P γ) (sample : IIDSample P.Ω (γ × ℝ × ℝ) P.μ S.P_Z) (split : OneShotSplit sample) (η_hat : ℕ → P.Ω → PLRNuisance γ) (hD : Integrable S.factualD P.μ) -- Square-integrability of the partialling-out moment at the truth (a fourth-moment -- condition on the treatment residual), so the fold-B WLLN applies to `mₐ(η₀, ·)`. (hg0_memLp : MemLp (plrMomentA S.η₀) 2 S.P_Z) -- Per-`(n, ω)` integrability witnesses for the bias decomposition. (hresid_sq : Integrable (fun ω => (S.factualD ω - S.mVal (S.factualX ω)) ^ 2) P.μ) (hΔm_sq : ∀ n ω, Integrable (fun ω' => (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω')) ^ 2) P.μ) (hcross : ∀ n ω, Integrable (fun ω' => (S.factualD ω' - S.mVal (S.factualX ω')) * (S.mVal (S.factualX ω') - (η_hat n ω).mFn (S.factualX ω'))) P.μ) -- L²(P_X) square-integrability of the treatment-regression error. (hΔm_memLp : ∀ n ω, MemLp (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X) -- The treatment-regression L²(P_X) `o_p(1)` rate. (h_m_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) -- Fold-A measurability of the partialling-out-moment increment (mirroring the -- `h_m_foldA`-style hypotheses of `plr_dml_isAsymLinear`: `η̂` is fold-A trained). (hΔa_meas : ∀ n, Measurable (uncurry (fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z))) (hΔa_foldA : ∀ n, Measurable[comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance] (fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z)) (hΔa_uncurry_foldA : ∀ n, Measurable[(comap (fun ω (i : split.foldA n) => sample.Z i ω) inferInstance).prod (inferInstance : MeasurableSpace (γ × ℝ × ℝ))] (uncurry (fun ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z))) -- Per-`(n, ω)` `L²(P_Z)` membership of the increment. (hΔa_memLp : ∀ n ω, MemLp (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z) -- L²(P_Z) `o_p(1)` rate of the increment (mirroring the boundedness bookkeeping of -- `plr_score_diff_isLittleOp_one`: the residual is bounded, `Δm` is bounded, and the -- L²(P_X) rate then propagates to the `mₐ`-increment). (hΔa_rate : IsLittleOp (fun n ω => (eLpNorm (fun z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ) : Tendsto_inProb (fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω)) (fun _ => S.plrGeneralMoment.J₀) P.μ := by classical -- Abbreviations: the truth statistic `g₀`, the truth-Jacobian average `Y₀`, and the -- target `Yn`. set g₀ : (γ × ℝ × ℝ) → ℝ := plrMomentA S.η₀ with hg₀_def set Yn : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, plrMomentA (η_hat n ω) (sample.Z i ω) with hYn_def set Y₀ : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, g₀ (sample.Z i ω) with hY₀_def set J₀ : ℝ := S.plrGeneralMoment.J₀ with hJ₀_def -- STEP 2: `Y₀ →ₚ J₀` by the fold-B WLLN, with the limit rewritten by step 1. have hY₀_lim : Tendsto_inProb Y₀ (fun _ => J₀) P.μ := by have hwlln := OneShotSplit.foldB_sampleMean_tendsto_inProb sample split (measurable_plrMomentA S.η₀) hg0_memLp have hint : ∫ z, g₀ z ∂S.P_Z = J₀ := S.integral_plrMomentA_η₀_eq_J₀ rw [hint] at hwlln exact hwlln -- STEP 3a (bias): `bias n ω = ∫ Δa dP_Z = −‖Δm‖²₂`, which is `o_p(1)`. set bias : ℕ → P.Ω → ℝ := fun n ω => ∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z with hbias_def have hbias_eq : ∀ n ω, bias n ω = -((eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal) ^ 2 := by intro n ω simp only [hbias_def] rw [S.integral_plrMomentA_diff_eq (η_hat n ω) hD hresid_sq (hΔm_sq n ω) (hcross n ω)] rw [S.integral_Δm_sq_eq_rate_sq (η_hat n ω) (hΔm_memLp n ω)] -- `‖Δm‖₂ →ₚ 0`, so its square →ₚ 0, so `bias →ₚ 0`, hence `o_p(1)`. set rateM : ℕ → P.Ω → ℝ := fun n ω => (eLpNorm (fun x => S.mVal x - (η_hat n ω).mFn x) 2 S.P_X).toReal with hrateM_def have hrateM_lo : IsLittleOp rateM (fun _ => (1 : ℝ)) P.μ := h_m_rate have hrateM_inProb : Tendsto_inProb rateM (fun _ => 0) P.μ := tendsto_inProb_zero_of_isLittleOp_one hrateM_lo have hrateMsq_inProb : Tendsto_inProb (fun n ω => (rateM n ω) ^ 2) (fun _ => 0) P.μ := by have hcont : ContinuousAt (fun x : ℝ => x ^ 2) (0 : ℝ) := (continuous_pow 2).continuousAt have := hrateM_inProb.comp_continuousAt (g := fun x : ℝ => x ^ 2) hcont simpa using this have hbias_inProb : Tendsto_inProb bias (fun _ => 0) P.μ := by have heq : bias = fun n ω => -((rateM n ω) ^ 2) := by funext n ω; rw [hbias_eq n ω, hrateM_def] rw [heq] have hcont : ContinuousAt (fun x : ℝ => -x) (0 : ℝ) := (continuous_neg).continuousAt have := hrateMsq_inProb.comp_continuousAt (g := fun x : ℝ => -x) hcont simpa using this have hbias_lo : IsLittleOp bias (fun _ => (1 : ℝ)) P.μ := hbias_inProb.isLittleOp_one -- The "effective" bias `(|B|⁻¹·|B|)·bias` — equal to `bias` on nonempty folds and `0` -- on empty folds — so that the pointwise decomposition below holds for ALL `n`. Its -- `{0,1}`-valued prefactor leaves it `o_p(1)`. set biasEff : ℕ → P.Ω → ℝ := fun n ω => (((split.foldB n).card : ℝ)⁻¹ * (split.foldB n).card) * bias n ω with hbiasEff_def have hbiasEff_lo : IsLittleOp biasEff (fun _ => (1 : ℝ)) P.μ := by refine IsLittleOp.of_abs_le_const_mul_one (C := 1) one_pos hbias_lo ?_ intro n ω simp only [hbiasEff_def] rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard · simp [hcard] · have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := by simp only [ne_eq, Nat.cast_eq_zero]; omega rw [inv_mul_cancel₀ hcardR_ne, one_mul, one_mul] -- STEP 3b (centered): `centered n ω = |B|⁻¹ Σ (Δa(Zᵢ) − ∫Δa)` is `o_p(1)`. set centered : ℕ → P.Ω → ℝ := fun n ω => ((split.foldB n).card : ℝ)⁻¹ * ∑ i ∈ split.foldB n, ((plrMomentA (η_hat n ω) (sample.Z i ω) - plrMomentA S.η₀ (sample.Z i ω)) - ∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z) with hcentered_def have hcentered_lo : IsLittleOp centered (fun _ => (1 : ℝ)) P.μ := by -- The fold-B centered empirical-process bound gives the `(√|B|)⁻¹`-normalized sum -- as `o_p(1)`; renormalizing by the extra `(√|B|)⁻¹ → 0` factor keeps it `o_p(1)`. -- The random function family `f n ω z = mₐ(η̂(n,ω), z) − mₐ(η₀, z)`. set f : ℕ → P.Ω → (γ × ℝ × ℝ) → ℝ := fun n ω z => plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z with hf_def -- The `(√|B|)⁻¹`-normalized centered fold-B sum is `o_p(1)`. have hsqrt_centered : IsLittleOp (fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ x, f n ω x ∂S.P_Z)) (fun _ => (1 : ℝ)) P.μ := foldB_centered_sum_isLittleOp_one sample split f hΔa_meas hΔa_uncurry_foldA hΔa_memLp hΔa_rate set centeredSqrt : ℕ → P.Ω → ℝ := fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * ∑ i ∈ split.foldB n, (f n ω (sample.Z i ω) - ∫ x, f n ω x ∂S.P_Z) with hcenteredSqrt_def -- `centeredSqrt` is `O_p(1)` (it converges in probability to `0`). have hcenteredSqrt_bigO : IsBigOp centeredSqrt (fun _ => (1 : ℝ)) P.μ := (tendsto_inProb_zero_of_isLittleOp_one hsqrt_centered).isBigOp_one -- The deterministic factor `(√|B(n)|)⁻¹ → 0`, since `|B(n)| → ∞`. have ha_tendsto : Tendsto (fun n => (sqrt ((split.foldB n).card : ℝ))⁻¹) atTop (𝓝 0) := by have hcard : Tendsto (fun n => ((split.foldB n).card : ℝ)) atTop atTop := tendsto_natCast_atTop_atTop.comp split.foldB_card_tendsto have hsqrt : Tendsto (fun n => sqrt ((split.foldB n).card : ℝ)) atTop atTop := Real.tendsto_sqrt_atTop.comp hcard exact hsqrt.inv_tendsto_atTop -- `centered = (√|B|)⁻¹ · centeredSqrt`, an `o_p(1)·(→0)` product. have hprod_lo : IsLittleOp (fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * centeredSqrt n ω) (fun _ => (1 : ℝ)) P.μ := IsBigOp.const_mul_tendsto_zero hcenteredSqrt_bigO ha_tendsto -- Pointwise: `centered = (√|B|)⁻¹ · centeredSqrt`. have hcentered_eq : centered = fun n ω => (sqrt ((split.foldB n).card : ℝ))⁻¹ * centeredSqrt n ω := by funext n ω simp only [hcentered_def, hcenteredSqrt_def, hf_def] rw [← mul_assoc] -- `|B|⁻¹ = (√|B|)⁻¹ · (√|B|)⁻¹`. have hinv : ((split.foldB n).card : ℝ)⁻¹ = (sqrt ((split.foldB n).card : ℝ))⁻¹ * (sqrt ((split.foldB n).card : ℝ))⁻¹ := by rw [← mul_inv] rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard · simp [hcard] · have hcardR_pos : (0 : ℝ) < ((split.foldB n).card : ℝ) := by exact_mod_cast hcard rw [Real.mul_self_sqrt (le_of_lt hcardR_pos)] rw [hinv] rw [hcentered_eq] exact hprod_lo -- STEP 3 combine: `Yn − Y₀ = centered + biasEff` pointwise, for ALL `n` (the empty -- fold makes every term — including `biasEff` — vanish). have hYn_sub_Y₀ : ∀ n ω, Yn n ω - Y₀ n ω = centered n ω + biasEff n ω := by intro n ω rcases Nat.eq_zero_or_pos (split.foldB n).card with hcard | hcard · -- Empty fold: every term is `0`. simp only [hYn_def, hY₀_def, hcentered_def, hbiasEff_def, hbias_def, hg₀_def, Finset.card_eq_zero.mp hcard, Finset.sum_empty, Finset.card_empty, mul_zero, cast_zero, inv_zero, zero_mul, sub_zero, add_zero] · -- Nonempty fold: `|B|⁻¹ Σ Δa = |B|⁻¹ Σ (Δa − c) + c` where `c = ∫Δa` and the -- correction `|B|⁻¹ · |B| · c = c`. have hcardR_ne : ((split.foldB n).card : ℝ) ≠ 0 := by simp only [ne_eq, Nat.cast_eq_zero]; omega simp only [hYn_def, hY₀_def, hcentered_def, hbiasEff_def, hbias_def, hg₀_def] set c : ℝ := ∫ z, (plrMomentA (η_hat n ω) z - plrMomentA S.η₀ z) ∂S.P_Z with hc_def -- RHS centered sum splits as `Σ (Δaᵢ) − |B|·c`. rw [Finset.sum_sub_distrib, Finset.sum_const, nsmul_eq_mul] rw [Finset.sum_sub_distrib, mul_sub, ← mul_assoc] rw [inv_mul_cancel₀ hcardR_ne, one_mul] ring have hYn_sub_Y₀_lo : IsLittleOp (fun n ω => Yn n ω - Y₀ n ω) (fun _ => (1 : ℝ)) P.μ := by have heq : (fun n ω => Yn n ω - Y₀ n ω) = fun n ω => centered n ω + biasEff n ω := by funext n ω; exact hYn_sub_Y₀ n ω rw [heq] exact IsLittleOp.add_one hcentered_lo hbiasEff_lo -- STEP 4: `Yn − J₀ = (Yn − Y₀) + (Y₀ − J₀)`, both `o_p(1)`; back to `Tendsto_inProb`. have hY₀_sub_lo : IsLittleOp (fun n ω => Y₀ n ω - J₀) (fun _ => (1 : ℝ)) P.μ := hY₀_lim.sub_const.isLittleOp_one have hYn_sub_J₀_lo : IsLittleOp (fun n ω => Yn n ω - J₀) (fun _ => (1 : ℝ)) P.μ := by have heq : (fun n ω => Yn n ω - J₀) = fun n ω => (Yn n ω - Y₀ n ω) + (Y₀ n ω - J₀) := by funext n ω; ring rw [heq] exact IsLittleOp.add_one hYn_sub_Y₀_lo hY₀_sub_lo -- Convert `IsLittleOp (Yn − J₀) 1` back into `Tendsto_inProb Yn J₀`. have hYn_sub_inProb : Tendsto_inProb (fun n ω => Yn n ω - J₀) (fun _ => 0) P.μ := tendsto_inProb_zero_of_isLittleOp_one hYn_sub_J₀_lo -- `Yn = (Yn − J₀) + J₀`, so `Yn →ₚ J₀`. have hfinal : Tendsto_inProb Yn (fun _ => J₀) P.μ := by have hcont : ContinuousAt (fun x : ℝ => x + J₀) (0 : ℝ) := (continuous_add_const J₀).continuousAt have := hYn_sub_inProb.comp_continuousAt (g := fun x : ℝ => x + J₀) hcont simpa using this exact hfinal

lemma plr_meanZero (hU : Integrable S.U P.μ) (hUV : Integrable (fun ω => S.U ω * S.toPOPartialLinearModel.resid ω) P.μ) (hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ) (hD : Integrable S.factualD P.μ) : MeanZero S.plrGeneralMoment := by change ∫ z, plrMomentFunctional S.η₀ z S.θ₀ ∂S.P_Z = 0 rw [S.integral_P_Z (measurable_plrMomentFunctional S.η₀ S.θ₀)] have hae : (fun ω => plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) =ᵐ[P.μ] fun ω => S.U ω * S.toPOPartialLinearModel.resid ω := by filter_upwards [S.lVal_compat, S.mVal_compat, S.factualY_sub_lReg hD hbX hU] with ω hl hm hY rw [S.plrMomentFunctional_factualZ ω, hl, hm] have hresid : S.toPOPartialLinearModel.resid ω = S.factualD ω - S.mReg ω := rfl rw [← hresid, hY] ring rw [integral_congr_ae hae, S.integral_U_resid hU hUV]

lemma plr_finite_var (hsq : Integrable (fun ω => (plrMomentFunctional S.η₀ (S.factualZ ω) S.θ₀) ^ 2) P.μ) : Integrable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) S.P_Z := by have hg : AEStronglyMeasurable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) S.P_Z := ((measurable_plrMomentFunctional S.η₀ S.θ₀).pow_const 2).aestronglyMeasurable change Integrable (fun z => (plrMomentFunctional S.η₀ z S.θ₀) ^ 2) (P.μ.map S.factualZ) rw [MeasureTheory.integrable_map_measure hg S.measurable_factualZ.aemeasurable] exact hsq

lemma plr_remainder_bound (η : PLRNuisance γ) (hD : Integrable S.factualD P.μ) (hbX : Integrable (fun ω => S.b (S.factualX ω)) P.μ) (hU : Integrable S.U P.μ) (hΔl : MemLp (fun x => η.lFn x - S.lVal x) 2 S.P_X) (hΔm : MemLp (fun x => η.mFn x - S.mVal x) 2 S.P_X) (hV : MemLp S.resid 2 P.μ) -- L¹ control of the orthogonal cross terms (each derivable from the above -- by Cauchy–Schwarz, but kept as explicit integrability hypotheses). (hUΔm : Integrable (fun ω => S.U ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ) (hΔlV : Integrable (fun ω => (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) * S.resid ω) P.μ) (hVΔm : Integrable (fun ω => S.resid ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) P.μ) (hUV : Integrable (fun ω => S.U ω * S.resid ω) P.μ) : |∫ z, plrMomentFunctional η z S.θ₀ ∂S.P_Z| ≤ (1 + |S.θ₀|) * ((S.plrGeneralMoment.ρ₁ η S.η₀ : NNReal) : ℝ) * ((S.plrGeneralMoment.ρ₂ η S.η₀ : NNReal) : ℝ) := by -- Notation for the two pulled-back nuisance errors. set δl : P.Ω → ℝ := fun ω => η.lFn (S.factualX ω) - S.lVal (S.factualX ω) with hδl_def set δm : P.Ω → ℝ := fun ω => η.mFn (S.factualX ω) - S.mVal (S.factualX ω) with hδm_def -- L²(μ) membership of the pulled-back errors, transported from L²(P_X). have hδl : MemLp δl 2 P.μ := hΔl.comp_of_map (f := S.factualX) S.measurable_factualX.aemeasurable have hδm : MemLp δm 2 P.μ := hΔm.comp_of_map (f := S.factualX) S.measurable_factualX.aemeasurable -- Step 1: change of variables to the `μ`-level integral. rw [S.integral_P_Z (measurable_plrMomentFunctional η S.θ₀)] -- Step 2: pointwise-a.e. rewrite of the integrand. have hae : (fun ω => plrMomentFunctional η (S.factualZ ω) S.θ₀) =ᵐ[P.μ] fun ω => (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω) := by filter_upwards [S.lVal_compat, S.mVal_compat, S.factualY_sub_lReg hD hbX hU] with ω hl hm hY simp only [plrMomentFunctional, plrResidual, hδl_def, hδm_def] change (S.factualY ω - η.lFn (S.factualX ω) - S.θ₀ * (S.factualD ω - η.mFn (S.factualX ω))) * (S.factualD ω - η.mFn (S.factualX ω)) = (S.U ω - (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) + S.θ * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) * (S.resid ω - (η.mFn (S.factualX ω) - S.mVal (S.factualX ω))) have hr : S.resid ω = S.factualD ω - S.mReg ω := rfl have ht : S.θ₀ = S.θ := rfl rw [ht] rw [hr] at hY ⊢ rw [hl, hm] linear_combination (S.factualD ω - η.mFn (S.factualX ω)) * hY rw [integral_congr_ae hae] -- `δl, δm` are σ(X)-pullbacks, hence orthogonal to `U` and `resid`. have hδl_meas : Measurable (fun x => η.lFn x - S.lVal x) := η.lMeas.sub S.lVal_meas have hδm_meas : Measurable (fun x => η.mFn x - S.mVal x) := η.mMeas.sub S.mVal_meas -- Step 3: the three orthogonal cross terms vanish. have h_U_resid : ∫ ω, S.U ω * S.resid ω ∂P.μ = 0 := S.integral_U_resid hU hUV have h_U_δm : ∫ ω, S.U ω * δm ω ∂P.μ = 0 := by rw [hδm_def] exact S.integral_condExpZero_mul_comp_factualX hδm_meas S.condExp_U_sigmaX hU hUΔm have h_δl_resid : ∫ ω, δl ω * S.resid ω ∂P.μ = 0 := by have hcomm : (fun ω => δl ω * S.resid ω) = fun ω => S.resid ω * (η.lFn (S.factualX ω) - S.lVal (S.factualX ω)) := by funext ω; rw [hδl_def]; ring rw [hcomm] exact S.integral_condExpZero_mul_comp_factualX hδl_meas (S.condExp_resid_sigmaX hD) (hV.integrable (by norm_num)) (by simpa [mul_comm] using hΔlV) have h_δm_resid : ∫ ω, δm ω * S.resid ω ∂P.μ = 0 := by have hcomm : (fun ω => δm ω * S.resid ω) = fun ω => S.resid ω * (η.mFn (S.factualX ω) - S.mVal (S.factualX ω)) := by funext ω; rw [hδm_def]; ring rw [hcomm] exact S.integral_condExpZero_mul_comp_factualX hδm_meas (S.condExp_resid_sigmaX hD) (hV.integrable (by norm_num)) hVΔm -- Cauchy–Schwarz integrability of the two surviving (`δl·δm`, `δm²`) terms. haveI : ENNReal.HolderTriple (2 : ENNReal) (2 : ENNReal) (1 : ENNReal) := by constructor; simpa using ENNReal.inv_two_add_inv_two have hδlδm_memLp : MemLp (fun ω => δl ω * δm ω) 1 P.μ := MemLp.mul' hδm hδl have hδmsq_memLp : MemLp (fun ω => δm ω * δm ω) 1 P.μ := MemLp.mul' hδm hδm have hδlδm_int : Integrable (fun ω => δl ω * δm ω) P.μ := hδlδm_memLp.integrable le_rfl have hδmsq_int : Integrable (fun ω => δm ω * δm ω) P.μ := hδmsq_memLp.integrable le_rfl -- Integrability of every product term in the expansion. have hUδm_int : Integrable (fun ω => S.U ω * δm ω) P.μ := by rw [hδm_def]; exact hUΔm have hδlresid_int : Integrable (fun ω => δl ω * S.resid ω) P.μ := by rw [hδl_def]; exact hΔlV have hδmresid_int : Integrable (fun ω => δm ω * S.resid ω) P.μ := by rw [hδm_def]; simpa [mul_comm] using hVΔm -- Step 3 (cont.): expand the integral; only `∫δl·δm − θ·∫δm²` survives. -- Integrability of the grouped sub-expressions, stated in pointwise form so -- the `integral_add` / `integral_sub` rewrites match the integrand. have hA1 : Integrable (fun ω => S.U ω * S.resid ω - S.U ω * δm ω) P.μ := hUV.sub hUδm_int have hA2 : Integrable (fun ω => S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω) P.μ := hA1.sub hδlresid_int have hA3 : Integrable (fun ω => S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω + δl ω * δm ω) P.μ := hA2.add hδlδm_int have hB : Integrable (fun ω => S.θ * (δm ω * S.resid ω) - S.θ * (δm ω * δm ω)) P.μ := (hδmresid_int.const_mul S.θ).sub (hδmsq_int.const_mul S.θ) have hint_eq : ∫ ω, (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω) ∂P.μ = ∫ ω, δl ω * δm ω ∂P.μ - S.θ * ∫ ω, δm ω * δm ω ∂P.μ := by have hexp : (fun ω => (S.U ω - δl ω + S.θ * δm ω) * (S.resid ω - δm ω)) = fun ω => (S.U ω * S.resid ω - S.U ω * δm ω - δl ω * S.resid ω + δl ω * δm ω) + (S.θ * (δm ω * S.resid ω) - S.θ * (δm ω * δm ω)) := by funext ω; ring rw [hexp, integral_add hA3 hB, integral_add hA2 hδlδm_int, integral_sub hA1 hδlresid_int, integral_sub hUV hUδm_int, integral_sub (hδmresid_int.const_mul S.θ) (hδmsq_int.const_mul S.θ), integral_const_mul, integral_const_mul, h_U_resid, h_U_δm, h_δl_resid, h_δm_resid] ring rw [hint_eq] -- Step 4: the bound. Abbreviate the two L²(P_X) nuisance errors. set a : ℝ := (eLpNorm (fun x => η.lFn x - S.lVal x) 2 S.P_X).toReal with ha_def set b : ℝ := (eLpNorm (fun x => η.mFn x - S.mVal x) 2 S.P_X).toReal with hb_def have ha_nonneg : 0 ≤ a := ENNReal.toReal_nonneg have hb_nonneg : 0 ≤ b := ENNReal.toReal_nonneg -- The right-hand side is `(1 + |θ₀|)·(max a b)·(max a b)`. have hrhs1 : ((S.plrGeneralMoment.ρ₁ η S.η₀ : NNReal) : ℝ) = max a b := by -- `NNReal.coe_mk` no longer fires as a simp rewrite; it is still `rfl`. simp only [plrGeneralMoment, η₀, ← ha_def, ← hb_def] rfl have hrhs2 : ((S.plrGeneralMoment.ρ₂ η S.η₀ : NNReal) : ℝ) = max a b := by -- `NNReal.coe_mk` no longer fires as a simp rewrite; it is still `rfl`. simp only [plrGeneralMoment, η₀, ← ha_def, ← hb_def] rfl rw [hrhs1, hrhs2] -- L²(μ) ↔ L²(P_X) bridge for the two pulled-back nuisance errors. have hbridge_l : (eLpNorm δl 2 P.μ).toReal = a := by rw [ha_def, hδl_def, P_X, eLpNorm_map_measure hδl_meas.aestronglyMeasurable S.measurable_factualX.aemeasurable] rfl have hbridge_m : (eLpNorm δm 2 P.μ).toReal = b := by rw [hb_def, hδm_def, P_X, eLpNorm_map_measure hδm_meas.aestronglyMeasurable S.measurable_factualX.aemeasurable] rfl -- Cauchy–Schwarz on `δl·δm` and on `δm²` (over `μ`). have hCS_lm : ∫ ω, |δl ω * δm ω| ∂P.μ ≤ a * b := by have h := integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := P.μ) hδl hδm rwa [hbridge_l, hbridge_m] at h have hCS_mm : ∫ ω, |δm ω * δm ω| ∂P.μ ≤ b * b := by have h := integral_abs_mul_le_eLpNorm_mul_eLpNorm (ν := P.μ) hδm hδm rwa [hbridge_m] at h -- `∫ δm² = ∫ |δm·δm| ≥ 0`. have hδmsq_abs : (fun ω => δm ω * δm ω) = fun ω => |δm ω * δm ω| := by funext ω; rw [abs_of_nonneg (mul_self_nonneg (δm ω))] have hδmsq_nonneg : 0 ≤ ∫ ω, δm ω * δm ω ∂P.μ := integral_nonneg fun ω => mul_self_nonneg (δm ω) -- `|∫ δl·δm| ≤ ∫ |δl·δm| ≤ a·b`. have hbound_lm : |∫ ω, δl ω * δm ω ∂P.μ| ≤ a * b := (abs_integral_le_integral_abs).trans hCS_lm -- `∫ δm² ≤ b²`. have hbound_mm : ∫ ω, δm ω * δm ω ∂P.μ ≤ b * b := by calc ∫ ω, δm ω * δm ω ∂P.μ = ∫ ω, |δm ω * δm ω| ∂P.μ := by rw [hδmsq_abs] _ ≤ b * b := hCS_mm -- Triangle inequality and the `max` bound. have hθ : S.θ₀ = S.θ := rfl have ha_le : a ≤ max a b := le_max_left a b have hb_le : b ≤ max a b := le_max_right a b have hmax_nonneg : 0 ≤ max a b := le_trans ha_nonneg ha_le calc |∫ ω, δl ω * δm ω ∂P.μ - S.θ * ∫ ω, δm ω * δm ω ∂P.μ| ≤ |∫ ω, δl ω * δm ω ∂P.μ| + |S.θ * ∫ ω, δm ω * δm ω ∂P.μ| := abs_sub _ _ _ = |∫ ω, δl ω * δm ω ∂P.μ| + |S.θ| * (∫ ω, δm ω * δm ω ∂P.μ) := by rw [abs_mul, abs_of_nonneg hδmsq_nonneg] _ ≤ a * b + |S.θ| * (b * b) := add_le_add hbound_lm (mul_le_mul_of_nonneg_left hbound_mm (abs_nonneg _)) _ ≤ max a b * max a b + |S.θ| * (max a b * max a b) := by gcongr _ = (1 + |S.θ₀|) * max a b * max a b := by rw [hθ]; ring

theorem plr_score_diff_isLittleOp_one (S : PLRSystem P γ) (η_hat : ℕ → P.Ω → PLRNuisance γ) {Ca Cv Cm : ℝ} (hCa : 0 ≤ Ca) (hCv : 0 ≤ Cv) (hCm : 0 ≤ Cm) (hA_bdd : ∀ᵐ z ∂S.P_Z, |z.2.2 - S.lVal z.1 - S.θ₀ * (z.2.1 - S.mVal z.1)| ≤ Ca) (hv_bdd : ∀ᵐ z ∂S.P_Z, |z.2.1 - S.mVal z.1| ≤ Cv) (hΔm_bdd : ∀ n ω x, |S.mVal x - (η_hat n ω).mFn x| ≤ Cm) (hΔl_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X) (hΔm_memLp : ∀ n ω, MemLp (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X) (h_l_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) (h_m_rate : IsLittleOp (fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X).toReal) (fun _ => (1 : ℝ)) P.μ) : IsLittleOp (fun n ω => (eLpNorm (fun z => plrMomentFunctional (η_hat n ω) z S.θ₀ - plrMomentFunctional S.η₀ z S.θ₀) 2 S.P_Z).toReal) (fun _ => (1 : ℝ)) P.μ := by classical -- The two L²(P_X) rate functions and their sum. set rateL : ℕ → P.Ω → ℝ := fun n ω => (eLpNorm (fun x => (η_hat n ω).lFn x - S.lVal x) 2 S.P_X).toReal with hrateL set rateM : ℕ → P.Ω → ℝ := fun n ω => (eLpNorm (fun x => (η_hat n ω).mFn x - S.mVal x) 2 S.P_X).toReal with hrateM have hrateL_nonneg : ∀ n ω, 0 ≤ rateL n ω := fun _ _ => ENNReal.toReal_nonneg have hrateM_nonneg : ∀ n ω, 0 ≤ rateM n ω := fun _ _ => ENNReal.toReal_nonneg -- Sum of the two rates is `o_p(1)`. have hsum_rate : IsLittleOp (fun n ω => rateL n ω + rateM n ω) (fun _ => (1 : ℝ)) P.μ := IsLittleOp.add_one h_l_rate h_m_rate -- The combined constant. set Cconst : ℝ := Ca + Cv + Cm + |S.θ₀| * Cv + |S.θ₀| * Cm with hCconst have hCconst_pos : 0 < Cconst + 1 := by have : 0 ≤ Cconst := by have hθ : 0 ≤ |S.θ₀| := abs_nonneg _ have : 0 ≤ |S.θ₀| * Cv := mul_nonneg hθ hCv have : 0 ≤ |S.θ₀| * Cm := mul_nonneg hθ hCm positivity linarith -- Reduce to a constant multiple of the rate sum, then apply the per-`(n, ω)` -- quantitative bound. refine IsLittleOp.of_abs_le_const_mul_one (C := Cconst + 1) hCconst_pos hsum_rate ?_ intro n ω exact plr_score_diff_abs_le S η_hat n ω hCa hCv hCm Cconst rateL rateM hrateL hrateM hrateL_nonneg hrateM_nonneg hCconst hA_bdd hv_bdd hΔm_bdd hΔl_memLp hΔm_memLp