Stat.MEstimation

lemma finitePoissonObjective_exists_unique_max {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Fintype I] [Nonempty I] (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (hq : ∀ i, 0 < q i) (hm : ∀ i, 0 < m i) (hA : Injective A) : ∃! x : E, ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A x := by classical let B : E →ₗ[ℝ] (I → ℝ) := { toFun := fun x i => q i * min (m i) 1 * A x i map_add' := by intro x y funext i simp only [map_add, Pi.add_apply] ring map_smul' := by intro c x funext i simp only [map_smul, RingHom.id_apply, Pi.smul_apply, smul_eq_mul] ring } have hB : Injective B := by intro x y hxy apply hA funext i have hi := congrFun hxy i have hqi : q i ≠ 0 := ne_of_gt (hq i) have hci : min (m i) 1 ≠ 0 := ne_of_gt (lt_min (hm i) zero_lt_one) dsimp [B] at hi have hprod : 0 < q i * min (m i) 1 := mul_pos (hq i) (lt_min (hm i) zero_lt_one) nlinarith obtain ⟨K, hK, hanti⟩ := (LinearMap.injective_iff_antilipschitz B).mp hB let kappa : ℝ := K⁻¹ have hkappa : 0 < kappa := inv_pos.mpr hK have hBnorm (x : E) : kappa * ‖x‖ ≤ ‖B x‖ := by have h := hanti x 0 have hh := ENNReal.toReal_mono (by finiteness) h have h' : ‖x‖ ≤ (K : ℝ) * ‖B x‖ := by simpa [edist_dist, dist_eq_norm, ENNReal.toReal_mul] using hh change (K : ℝ)⁻¹ * ‖x‖ ≤ ‖B x‖ calc (K : ℝ)⁻¹ * ‖x‖ ≤ (K : ℝ)⁻¹ * ((K : ℝ) * ‖B x‖) := mul_le_mul_of_nonneg_left h' (inv_nonneg.mpr hK.le) _ = ((K : ℝ)⁻¹ * (K : ℝ)) * ‖B x‖ := by ring _ = ‖B x‖ := by rw [inv_mul_cancel₀ (show (K : ℝ) ≠ 0 by exact_mod_cast ne_of_gt hK)] simp let R : ℝ := max 0 (((∑ i, q i * ((m i + 1) ^ 2 / 2)) - finitePoissonObjective q m A 0) / kappa + 1) have hR0 : 0 ≤ R := by dsimp [R] exact le_max_left _ _ have hbound (x : E) : finitePoissonObjective q m A x ≤ (∑ i, q i * ((m i + 1) ^ 2 / 2)) - ‖B x‖ := by have hterm : ∀ i, q i * (m i * A x i - exp (A x i)) ≤ q i * ((m i + 1) ^ 2 / 2) - |B x i| := by intro i have hc := poissonCell_linear_coercive_bound (m i) (A x i) (hm i) have hqi := (hq i).le have habs : |B x i| = q i * min (m i) 1 * |A x i| := by dsimp [B] rw [abs_mul, abs_mul, abs_of_pos (hq i), abs_of_pos (lt_min (hm i) zero_lt_one)] rw [habs] nlinarith [mul_le_mul_of_nonneg_left hc hqi] calc finitePoissonObjective q m A x ≤ ∑ i, (q i * ((m i + 1) ^ 2 / 2) - |B x i|) := Finset.sum_le_sum fun i _ => hterm i _ = (∑ i, q i * ((m i + 1) ^ 2 / 2)) - ∑ i, |B x i| := by rw [Finset.sum_sub_distrib] _ ≤ (∑ i, q i * ((m i + 1) ^ 2 / 2)) - ‖B x‖ := by gcongr rw [Pi.norm_def] have hnn : (Finset.univ.sup fun b => ‖B x b‖₊) ≤ ∑ i, ‖B x i‖₊ := Finset.sup_le (fun i _ => Finset.single_le_sum (f := fun k => ‖B x k‖₊) (fun _ _ => zero_le) (Finset.mem_univ i)) have hr := NNReal.coe_le_coe.mpr hnn simpa only [NNReal.coe_sum, coe_nnnorm, Real.norm_eq_abs] using hr let ball : Set E := closedBall 0 R have : ProperSpace E := proper_real E obtain ⟨xstar, hxball, hxmax⟩ := (ProperSpace.isCompact_closedBall (0 : E) R).exists_isMaxOn ⟨0, by simp [Metric.mem_closedBall, hR0]⟩ (finitePoissonObjective_continuous q m A).continuousOn have hxglobal : ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A xstar := by intro y by_cases hy : y ∈ ball · exact hxmax hy · have hyR : R < ‖y‖ := by simpa [ball, Metric.mem_closedBall, dist_eq_norm, not_le] using hy have hcoarse := hbound y have hanti' := hBnorm y have hRlower : ((∑ i, q i * ((m i + 1) ^ 2 / 2)) - finitePoissonObjective q m A 0) / kappa + 1 ≤ R := le_max_right _ _ have hzero_mem : (0 : E) ∈ ball := by simp [ball, Metric.mem_closedBall, hR0] have hxzero := hxmax hzero_mem have hKne : kappa ≠ 0 := ne_of_gt hkappa have htail : (∑ i, q i * ((m i + 1) ^ 2 / 2)) - kappa * ‖y‖ < finitePoissonObjective q m A 0 := by apply (sub_lt_iff_lt_add).2 have := lt_of_le_of_lt hRlower hyR field_simp [hKne] at this ⊢ nlinarith exact (hcoarse.trans (sub_le_sub_left hanti' _)).trans (htail.le.trans hxzero) refine ⟨xstar, hxglobal, ?_⟩ intro y hymax by_contra hyne have hAy : A y ≠ A xstar := fun h => hyne (hA h) obtain ⟨i, hi⟩ : ∃ i, A y i ≠ A xstar i := by simpa only [Function.ne_iff] using hAy let mid : E := (1 / 2 : ℝ) • y + (1 / 2 : ℝ) • xstar have hstrictTerm : (q i * (m i * A y i - exp (A y i)) + q i * (m i * A xstar i - exp (A xstar i))) / 2 < q i * (m i * A mid i - exp (A mid i)) := by have hcell := poissonCell_strictConcave_midpoint (q i) (m i) (A y i) (A xstar i) (hq i) hi dsimp [mid] simp only [map_add, map_smul, Pi.add_apply, Pi.smul_apply, smul_eq_mul] have harg : (1 / 2 : ℝ) * A y i + (1 / 2 : ℝ) * A xstar i = (A y i + A xstar i) / 2 := by ring rw [harg] exact hcell have hmid : (finitePoissonObjective q m A y + finitePoissonObjective q m A xstar) / 2 < finitePoissonObjective q m A mid := by unfold finitePoissonObjective rw [← Finset.sum_add_distrib] simp_rw [div_eq_mul_inv] rw [Finset.sum_mul] apply Finset.sum_lt_sum · intro j hj by_cases hji : j = i · subst j exact (hstrictTerm.le) · have hconv := convexOn_exp.2 (Set.mem_univ (A y j)) (Set.mem_univ (A xstar j)) (show 0 ≤ (1 / 2 : ℝ) by norm_num) (show 0 ≤ (1 / 2 : ℝ) by norm_num) (by norm_num) simp only [smul_eq_mul] at hconv have hqconv := mul_le_mul_of_nonneg_left hconv (hq j).le dsimp [mid] simp only [map_add, map_smul, Pi.add_apply, Pi.smul_apply, smul_eq_mul] nlinarith · exact ⟨i, Finset.mem_univ i, hstrictTerm⟩ have hy_eq : finitePoissonObjective q m A y = finitePoissonObjective q m A xstar := by apply le_antisymm (hxglobal y) exact hymax xstar rw [hy_eq] at hmid have hmid' : finitePoissonObjective q m A xstar < finitePoissonObjective q m A mid := by simpa using hmid exact (not_lt_of_ge (hxglobal mid)) hmid'

theorem zEstimator_asymLinear_of_smoothScore (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : SmoothZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ reg.influence S (fun n => range n) := by let : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable rcases reg.deriv_lipschitz with ⟨δL, hδL, L, hLmeas, hLint, hLnonneg, hLbound⟩ -- The Lipschitz envelope is only valid near `θ₀`; consistency puts the estimator there -- with probability tending to one, and every bound below is asserted on that event. let G : ℕ → Set Ω := fun n => {ω | θn n ω ∈ closedBall θ₀ δL} have hGc : Tendsto (fun n => μ ((G n)ᶜ)) atTop (𝓝 0) := by refine (hConsistent δL hδL).congr fun n => ?_ congr 1 ext ω simp [G, Metric.mem_closedBall, dist_eq_norm, not_le] have hJleft : ∀ x : E, reg.jacobianInv (reg.jacobian x) = x := by have hJsurj : Surjective reg.jacobian := fun y => ⟨reg.jacobianInv y, by have h := congrArg (fun T : E →L[ℝ] E => T y) reg.jacobian_inverse simpa [SmoothZEstimatorRegularity.jacobian] using h⟩ have hJinj : Injective reg.jacobian := (LinearMap.injective_iff_surjective (f := (reg.jacobian : E →ₗ[ℝ] E))).mpr hJsurj intro x apply hJinj have h := congrArg (fun T : E →L[ℝ] E => T (reg.jacobian x)) reg.jacobian_inverse simpa [SmoothZEstimatorRegularity.jacobian] using h let U : ℕ → Ω → E := IsAsymLinearVec.normalizedSum S (ψ θ₀) (fun n => range n) have hU_def : ∀ n ω, U n ω = (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ θ₀ (S.Z i ω) := by intro n ω simp [U, IsAsymLinearVec.normalizedSum_def] let T : ℕ → Ω → E := fun n ω => (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω) let Jn : ℕ → Ω → (E →L[ℝ] E) := S.sampleMeanVec (reg.deriv θ₀) let A : ℕ → Ω → ℝ := fun n ω => ‖Jn n ω - reg.jacobian‖ let Lbar : ℕ → Ω → ℝ := S.sampleMean L let d : ℕ → Ω → ℝ := fun n ω => ‖θn n ω - θ₀‖ let C : ℕ → Ω → ℝ := fun n ω => A n ω + Lbar n ω * d n ω let Y : ℕ → Ω → ℝ := fun n ω => ‖Real.sqrt (n : ℝ) • (θn n ω - θ₀)‖ let M : ℕ → Ω → ℝ := fun n ω => ‖T n ω‖ let c : ℝ := ‖reg.jacobianInv‖ + 1 let Ac : ℕ → Ω → ℝ := fun n ω => c * C n ω let B : ℕ → Ω → ℝ := fun n ω => c * (‖U n ω‖ + M n ω) have hc : 0 < c := by dsimp [c] linarith [norm_nonneg reg.jacobianInv] have hUmeas : ∀ n, AEMeasurable (U n) μ := by intro n rw [show U n = fun ω => (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ θ₀ (S.Z i ω) by funext ω; exact hU_def n ω] exact ((Finset.measurable_sum _ (fun i _ => reg.score_meas.comp (S.meas i))).const_smul _).aemeasurable have hUclt : Modes.TendstoInLaw (fun _ : ℕ => μ) U atTop (gaussianLimit reg.score_meas reg.score_finite_var) := by exact S.clt_normalizedSum_vec reg.score_meas reg.score_finite_var reg.identification have hNormUclt := Modes.TendstoInLaw.map_continuous hUclt continuous_norm have hUbig : IsBigOp (fun n ω => ‖U n ω‖) (fun _ => (1 : ℝ)) μ := by let : IsProbabilityMeasure ((gaussianLimit reg.score_meas reg.score_finite_var).map norm) := Measure.isProbabilityMeasure_map continuous_norm.measurable.aemeasurable exact Modes.TendstoInLaw.tightness ((Tendsto_dist_iff _ _ _ (fun n => continuous_norm.measurable.comp_aemeasurable (hUmeas n))).2 hNormUclt) have hAlo : IsLittleOp A (fun _ => (1 : ℝ)) μ := by simpa [A, Jn, SmoothZEstimatorRegularity.jacobian] using S.sampleMeanVec_norm_sub_isLittleOp reg.deriv_at_target_meas reg.deriv_at_target_integrable have hLbig : IsBigOp Lbar (fun _ => (1 : ℝ)) μ := by simpa [Lbar] using Modes.TendstoInProbability.isBigOp_one (S.sampleMean_tendsto_inProb hLmeas hLint) have hdlo : IsLittleOp d (fun _ => (1 : ℝ)) μ := by apply (Modes.isLittleOpF_iff_strict (fun _ => μ) d atTop (fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2 intro ε hε simpa [d, abs_of_nonneg (norm_nonneg _)] using hConsistent ε hε have hLdlo : IsLittleOp (fun n ω => Lbar n ω * d n ω) (fun _ => (1 : ℝ)) μ := IsBigOp.mul_isLittleOp_one_isLittleOp hLbig hdlo have hClo : IsLittleOp C (fun _ => (1 : ℝ)) μ := by simpa [C] using hAlo.add_one hLdlo have hAclo : IsLittleOp Ac (fun _ => (1 : ℝ)) μ := by apply IsLittleOp.of_abs_le_const_mul_one hc hClo intro n ω simp [Ac, abs_mul, abs_of_pos hc] have hMlo : IsLittleOp M (fun _ => (1 : ℝ)) μ := by simpa [M, T] using hMoment have hMbig : IsBigOp M (fun _ => (1 : ℝ)) μ := isBigOp_one_of_isLittleOp_one hMlo have hBbig : IsBigOp B (fun _ => (1 : ℝ)) μ := by simpa [B] using IsBigOp.const_mul c (IsBigOp.add hUbig hMbig) have hA_nonneg : ∀ n ω, 0 ≤ Ac n ω := by intro n ω exact mul_nonneg hc.le <| add_nonneg (norm_nonneg _) (mul_nonneg (mul_nonneg (inv_nonneg.2 (Nat.cast_nonneg _)) (Finset.sum_nonneg fun i _ => hLnonneg _)) (norm_nonneg _)) have hB_nonneg : ∀ n ω, 0 ≤ B n ω := by intro n ω exact mul_nonneg hc.le (add_nonneg (norm_nonneg _) (norm_nonneg _)) have hY_nonneg : ∀ n ω, 0 ≤ Y n ω := fun n ω => norm_nonneg _ have hExpansion : ∀ n ω, ω ∈ G n → ‖T n ω - (U n ω + reg.jacobian (sqrt (n : ℝ) • (θn n ω - θ₀)))‖ ≤ C n ω * Y n ω := by intro n ω hmem by_cases hn : n = 0 · subst n rw [hU_def] simp [T, C, Y, Jn, A, Lbar, d, IIDSample.sampleMean, IIDSample.sampleMeanVec] · have hnpos : 0 < (n : ℝ) := by exact_mod_cast Nat.pos_of_ne_zero hn have hsqrt : 0 < sqrt (n : ℝ) := Real.sqrt_pos.2 hnpos let Δ : E := θn n ω - θ₀ let R : ℕ → E := fun i => ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω) - reg.deriv θ₀ (S.Z i ω) Δ have hR : ∀ i ∈ range n, ‖R i‖ ≤ L (S.Z i ω) * ‖Δ‖ ^ 2 := by intro i hi exact reg.score_taylor_remainder_le hLnonneg hLbound hmem (S.Z i ω) have hsum : (∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)) = (∑ i ∈ range n, ψ θ₀ (S.Z i ω)) + (∑ i ∈ range n, reg.deriv θ₀ (S.Z i ω) Δ) + ∑ i ∈ range n, R i := by rw [← Finset.sum_add_distrib, ← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi dsimp [R, Δ] abel have hcoef : sqrt (n : ℝ) * (n : ℝ)⁻¹ = (sqrt (n : ℝ))⁻¹ := by field_simp [hsqrt.ne'] rw [Real.sq_sqrt hnpos.le] have hJn : Jn n ω (sqrt (n : ℝ) • Δ) = (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, reg.deriv θ₀ (S.Z i ω) Δ := by simp only [Jn, IIDSample.sampleMeanVec, smul_apply, map_smul] rw [smul_smul, hcoef] simp have heq : T n ω - (U n ω + reg.jacobian (sqrt (n : ℝ) • Δ)) = (Jn n ω - reg.jacobian) (sqrt (n : ℝ) • Δ) + (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i := by dsimp [T] rw [hU_def, hsum, smul_add, smul_add, ← hJn] simp only [sub_apply] abel have hrem : ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ Lbar n ω * d n ω * Y n ω := by calc ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, ‖R i‖ := by rw [norm_smul_of_nonneg (inv_nonneg.2 hsqrt.le)] exact mul_le_mul_of_nonneg_left (norm_sum_le _ _) (inv_nonneg.2 hsqrt.le) _ ≤ (sqrt (n : ℝ))⁻¹ * ∑ i ∈ range n, (L (S.Z i ω) * ‖Δ‖ ^ 2) := by gcongr with i hi exact hR i hi _ = Lbar n ω * d n ω * Y n ω := by simp only [Lbar, IIDSample.sampleMean, d, Y, Δ] rw [← Finset.sum_mul] rw [norm_smul_of_nonneg hsqrt.le] field_simp [hsqrt.ne'] rw [Real.sq_sqrt hnpos.le] ring rw [show θn n ω - θ₀ = Δ by rfl, heq] calc ‖(Jn n ω - reg.jacobian) (sqrt (n : ℝ) • Δ) + (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ ≤ ‖(Jn n ω - reg.jacobian) (sqrt (n : ℝ) • Δ)‖ + ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, R i‖ := norm_add_le _ _ _ ≤ A n ω * Y n ω + Lbar n ω * d n ω * Y n ω := by exact add_le_add ((Jn n ω - reg.jacobian).le_opNorm _) hrem _ = C n ω * Y n ω := by ring have hRateBound : ∀ n ω, ω ∈ G n → Y n ω ≤ B n ω + Ac n ω * Y n ω := by intro n ω hmem let v : E := sqrt (n : ℝ) • (θn n ω - θ₀) let err : E := T n ω - (U n ω + reg.jacobian v) have hvid : v = reg.jacobianInv (T n ω - U n ω - err) := by have hinside : T n ω - U n ω - err = reg.jacobian v := by dsimp [err] abel rw [hinside, hJleft] calc Y n ω = ‖v‖ := rfl _ = ‖reg.jacobianInv (T n ω - U n ω - err)‖ := by rw [hvid] _ ≤ ‖reg.jacobianInv‖ * ‖T n ω - U n ω - err‖ := reg.jacobianInv.le_opNorm _ _ ≤ ‖reg.jacobianInv‖ * (M n ω + ‖U n ω‖ + ‖err‖) := by gcongr exact (norm_sub_le _ _).trans <| add_le_add_left (norm_sub_le _ _) _ _ ≤ c * (M n ω + ‖U n ω‖ + C n ω * Y n ω) := by gcongr · dsimp [c] linarith [norm_nonneg reg.jacobianInv] · exact hExpansion n ω hmem _ = B n ω + Ac n ω * Y n ω := by simp only [B, Ac] ring have hYbig : IsBigOp Y (fun _ => (1 : ℝ)) μ := isBigOp_of_absorption_on_event hAclo hBbig hA_nonneg hB_nonneg hY_nonneg hGc hRateBound refine ⟨reg.influenceFunction.mean_zero, reg.influenceFunction.finite_var, ?_⟩ · have hCYlo : IsLittleOp (fun n ω => C n ω * Y n ω) (fun _ => (1 : ℝ)) μ := by simpa using IsLittleOp.mul_isBigOp (Eventually.of_forall fun _ => zero_lt_one) (Eventually.of_forall fun _ => zero_lt_one) hClo hYbig have hMCYlo : IsLittleOp (fun n ω => M n ω + C n ω * Y n ω) (fun _ => (1 : ℝ)) μ := hMlo.add_one hCYlo apply IsLittleOp.of_abs_le_const_mul_one_on_event hc hMCYlo hGc intro n ω hmem let v : E := sqrt (n : ℝ) • (θn n ω - θ₀) let err : E := T n ω - (U n ω + reg.jacobian v) -- … truncated; follow the source link for the rest …

theorem zEstimator_tendsto_normal_of_smoothScore (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : SmoothZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨gaussianLimit reg.influence_measurable reg.influence_integrable_sq, inferInstance⟩) := by have hAL := zEstimator_asymLinear_of_smoothScore ψ θ₀ P reg S θn hConsistent hMoment exact hAL.tendsto_normal_vec_clt reg.influence_measurable (gaussianLimit reg.influence_measurable reg.influence_integrable_sq) (gaussianLimit_charFun reg.influence_measurable reg.influence_integrable_sq) hθn_meas

lemma tendsto_argmax_of_eventually_mem_compact {E : Type*} [PseudoMetricSpace E] [SecondCountableTopology E] (criterion : ℕ → E → ℝ) (limitCriterion : E → ℝ) (argmax : ℕ → E) (limitArgmax : E) (K : Set E) (hK : IsCompact K) (hLimitMem : limitArgmax ∈ K) (hLimitContinuous : ContinuousOn limitCriterion K) (hLimitMax : ∀ y ∈ K, limitCriterion y ≤ limitCriterion limitArgmax) (hUniform : TendstoUniformlyOn criterion limitCriterion atTop K) (hArgmaxMem : ∀ᶠ N in atTop, argmax N ∈ K) (hArgmax : ∀ᶠ N in atTop, ∀ y ∈ K, criterion N y ≤ criterion N (argmax N)) (hUnique : ∀ y ∈ K, limitCriterion y = limitCriterion limitArgmax → y = limitArgmax) : Tendsto argmax atTop (nhds limitArgmax) := by rw [Metric.tendsto_atTop] intro ε hε let S : Set E := K ∩ {y | ε ≤ dist y limitArgmax} have hScompact : IsCompact S := by apply hK.inter_right exact isClosed_le continuous_const (continuous_id.dist continuous_const) by_cases hSne : S.Nonempty · obtain ⟨z, hzS, hzmax⟩ := hScompact.exists_isMaxOn hSne (hLimitContinuous.mono inter_subset_left) have hzK : z ∈ K := hzS.1 have hzlt : limitCriterion z < limitCriterion limitArgmax := by refine lt_of_le_of_ne (hLimitMax z hzK) ?_ intro heq have hzl := hUnique z hzK heq subst z have : ε ≤ 0 := by simpa using hzS.2 exact (not_le_of_gt hε) this let d := (limitCriterion limitArgmax - limitCriterion z) / 3 have hd : 0 < d := div_pos (sub_pos.mpr hzlt) (by norm_num) have hU := (Metric.tendstoUniformlyOn_iff.mp hUniform d hd) have hevent : ∀ᶠ N in atTop, dist (argmax N) limitArgmax < ε := by filter_upwards [hU, hArgmaxMem, hArgmax] with N hUN hmem hmax by_contra hdist have hargS : argmax N ∈ S := ⟨hmem, le_of_not_gt hdist⟩ have hlimerr := hUN limitArgmax hLimitMem have hargerr := hUN (argmax N) hmem have hzbound := hzmax hargS change limitCriterion (argmax N) ≤ limitCriterion z at hzbound have hselected := hmax limitArgmax hLimitMem rw [Real.dist_eq] at hlimerr hargerr dsimp [d] at hd hlimerr hargerr linarith [abs_lt.mp hlimerr, abs_lt.mp hargerr] exact Filter.eventually_atTop.1 hevent · have hinside : ∀ y ∈ K, dist y limitArgmax < ε := by intro y hy by_contra h exact hSne ⟨y, hy, le_of_not_gt h⟩ have hevent : ∀ᶠ N in atTop, dist (argmax N) limitArgmax < ε := by filter_upwards [hArgmaxMem] with N hN exact hinside (argmax N) hN exact Filter.eventually_atTop.1 hevent

theorem localStochasticExpansion (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S θn) (hRate : IsBigOp (fun n ω => ‖θn n ω - θ₀‖) (fun n => (sqrt (n : ℝ))⁻¹) μ) : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)) - sqrt (n : ℝ) • reg.J₀ (θn n ω - θ₀)‖) (fun _ => (1 : ℝ)) μ := by let Sn : ℕ → Ω → E := fun n ω => (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)) let In : ℕ → Ω → E := fun n ω => sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P let Jn : ℕ → Ω → E := fun n ω => sqrt (n : ℝ) • reg.J₀ (θn n ω - θ₀) have hI : IsLittleOp (fun n ω => ‖Sn n ω - In n ω‖) (fun _ => (1 : ℝ)) μ := by simpa [Sn, In] using empiricalScoreDiff_isLittleOp_sqrt ψ θ₀ P S θn hConsistent hStochEquicont have hF : (fun θ => ∫ z, (ψ θ z - ψ θ₀ z) ∂P - reg.J₀ (θ - θ₀)) =o[𝓝 θ₀] fun θ => ‖θ - θ₀‖ := populationScoreDiff_eq_jacobian_plus_remainder ψ θ₀ P reg have hII : IsLittleOp (fun n ω => ‖In n ω - Jn n ω‖) (fun _ => (1 : ℝ)) μ := by apply (Modes.isLittleOpF_iff_strict (fun _ => μ) (fun n ω => ‖In n ω - Jn n ω‖) atTop (fun _ => (1 : ℝ)) (Eventually.of_forall fun _ => zero_lt_one)).2 intro ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ by_cases hδtop : δ = ⊤ · filter_upwards with n simp [hδtop] have hδpos : 0 < δ.toReal := ENNReal.toReal_pos (ne_of_gt hδ) hδtop let α : ℝ := δ.toReal / 8 have hαpos : 0 < α := by dsimp [α] linarith rcases hRate (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) with ⟨M0, _hM0pos, hM0event⟩ have hM0 := Filter.limsup_le_of_le (h := hM0event) let M : ℝ := max M0 1 have hMpos : 0 < M := by dsimp [M] exact lt_of_lt_of_le zero_lt_one (le_max_right M0 1) have hM0le : M0 ≤ M := by dsimp [M] exact le_max_left M0 1 let A : ℕ → Set Ω := fun n => {ω | M * (sqrt (n : ℝ))⁻¹ < |‖θn n ω - θ₀‖|} have hlimA : limsup (fun n => μ (A n)) atTop ≤ ofReal α := by refine le_trans (Filter.limsup_le_limsup (Eventually.of_forall ?_)) hM0 intro n apply measure_mono intro ω hω dsimp [A] at hω ⊢ have hrn_nonneg : 0 ≤ (sqrt (n : ℝ))⁻¹ := inv_nonneg.mpr (Real.sqrt_nonneg _) exact (lt_of_le_of_lt (mul_le_mul_of_nonneg_right hM0le hrn_nonneg) hω).le have halpha_two : ofReal α < ofReal (2 * α) := by rw [ENNReal.ofReal_lt_ofReal_iff] · linarith · linarith have hAevent := Filter.eventually_lt_of_limsup_lt (lt_of_le_of_lt hlimA halpha_two) let η : ℝ := ε / M have hηpos : 0 < η := by dsimp [η] exact div_pos hε hMpos have hderiv_event : ∀ᶠ θ in 𝓝 θ₀, ‖∫ z, (ψ θ z - ψ θ₀ z) ∂P - reg.J₀ (θ - θ₀)‖ ≤ η * ‖θ - θ₀‖ := by have hderiv_event0 := hF.def hηpos filter_upwards [hderiv_event0] with θ hθ simpa [Real.norm_eq_abs, abs_of_nonneg (norm_nonneg (θ - θ₀))] using hθ rcases Metric.eventually_nhds_iff.mp hderiv_event with ⟨ρ, hρpos, hρprop⟩ let B : ℕ → Set Ω := fun n => {ω | ρ ≤ ‖θn n ω - θ₀‖} have hConsistentHalf := hConsistent (ρ / 2) (by linarith) have hBsmall0 := (ENNReal.tendsto_nhds_zero.mp hConsistentHalf) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have hBevent : ∀ᶠ n in atTop, μ (B n) < ofReal (2 * α) := by filter_upwards [hBsmall0] with n hn exact lt_of_le_of_lt (le_trans (measure_mono (by intro ω hω dsimp [B] at hω have : ρ / 2 < ‖θn n ω - θ₀‖ := by linarith exact this)) hn) halpha_two let C : ℕ → Set Ω := fun n => {ω | ε < |‖In n ω - Jn n ω‖|} have hpoint : ∀ n, μ (C n) ≤ μ (A n) + μ (B n) := by intro n have hsubset : C n ⊆ A n ∪ B n := by intro ω hω by_contra hnot have hnotA : ¬ M * (sqrt (n : ℝ))⁻¹ < |‖θn n ω - θ₀‖| := by intro hx exact hnot (inl hx) have hnotB : ¬ ρ ≤ ‖θn n ω - θ₀‖ := by intro hx exact hnot (inr hx) have hθle : ‖θn n ω - θ₀‖ ≤ M * (sqrt (n : ℝ))⁻¹ := by have := le_of_not_gt hnotA simpa [abs_of_nonneg (norm_nonneg (θn n ω - θ₀))] using this have hnear : ‖θn n ω - θ₀‖ < ρ := lt_of_not_ge hnotB have hder := hρprop (by simpa [dist_eq_norm] using hnear) have hscaled_le : sqrt (n : ℝ) * ‖θn n ω - θ₀‖ ≤ M := by by_cases hn : n = 0 · simp [hn, hMpos.le] · have hnpos_nat : 0 < n := Nat.pos_of_ne_zero hn have hnpos : 0 < (n : ℝ) := by exact_mod_cast hnpos_nat have hsqrt_pos : 0 < sqrt (n : ℝ) := Real.sqrt_pos.mpr hnpos calc sqrt (n : ℝ) * ‖θn n ω - θ₀‖ ≤ sqrt (n : ℝ) * (M * (sqrt (n : ℝ))⁻¹) := mul_le_mul_of_nonneg_left hθle (Real.sqrt_nonneg _) _ = M := by field_simp [hsqrt_pos.ne'] have hRle : ‖In n ω - Jn n ω‖ ≤ ε := by calc ‖In n ω - Jn n ω‖ = ‖Real.sqrt (n : ℝ) • (∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P - reg.J₀ (θn n ω - θ₀))‖ := by simp [In, Jn, sub_eq_add_neg, smul_add, smul_neg] _ = sqrt (n : ℝ) * ‖∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P - reg.J₀ (θn n ω - θ₀)‖ := by rw [norm_smul, Real.norm_eq_abs, abs_of_nonneg (Real.sqrt_nonneg _)] _ ≤ sqrt (n : ℝ) * (η * ‖θn n ω - θ₀‖) := by exact mul_le_mul_of_nonneg_left hder (Real.sqrt_nonneg _) _ = η * (sqrt (n : ℝ) * ‖θn n ω - θ₀‖) := by ring _ ≤ η * M := mul_le_mul_of_nonneg_left hscaled_le (le_of_lt hηpos) _ = ε := by dsimp [η] field_simp [hMpos.ne'] have hω' : ε < ‖In n ω - Jn n ω‖ := by simpa [C, abs_of_nonneg (norm_nonneg (In n ω - Jn n ω))] using hω exact not_lt_of_ge hRle hω' calc μ (C n) ≤ μ (A n ∪ B n) := measure_mono hsubset _ ≤ μ (A n) + μ (B n) := MeasureTheory.measure_union_le (A n) (B n) have hfour_alpha_lt_delta : ofReal (4 * α) < δ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hδpos] · exact hδtop filter_upwards [hAevent, hBevent] with n hAn hBn exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |‖In n ω - Jn n ω‖|} = μ (C n) := by simp [C] _ ≤ μ (A n) + μ (B n) := hpoint n _ < ofReal (2 * α) + ofReal (2 * α) := ENNReal.add_lt_add hAn hBn _ = ofReal (4 * α) := by rw [← ENNReal.ofReal_add] · congr 1 ring · linarith · linarith _ < δ := hfour_alpha_lt_delta have hLittle_add_one : ∀ {Xn Yn : ℕ → Ω → ℝ}, IsLittleOp Xn (fun _ => (1 : ℝ)) μ → IsLittleOp Yn (fun _ => (1 : ℝ)) μ → IsLittleOp (fun n ω => Xn n ω + Yn n ω) (fun _ => (1 : ℝ)) μ := by intro Xn Yn hX hY exact IsLittleOp.add_one hX hY have hsum : IsLittleOp (fun n ω => ‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖) (fun _ => (1 : ℝ)) μ := hLittle_add_one hI hII have hmono_one : ∀ {Xn Yn : ℕ → Ω → ℝ}, IsLittleOp Yn (fun _ => (1 : ℝ)) μ → (∀ n ω, |Xn n ω| ≤ |Yn n ω|) → IsLittleOp Xn (fun _ => (1 : ℝ)) μ := by intro Xn Yn hY hbound ε hε rw [ENNReal.tendsto_nhds_zero] intro δ hδ have hYevent := (ENNReal.tendsto_nhds_zero.mp (hY ε hε)) δ hδ filter_upwards [hYevent] with n hn refine (measure_mono ?_).trans hn intro ω hω exact hω.trans (by simpa using hbound n ω) refine hmono_one hsum ?_ intro n ω have htri : ‖Sn n ω - Jn n ω‖ ≤ ‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖ := by calc ‖Sn n ω - Jn n ω‖ = ‖(Sn n ω - In n ω) + (In n ω - Jn n ω)‖ := by congr 1 abel _ ≤ ‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖ := norm_add_le _ _ have hsum_nonneg : 0 ≤ ‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖ := add_nonneg (norm_nonneg _) (norm_nonneg _) calc |‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)) - sqrt (n : ℝ) • reg.J₀ (θn n ω - θ₀)‖| = ‖Sn n ω - Jn n ω‖ := by simp [Sn, Jn] _ ≤ ‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖ := htri _ = |‖Sn n ω - In n ω‖ + ‖In n ω - Jn n ω‖| := by rw [abs_of_nonneg hsum_nonneg]

theorem zEstimator_asymLinear_of_extremum (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : WeakGlivenkoCantelli S m) (slack : ℕ → Ω → ℝ) (hSlack : Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)) (hApprox : ∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m θ₀ x ∂P) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S θn) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n) := zEstimator_asymLinear ψ θ₀ P reg S θn (consistent_lt_norm_of_le_dist θn θ₀ (mEstimator_consistent_of_glivenkoCantelli S m θ₀ θn hGC slack hSlack hApprox hSep)) hStochEquicont hMoment

theorem zEstimator_asymLinear_of_asymptoticEquicont (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n) := zEstimator_asymLinear ψ θ₀ P reg S θn hConsistent (stochEquicontAt_of_asymptoticEquicont ψ θ₀ S θn hAEC hConsistent) hMoment

theorem zEstimator_asymLinear_of_extremum_asymptoticEquicont (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (m : E → X → ℝ) (hGC : WeakGlivenkoCantelli S m) (slack : ℕ → Ω → ℝ) (hSlack : Modes.TendstoInProbability (fun _ : ℕ => μ) slack atTop (fun _ _ => 0)) (hApprox : ∀ n ω, S.sampleMean (m θ₀) n ω ≤ S.sampleMean (m (θn n ω)) n ω + slack n ω) (hSep : ∀ ε : ℝ, 0 < ε → ∃ η : ℝ, 0 < η ∧ ∀ θ : E, ε ≤ dist θ θ₀ → (∫ x, m θ x ∂P) + η ≤ ∫ x, m θ₀ x ∂P) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n) := have hcons := consistent_lt_norm_of_le_dist θn θ₀ (mEstimator_consistent_of_glivenkoCantelli S m θ₀ θn hGC slack hSlack hApprox hSep) zEstimator_asymLinear ψ θ₀ P reg S θn hcons (stochEquicontAt_of_asymptoticEquicont ψ θ₀ S θn hAEC hcons) hMoment

theorem finite_penalized_argmin_consistent [Fintype ι] [Nonempty ι] (empirical : ℕ → Ω → ι → ℝ) (population : ι → ℝ) (penalty : ℕ → ι → ℝ) (rank : ι → ℕ) (selector : ℕ → Ω → ι) (μ : Measure Ω) [IsProbabilityMeasure μ] (hcoord : ∀ i, Modes.TendstoInProbability (fun _ : ℕ => μ) (fun n ω => empirical n ω i) atTop (fun _ _ => population i)) (hgap : ∃ gap : ℝ, 0 < gap ∧ ∀ i ∈ populationMinimizers population, ∀ j ∉ populationMinimizers population, population i + gap ≤ population j) (hpenalty : ∀ i, Tendsto (fun n => penalty n i / (n : ℝ)) atTop (𝓝 0)) (hselect : ∀ (n : ℕ) (ω : Ω), IsRankedMinimizer rank (fun i => (n : ℝ) * empirical n ω i + penalty n i) (selector n ω)) (hmeas : ∀ n, MeasurableSet {ω | selector n ω ∈ populationMinimizers population}) : Tendsto (fun n => μ {ω | selector n ω ∈ populationMinimizers population}) atTop (𝓝 1) := by have hfailure := finite_penalized_argmin_failure_tendsto_zero empirical population penalty rank selector μ hcoord hgap hpenalty hselect have hsuccess_eq : ∀ n, μ {ω | selector n ω ∈ populationMinimizers population} = 1 - μ {ω | selector n ω ∉ populationMinimizers population} := by intro n let success : Set Ω := {ω | selector n ω ∈ populationMinimizers population} have hfailure_set : {ω | selector n ω ∉ populationMinimizers population} = successᶜ := by ext ω simp [success] have hsuccess_set : {ω | selector n ω ∈ populationMinimizers population} = ({ω | selector n ω ∉ populationMinimizers population} : Set Ω)ᶜ := by rw [hfailure_set, compl_compl] rw [hsuccess_set, measure_compl] · simp · simpa [hfailure_set, success] using (hmeas n).compl · exact measure_ne_top _ _ simpa only [hsuccess_eq, tsub_zero] using (ENNReal.Tendsto.sub tendsto_const_nhds hfailure (inl ENNReal.one_ne_top))

lemma finitePoissonObjective_argmax_tendsto {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [SecondCountableTopology E] [Fintype I] (qN mN : ℕ → I → ℝ) (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (argmax : ℕ → E) (limitArgmax : E) (hqpos : ∀ i, 0 < q i) (hmpos : ∀ i, 0 < m i) (hA : Injective A) (hq : ∀ i, Tendsto (fun N => qN N i) atTop (nhds (q i))) (hm : ∀ i, Tendsto (fun N => mN N i) atTop (nhds (m i))) (hArgmax : ∀ᶠ N in atTop, ∀ y, finitePoissonObjective (qN N) (mN N) A y ≤ finitePoissonObjective (qN N) (mN N) A (argmax N)) (hLimit : IsUniqueGlobalMax (finitePoissonObjective q m A) limitArgmax) : Tendsto argmax atTop (nhds limitArgmax) := by obtain ⟨K₀, hK₀, hmem⟩ := finitePoissonObjective_eventually_common_compact qN mN q m A argmax hqpos hmpos hA hq hm hArgmax let K : Set E := insert limitArgmax K₀ have hK : IsCompact K := hK₀.insert limitArgmax have hlimitmem : limitArgmax ∈ K := Set.mem_insert _ _ have hargmem : ∀ᶠ N in atTop, argmax N ∈ K := hmem.mono fun N hN => Set.mem_insert_of_mem _ hN apply tendsto_argmax_of_eventually_mem_compact (fun N => finitePoissonObjective (qN N) (mN N) A) (finitePoissonObjective q m A) argmax limitArgmax K hK hlimitmem · exact (finitePoissonObjective_continuous q m A).continuousOn · intro y hy exact hLimit.1 y · exact finitePoissonObjective_tendstoUniformlyOn qN mN q m A K hK hq hm · exact hargmem · exact hArgmax.mono fun N hN y hy => hN y · intro y hy heq exact hLimit.2 y heq

lemma finitePoissonObjective_argmax_continuousAt_mean {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Fintype I] [Nonempty I] (q : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (m₀ : I → ℝ) (hq : ∀ i, 0 < q i) (hm₀ : ∀ i, 0 < m₀ i) (hA : Injective A) : ContinuousAt (fun m : I → ℝ => maximizerOrZero (finitePoissonObjective q m A)) m₀ := by classical rw [ContinuousAt, Filter.tendsto_iff_seq_tendsto] intro mN hmN have hm : ∀ i, Tendsto (fun N => mN N i) atTop (nhds (m₀ i)) := tendsto_pi_nhds.mp hmN have hmpos : ∀ᶠ N in atTop, ∀ i, 0 < mN N i := by rw [Filter.eventually_all] intro i exact (tendsto_order.1 (hm i)).1 0 (hm₀ i) have hmax : ∀ᶠ N in atTop, ∀ y, finitePoissonObjective q (mN N) A y ≤ finitePoissonObjective q (mN N) A (maximizerOrZero (finitePoissonObjective q (mN N) A)) := by filter_upwards [hmpos] with N hpos exact (uniqueGlobalMax_maximizerOrZero _ (finitePoissonObjective_exists_unique_max q (mN N) A hq hpos hA)).1 have hlimit : IsUniqueGlobalMax (finitePoissonObjective q m₀ A) (maximizerOrZero (finitePoissonObjective q m₀ A)) := uniqueGlobalMax_maximizerOrZero _ (finitePoissonObjective_exists_unique_max q m₀ A hq hm₀ hA) exact finitePoissonObjective_argmax_tendsto (fun _ => q) mN q m₀ A (fun N => maximizerOrZero (finitePoissonObjective q (mN N) A)) (maximizerOrZero (finitePoissonObjective q m₀ A)) hq hm₀ hA (fun i => tendsto_const_nhds) hm hmax hlimit

lemma finitePoissonObjective_expCell_argmax_snd_hasDerivAt {U I : Type*} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [Fintype I] [DecidableEq I] [Nonempty I] (q m : I → ℝ) (A : (U × ℝ) →ₗ[ℝ] (I → ℝ)) (j : I) (B x₀ betaDot : ℝ) (hq : ∀ i, 0 < q i) (hm : ∀ i, 0 < m i) (hB : 0 < B) (hA : Injective A) (hbeta : ∀ v : U × ℝ, (∀ d : U × ℝ, ∑ i, q i * A d i * ((if i = j then B * exp x₀ else 0) - exp (A (maximizerOrZero (finitePoissonObjective q (expCellUpdatedMean m j B x₀) A)) i) * A v i) = 0) → v.2 = betaDot) : HasDerivAt (fun x => (maximizerOrZero (finitePoissonObjective q (expCellUpdatedMean m j B x) A)).2) betaDot x₀ := by classical let E := U × ℝ let b := Basis.ofVectorSpace ℝ E let theta₀ : E := maximizerOrZero (finitePoissonObjective q (expCellUpdatedMean m j B x₀) A) let S : ℝ × E → (Basis.ofVectorSpaceIndex ℝ E → ℝ) := fun p k ↦ ∑ i, q i * A (b k) i * ((if i = j then B * exp p.1 else m i) - exp (A p.2 i)) let D : (ℝ × E) →L[ℝ] (Basis.ofVectorSpaceIndex ℝ E → ℝ) := ContinuousLinearMap.pi fun k ↦ ∑ i, (q i * A (b k) i) • (((if i = j then B * exp x₀ else 0) • ContinuousLinearMap.fst ℝ ℝ E) - (exp (A theta₀ i)) • ((ContinuousLinearMap.proj i).comp (A.toContinuousLinearMap.comp (ContinuousLinearMap.snd ℝ ℝ E)))) have hSD : HasFDerivAt S D (x₀, theta₀) := by dsimp [S, D] rw [hasFDerivAt_pi] intro k apply HasFDerivAt.fun_sum intro i hi by_cases hij : i = j · subst i have hleft := (hasFDerivAt_fst (p := (x₀, theta₀))).exp.const_mul B have hright := (((ContinuousLinearMap.proj j).comp (A.toContinuousLinearMap.comp (ContinuousLinearMap.snd ℝ ℝ E))).hasFDerivAt (x := (x₀, theta₀))).exp convert (hleft.fun_sub hright).const_mul (q j * A (b k) j) using 1 <;> first | rfl | (ext z <;> simp) · have hleft : HasFDerivAt (fun _p : ℝ × E ↦ m i) (0 : (ℝ × E) →L[ℝ] ℝ) (x₀, theta₀) := hasFDerivAt_const (x := (x₀, theta₀)) (c := m i) have hright := (((ContinuousLinearMap.proj i).comp (A.toContinuousLinearMap.comp (ContinuousLinearMap.snd ℝ ℝ E))).hasFDerivAt (x := (x₀, theta₀))).exp convert (hleft.fun_sub hright).const_mul (q i * A (b k) i) using 1 <;> first | rfl | (ext z <;> simp [hij]) let L : E →L[ℝ] (Basis.ofVectorSpaceIndex ℝ E → ℝ) := D.comp (ContinuousLinearMap.inr ℝ ℝ E) have hL_inj : Injective L := by intro v w hvw have hzero : L (v - w) = 0 := by rw [map_sub, hvw, sub_self] let G : E →ₗ[ℝ] ℝ := { toFun := fun d ↦ ∑ i, q i * exp (A theta₀ i) * A d i * A (v - w) i map_add' := by intro d e simp only [map_add, Pi.add_apply] rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi ring map_smul' := by intro c d simp only [map_smul, RingHom.id_apply, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi ring } have hG : G = 0 := by apply b.ext intro k have hk : L (v - w) k = 0 := by simpa using congrFun hzero k norm_num [L, D] at hk have hk' : -(∑ i, q i * A (b k) i * (exp (A theta₀ i) * A (v - w) i)) = 0 := by convert hk using 1 rw [← Finset.sum_neg_distrib] apply Finset.sum_congr rfl intro i hi by_cases hij : i = j <;> simp [hij] dsimp [G] have hk'' := neg_eq_zero.mp hk' convert hk'' using 1 apply Finset.sum_congr rfl intro i hi ring have hsum : ∑ i, q i * exp (A theta₀ i) * (A (v - w) i) ^ 2 = 0 := by have hu := LinearMap.congr_fun hG (v - w) change ∑ i, q i * exp (A theta₀ i) * A (v - w) i * A (v - w) i = 0 at hu convert hu using 1 apply Finset.sum_congr rfl intro i hi ring have hAv : A (v - w) = 0 := by funext i have hi := (Finset.sum_eq_zero_iff_of_nonneg (fun i _ ↦ mul_nonneg (mul_nonneg (le_of_lt (hq i)) (le_of_lt (Real.exp_pos _))) (sq_nonneg _))).mp hsum i (Finset.mem_univ i) have hpos : 0 < q i * exp (A theta₀ i) := mul_pos (hq i) (Real.exp_pos _) exact sq_eq_zero_iff.mp ((mul_eq_zero.mp hi).resolve_left (ne_of_gt hpos)) apply sub_eq_zero.mp apply hA simpa using hAv have hdim : finrank ℝ E = finrank ℝ (Basis.ofVectorSpaceIndex ℝ E → ℝ) := by simpa [Module.finrank_pi_fintype, finrank_self] using Module.finrank_eq_card_basis b have hL_bij : Bijective L := ⟨hL_inj, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hdim).mp hL_inj⟩ have hScont : ContDiffAt ℝ 1 S (x₀, theta₀) := by dsimp [S] rw [contDiffAt_pi] intro k apply ContDiffAt.sum intro i hi have heta : ContDiffAt ℝ 1 (fun p : ℝ × E ↦ A p.2 i) (x₀, theta₀) := ((ContinuousLinearMap.proj i).comp (A.toContinuousLinearMap.comp (ContinuousLinearMap.snd ℝ ℝ E))).contDiff.contDiffAt by_cases hij : i = j · subst i have hBexp : ContDiffAt ℝ 1 (fun p : ℝ × E ↦ B * exp p.1) (x₀, theta₀) := contDiffAt_const.mul contDiffAt_fst.exp simpa using contDiffAt_const.mul (hBexp.sub heta.exp) · have hmconst : ContDiffAt ℝ 1 (fun _p : ℝ × E ↦ m i) (x₀, theta₀) := contDiffAt_const simpa [hij] using contDiffAt_const.mul (hmconst.sub heta.exp) have hpn : (1 : WithTop ℕ∞) ≠ 0 := by norm_num have hfd : fderiv ℝ S (x₀, theta₀) = D := hSD.fderiv have hinv : ((fderiv ℝ S (x₀, theta₀)).comp (ContinuousLinearMap.inr ℝ ℝ E)).IsInvertible := by rw [hfd] exact ⟨ContinuousLinearEquiv.ofBijective L (LinearMap.ker_eq_bot.mpr hL_bij.1) (LinearMap.range_eq_top.mpr hL_bij.2), ContinuousLinearEquiv.coe_ofBijective _ _ _⟩ let phi : ℝ → E := hScont.implicitFunction hpn hinv have hmexp (x : ℝ) : ∀ i, 0 < expCellUpdatedMean m j B x i := by intro i simp only [expCellUpdatedMean, Function.update_apply] split · exact mul_pos hB (Real.exp_pos _) · exact hm i have hmax0 : ∀ y, finitePoissonObjective q (expCellUpdatedMean m j B x₀) A y ≤ finitePoissonObjective q (expCellUpdatedMean m j B x₀) A theta₀ := by obtain ⟨xstar, hxstar, huniq⟩ := finitePoissonObjective_exists_unique_max q (expCellUpdatedMean m j B x₀) A hq (hmexp x₀) hA have hex : ∃ x, ∀ y, finitePoissonObjective q (expCellUpdatedMean m j B x₀) A y ≤ finitePoissonObjective q (expCellUpdatedMean m j B x₀) A x := ⟨xstar, hxstar⟩ dsimp [theta₀, maximizerOrZero] rw [dif_pos hex] exact Classical.choose_spec hex have hS0 : S (x₀, theta₀) = 0 := by funext k have hs := finitePoissonObjective_score q (expCellUpdatedMean m j B x₀) A theta₀ (b k) hmax0 simpa [S, expCellUpdatedMean, Function.update_apply] using hs have hphi0 : phi x₀ = theta₀ := hScont.implicitFunction_apply_self hpn hinv have hphi_score : ∀ᶠ x in nhds x₀, S (x, phi x) = 0 := by filter_upwards [hScont.eventually_apply_implicitFunction hpn hinv] with x hx change S (x, phi x) = 0 simpa only [hS0] using hx have hselected_phi : (fun x ↦ maximizerOrZero (finitePoissonObjective q (expCellUpdatedMean m j B x) A)) =ᶠ[nhds x₀] phi := by filter_upwards [hphi_score] with x hx let Gx : E →ₗ[ℝ] ℝ := { toFun := fun d ↦ ∑ i, q i * A d i * (expCellUpdatedMean m j B x i - exp (A (phi x) i)) map_add' := by intro d e simp only [map_add, Pi.add_apply] rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro i hi ring map_smul' := by intro c d simp only [map_smul, RingHom.id_apply, Pi.smul_apply, smul_eq_mul] rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi ring } have hGx : Gx = 0 := by apply b.ext intro k have hk := congrFun hx k simpa [Gx, S, expCellUpdatedMean, Function.update_apply] using hk have hscore : ∀ d : E, ∑ i, q i * A d i * (expCellUpdatedMean m j B x i - exp (A (phi x) i)) = 0 := by intro d exact LinearMap.congr_fun hGx d have hphimax := finitePoissonObjective_isMax_of_score q (expCellUpdatedMean m j B x) A (phi x) (fun i ↦ (hq i).le) hscore obtain ⟨xstar, hxstar, huniq⟩ := finitePoissonObjective_exists_unique_max q (expCellUpdatedMean m j B x) A hq (hmexp x) hA have hex : ∃ z, ∀ y, finitePoissonObjective q (expCellUpdatedMean m j B x) A y ≤ finitePoissonObjective q (expCellUpdatedMean m j B x) A z := ⟨xstar, hxstar⟩ rw [maximizerOrZero, dif_pos hex] have hchoose : choose hex = xstar := huniq _ (Classical.choose_spec hex) have hphi : phi x = xstar := huniq _ hphimax exact hchoose.trans hphi.symm have hphidiff : DifferentiableAt ℝ phi x₀ := by exact (hScont.contDiffAt_implicitFunction hpn hinv).differentiableAt (by norm_num) let v : E := fderiv ℝ phi x₀ 1 let P : ℝ →L[ℝ] (ℝ × E) := (id ℝ ℝ).prod (fderiv ℝ phi x₀) have hpair : HasFDerivAt (fun x ↦ (x, phi x)) P x₀ := by exact (hasFDerivAt_id x₀).prodMk hphidiff.hasFDerivAt have hcomp : HasFDerivAt (fun x ↦ S (x, phi x)) (D.comp P) x₀ := by have hSD' : HasFDerivAt S D (x₀, phi x₀) := by simpa [hphi0] using hSD exact hSD'.comp x₀ hpair have hcompzero : HasFDerivAt (fun x ↦ S (x, phi x)) (0 : ℝ →L[ℝ] (Basis.ofVectorSpaceIndex ℝ E → ℝ)) x₀ := by apply (hasFDerivAt_const (x := x₀) (c := (0 : Basis.ofVectorSpaceIndex ℝ E → ℝ))).congr_of_eventuallyEq exact hphi_score have hDPzero : D.comp P = 0 := hcomp.unique hcompzero have hvscore_basis (k : Basis.ofVectorSpaceIndex ℝ E) : ∑ i, q i * A (b k) i * ((if i = j then B * exp x₀ else 0) - exp (A theta₀ i) * A v i) = 0 := by have hk := congrFun (congrArg (fun F ↦ F 1) hDPzero) k dsimp [D, P, v] at hk rw [ContinuousLinearMap.sum_apply] at hk simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.sub_apply, ContinuousLinearMap.comp_apply] at hk simpa [mul_sub] using hk -- … truncated; follow the source link for the rest …

lemma finitePoissonObjective_snd_sign_of_nuisance_score {U I : Type*} [NormedAddCommGroup U] [NormedSpace ℝ U] [FiniteDimensional ℝ U] [Fintype I] [Nonempty I] (q m : I → ℝ) (A : (U × ℝ) →ₗ[ℝ] (I → ℝ)) (u₀ : U) (hq : ∀ i, 0 < q i) (hm : ∀ i, 0 < m i) (hA : Injective A) (hNuisance : ∀ u : U, ∑ i, q i * A (u, 0) i * (m i - exp (A (u₀, 0) i)) = 0) : let beta := (maximizerOrZero (finitePoissonObjective q m A)).2 let scalarScore := ∑ i, q i * A (0, 1) i * (m i - exp (A (u₀, 0) i)) (beta < 0 ↔ scalarScore < 0) ∧ (beta = 0 ↔ scalarScore = 0) ∧ (0 < beta ↔ 0 < scalarScore) := by classical dsimp only let xstar : U × ℝ := maximizerOrZero (finitePoissonObjective q m A) let xzero : U × ℝ := (u₀, 0) let v : U × ℝ := xstar - xzero let scalarScore : ℝ := ∑ i, q i * A (0, 1) i * (m i - exp (A xzero i)) have hunique := finitePoissonObjective_exists_unique_max q m A hq hm hA obtain ⟨x, hxmax, hxunique⟩ := hunique have hexists : ∃ x, ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A x := ⟨x, hxmax⟩ have hxstar_eq : xstar = x := by dsimp [xstar, maximizerOrZero] rw [dif_pos hexists] exact hxunique _ (Classical.choose_spec hexists) have hxstar : ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A xstar := by rw [hxstar_eq] exact hxmax have hstarScore (d : U × ℝ) : ∑ i, q i * A d i * (m i - exp (A xstar i)) = 0 := finitePoissonObjective_score q m A xstar d hxstar have hxstar_add : xstar = xzero + v := by simp [v] have hzeroScore (d : U × ℝ) : (∑ i, q i * A d i * (m i - exp (A xzero i))) = d.2 * scalarScore := by have hd : d = (d.1, 0) + d.2 • (0, (1 : ℝ)) := by ext <;> simp have hAd (i : I) : A d i = A (d.1, 0) i + d.2 * A (0, 1) i := by calc A d i = A ((d.1, 0) + d.2 • (0, (1 : ℝ))) i := congrArg (fun z => A z i) hd _ = _ := by rw [map_add, map_smul] simp only [Pi.add_apply, Pi.smul_apply, smul_eq_mul] calc _ = ∑ i, (q i * A (d.1, 0) i * (m i - exp (A xzero i)) + d.2 * (q i * A (0, 1) i * (m i - exp (A xzero i)))) := by apply Finset.sum_congr rfl intro i _ rw [hAd] ring _ = (∑ i, q i * A (d.1, 0) i * (m i - exp (A xzero i))) + d.2 * ∑ i, q i * A (0, 1) i * (m i - exp (A xzero i)) := by rw [Finset.sum_add_distrib, Finset.mul_sum] _ = d.2 * scalarScore := by rw [show (∑ i, q i * A (d.1, 0) i * (m i - exp (A xzero i))) = 0 by simpa [xzero] using hNuisance d.1] simp [scalarScore] have hvsecond : v.2 = xstar.2 := by simp [v, xzero] have hstrict (hv : v ≠ 0) : 0 < xstar.2 * scalarScore := by have hAv : A v ≠ 0 := fun hav => hv (hA (by simpa using hav)) obtain ⟨i, hi⟩ : ∃ i, A v i ≠ 0 := by simpa only [Function.ne_iff, Pi.zero_apply] using hAv have harg (j : I) : A xstar j = A xzero j + A v j := by rw [hxstar_add, map_add] rfl have hnonneg (j : I) : 0 ≤ q j * A v j * (exp (A xstar j) - exp (A xzero j)) := by have hqj := (hq j).le by_cases hav : 0 ≤ A v j · have he : exp (A xzero j) ≤ exp (A xstar j) := by apply Real.exp_le_exp.mpr rw [harg] linarith exact mul_nonneg (mul_nonneg hqj hav) (sub_nonneg.mpr he) · have hav' : A v j ≤ 0 := le_of_not_ge hav have he : exp (A xstar j) ≤ exp (A xzero j) := by apply Real.exp_le_exp.mpr rw [harg] linarith have : exp (A xstar j) - exp (A xzero j) ≤ 0 := sub_nonpos.mpr he exact mul_nonneg_of_nonpos_of_nonpos (mul_nonpos_of_nonneg_of_nonpos hqj hav') this have hposi : 0 < q i * A v i * (exp (A xstar i) - exp (A xzero i)) := by rcases lt_or_gt_of_ne hi with hav | hav · have he : exp (A xstar i) < exp (A xzero i) := by apply Real.exp_lt_exp.mpr rw [harg] linarith have hdiff : exp (A xstar i) - exp (A xzero i) < 0 := sub_neg.mpr he exact mul_pos_of_neg_of_neg (mul_neg_of_pos_of_neg (hq i) hav) hdiff · have he : exp (A xzero i) < exp (A xstar i) := by apply Real.exp_lt_exp.mpr rw [harg] linarith exact mul_pos (mul_pos (hq i) hav) (sub_pos.mpr he) have hsumpos : 0 < ∑ j, q j * A v j * (exp (A xstar j) - exp (A xzero j)) := by apply Finset.sum_pos' · intro j _ exact hnonneg j · exact ⟨i, Finset.mem_univ i, hposi⟩ have hdecomp : (∑ j, q j * A v j * (m j - exp (A xzero j))) = (∑ j, q j * A v j * (m j - exp (A xstar j))) + ∑ j, q j * A v j * (exp (A xstar j) - exp (A xzero j)) := by rw [← Finset.sum_add_distrib] apply Finset.sum_congr rfl intro j _ ring rw [hzeroScore v, hvsecond, hstarScore v, zero_add] at hdecomp rw [hdecomp] exact hsumpos have hzero : xstar.2 = 0 ↔ scalarScore = 0 := by constructor · intro hb by_contra hs have hv : v = 0 := by by_contra hv have := hstrict hv rw [hb, zero_mul] at this exact (lt_irrefl 0) this have hscalar := hstarScore (0, 1) rw [show xstar = xzero by simpa [v] using congrArg (fun z => z + xzero) hv] at hscalar exact hs (by simpa [scalarScore] using hscalar) · intro hs have hzeroScore' (d : U × ℝ) : ∑ i, q i * A d i * (m i - exp (A xzero i)) = 0 := by rw [hzeroScore d, hs, mul_zero] have hxzero : ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A xzero := finitePoissonObjective_isMax_of_score q m A xzero (fun i => (hq i).le) hzeroScore' have hxzero_eq : xzero = x := hxunique xzero hxzero rw [hxstar_eq, ← hxzero_eq] have hneg : xstar.2 < 0 ↔ scalarScore < 0 := by constructor · intro hb have hv : v ≠ 0 := by intro hv have := congrArg snd hv simp [v, xzero] at this linarith have hp := hstrict hv nlinarith · intro hs have hb : xstar.2 ≠ 0 := fun hb => hs.ne (hzero.mp hb) have hv : v ≠ 0 := by intro hv have hsnd : xstar.2 = 0 := by simpa [v, xzero] using congrArg snd hv exact hb hsnd have hp := hstrict hv nlinarith have hpos : 0 < xstar.2 ↔ 0 < scalarScore := by constructor · intro hb have hv : v ≠ 0 := by intro hv have := congrArg snd hv simp [v, xzero] at this linarith have hp := hstrict hv nlinarith · intro hs have hb : xstar.2 ≠ 0 := fun hb => hs.ne' (hzero.mp hb) have hv : v ≠ 0 := by intro hv have hsnd : xstar.2 = 0 := by simpa [v, xzero] using congrArg snd hv exact hb hsnd have hp := hstrict hv nlinarith simpa [xstar, xzero, scalarScore] using intro hneg (intro hzero hpos)

theorem logLinearScoreDeriv_lipschitz_on_ball (z : ℝ × ℝ) (θ₀ : ℝ) {δ : ℝ} {θ : ℝ} (hθ : θ ∈ closedBall θ₀ δ) {θ' : ℝ} (hθ' : θ' ∈ closedBall θ₀ δ) : |logLinearScoreDeriv θ z - logLinearScoreDeriv θ' z| ≤ (|z.1| ^ 3 * exp ((|θ₀| + δ) * |z.1|)) * |θ - θ'| := by -- Every parameter in the ball has modulus at most `|θ₀| + δ`. have hball : ∀ s ∈ closedBall θ₀ δ, |s| ≤ |θ₀| + δ := by intro s hs have hs' : |s - θ₀| ≤ δ := by simpa [Real.dist_eq] using Metric.mem_closedBall.mp hs calc |s| = |θ₀ + (s - θ₀)| := by ring_nf _ ≤ |θ₀| + |s - θ₀| := abs_add_le _ _ _ ≤ |θ₀| + δ := by linarith have hsub : uIcc θ' θ ⊆ closedBall θ₀ δ := (convex_closedBall θ₀ δ).ordConnected.uIcc_subset hθ' hθ set f : ℝ → ℝ := fun s => exp (s * z.1) with hf have hderiv : ∀ s ∈ uIcc θ' θ, HasDerivWithinAt f (exp (s * z.1) * z.1) (uIcc θ' θ) s := by intro s _ have : HasDerivAt f (exp (s * z.1) * z.1) s := by simpa [hf] using ((hasDerivAt_id s).mul_const z.1).exp exact this.hasDerivWithinAt have hbound : ∀ s ∈ uIcc θ' θ, ‖Real.exp (s * z.1) * z.1‖ ≤ exp ((|θ₀| + δ) * |z.1|) * |z.1| := by intro s hs have hle : s * z.1 ≤ (|θ₀| + δ) * |z.1| := by refine le_trans (le_abs_self _) ?_ rw [abs_mul] exact mul_le_mul_of_nonneg_right (hball s (hsub hs)) (abs_nonneg _) have hexp : exp (s * z.1) ≤ exp ((|θ₀| + δ) * |z.1|) := Real.exp_le_exp.2 hle calc ‖Real.exp (s * z.1) * z.1‖ = exp (s * z.1) * |z.1| := by rw [Real.norm_eq_abs, abs_mul, abs_of_pos (Real.exp_pos _)] _ ≤ exp ((|θ₀| + δ) * |z.1|) * |z.1| := mul_le_mul_of_nonneg_right hexp (abs_nonneg _) have hmv := (convex_uIcc θ' θ).norm_image_sub_le_of_norm_hasDerivWithin_le hderiv hbound left_mem_uIcc right_mem_uIcc have hstep : |f θ - f θ'| ≤ exp ((|θ₀| + δ) * |z.1|) * |z.1| * |θ - θ'| := by simpa [Real.norm_eq_abs] using hmv -- The derivative differs from `f` by the factor `x²`. have hfactor : |logLinearScoreDeriv θ z - logLinearScoreDeriv θ' z| = |f θ - f θ'| * z.1 ^ 2 := by simp only [logLinearScoreDeriv, hf] rw [show -(exp (θ * z.1) * z.1 ^ 2) - -(exp (θ' * z.1) * z.1 ^ 2) = -((exp (θ * z.1) - exp (θ' * z.1)) * z.1 ^ 2) by ring] rw [abs_neg, abs_mul, abs_of_nonneg (sq_nonneg z.1)] rw [hfactor] calc |f θ - f θ'| * z.1 ^ 2 ≤ (exp ((|θ₀| + δ) * |z.1|) * |z.1| * |θ - θ'|) * z.1 ^ 2 := mul_le_mul_of_nonneg_right hstep (sq_nonneg _) _ = (|z.1| ^ 3 * exp ((|θ₀| + δ) * |z.1|)) * |θ - θ'| := by rw [show z.1 ^ 2 = |z.1| ^ 2 from (sq_abs z.1).symm] ring

theorem logLinearScoreDeriv_not_globally_lipschitz : ¬ ∃ L : ℝ, ∀ θ θ' : ℝ, |logLinearScoreDeriv θ ((1 : ℝ), (1 : ℝ)) - logLinearScoreDeriv θ' ((1 : ℝ), (1 : ℝ))| ≤ L * |θ - θ'| := by rintro ⟨L, hL⟩ have hd : ∀ t : ℝ, logLinearScoreDeriv t ((1 : ℝ), (1 : ℝ)) = -exp t := by intro t simp [logLinearScoreDeriv] -- Comparing `θ` with `θ + 1` forces `exp θ (e - 1) ≤ L` for every `θ`. have key : ∀ θ : ℝ, exp θ * (exp 1 - 1) ≤ L := by intro θ have h := hL (θ + 1) θ rw [hd, hd] at h have hlt : exp θ < exp (θ + 1) := Real.exp_lt_exp.2 (by linarith) have habs : |(-exp (θ + 1)) - (-exp θ)| = exp (θ + 1) - exp θ := by rw [show (-exp (θ + 1)) - (-exp θ) = -(exp (θ + 1) - exp θ) by ring, abs_neg, abs_of_pos (by linarith)] rw [habs, show |θ + 1 - θ| = 1 by norm_num, mul_one, Real.exp_add] at h nlinarith [Real.exp_pos θ] -- But `exp` is unbounded above. have he : (0 : ℝ) < exp 1 - 1 := by have := Real.add_one_le_exp (1 : ℝ) linarith -- `x + 1 ≤ exp x` already outruns any bound, no logarithm needed. obtain ⟨θ, hθ⟩ : ∃ θ : ℝ, L / (exp 1 - 1) < exp θ := by refine ⟨L / (exp 1 - 1), ?_⟩ linarith [Real.add_one_le_exp (L / (exp 1 - 1))] have hcontra := key θ rw [← le_div_iff₀ he] at hcontra exact absurd hcontra (not_le.2 hθ)

theorem norm_taylor_remainder_le_of_fderiv_lipschitz (f : Θ → V) (D : Θ → (Θ →L[ℝ] V)) (θ₀ θ : Θ) {L δ : ℝ} (hLnonneg : 0 ≤ L) (hLbound : ∀ η ∈ closedBall θ₀ δ, ∀ η' ∈ closedBall θ₀ δ, ‖D η - D η'‖ ≤ L * ‖η - η'‖) (hD : ∀ η, HasFDerivAt f (D η) η) (hθ : θ ∈ closedBall θ₀ δ) : ‖f θ - f θ₀ - D θ₀ (θ - θ₀)‖ ≤ L * ‖θ - θ₀‖ ^ 2 := by have hδ0 : (0 : ℝ) ≤ δ := le_trans dist_nonneg (Metric.mem_closedBall.mp hθ) have hθ₀ : θ₀ ∈ closedBall θ₀ δ := Metric.mem_closedBall_self hδ0 let s : Set Θ := segment ℝ θ₀ θ have hs : Convex ℝ s := convex_segment θ₀ θ have hsub : s ⊆ closedBall θ₀ δ := (convex_closedBall θ₀ δ).segment_subset hθ₀ hθ have hderiv : ∀ η ∈ s, HasFDerivWithinAt f (D η) s η := by intro η _ exact (hD η).hasFDerivWithinAt have hbound : ∀ η ∈ s, ‖D η - D θ₀‖ ≤ L * ‖θ - θ₀‖ := by intro η hη exact (hLbound η (hsub hη) θ₀ hθ₀).trans <| mul_le_mul_of_nonneg_left (norm_sub_le_of_mem_segment hη) hLnonneg have hmv := hs.norm_image_sub_le_of_norm_hasFDerivWithin_le' hderiv hbound (left_mem_segment ℝ θ₀ θ) (right_mem_segment ℝ θ₀ θ) calc ‖f θ - f θ₀ - D θ₀ (θ - θ₀)‖ ≤ (L * ‖θ - θ₀‖) * ‖θ - θ₀‖ := hmv _ = L * ‖θ - θ₀‖ ^ 2 := by ring

theorem zEstimator_tendsto_normal_of_smoothScore_of_sampleFn (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : SmoothZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (est : (n : ℕ) → (Fin n → X) → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖est n (S.sampleVector n ω) - θ₀‖}) atTop (𝓝 0)) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (est n (S.sampleVector n ω)) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (hEstMeas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator (fun m ω => est m (S.sampleVector m ω)) θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hEstMeas n)⟩) atTop (𝓝 ⟨gaussianLimit reg.influence_measurable reg.influence_integrable_sq, inferInstance⟩) := zEstimator_tendsto_normal_of_smoothScore ψ θ₀ P reg S (fun n ω => est n (S.sampleVector n ω)) hConsistent hMoment hEstMeas

theorem zEstimator_asymLinear (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S θn) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsAsymLinearVec (E := E) θn θ₀ (fun z => -(reg.J₀_inv (ψ θ₀ z))) S (fun n => range n) := by refine ⟨(reg.influenceFunction ψ θ₀ P).mean_zero, (reg.influenceFunction ψ θ₀ P).finite_var, ?_⟩ · have hRootRate := zEstimator_rootRate ψ θ₀ P reg S θn hConsistent hStochEquicont hMoment have hRate := inverseRootRate_of_rootRate θn θ₀ hRootRate have hA : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)) - sqrt (n : ℝ) • reg.J₀ (θn n ω - θ₀)‖) (fun _ => (1 : ℝ)) μ := localStochasticExpansion ψ θ₀ P reg S θn hConsistent hStochEquicont hRate let A : ℕ → Ω → E := fun n ω => (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)) - sqrt (n : ℝ) • reg.J₀ (θn n ω - θ₀) let R : ℕ → Ω → E := fun n ω => (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω) let B : ℕ → Ω → E := fun n ω => sqrt (n : ℝ) • (θn n ω - θ₀) - (sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, -reg.J₀_inv (ψ θ₀ (S.Z i ω)) have hA' : IsLittleOp (fun n ω => ‖A n ω‖) (fun _ => (1 : ℝ)) μ := by simpa [A] using hA have hJ_left : ∀ x : E, reg.J₀_inv (reg.J₀ x) = x := by have hJ_surj : Surjective reg.J₀ := fun y => ⟨reg.J₀_inv y, by have := congrArg (fun T : E →L[ℝ] E => T y) reg.J₀_inverse simpa using this⟩ have hJ_inj : Injective reg.J₀ := by exact (LinearMap.injective_iff_surjective (f := (reg.J₀ : E →ₗ[ℝ] E))).mpr hJ_surj intro x apply hJ_inj have := congrArg (fun T : E →L[ℝ] E => T (reg.J₀ x)) reg.J₀_inverse simpa using this let C : ℝ := ‖reg.J₀_inv‖ + 1 have hC : 0 < C := by dsimp [C]; linarith [norm_nonneg reg.J₀_inv] have mapLittle : ∀ (V : ℕ → Ω → E), IsLittleOp (fun n ω => ‖V n ω‖) (fun _ => (1 : ℝ)) μ → IsLittleOp (fun n ω => ‖reg.J₀_inv (V n ω)‖) (fun _ => (1 : ℝ)) μ := by intro V hV exact IsLittleOp.of_abs_le_const_mul_one hC hV (fun n ω => by simp only [abs_of_nonneg (norm_nonneg _)] exact (reg.J₀_inv.le_opNorm (V n ω)).trans (mul_le_mul_of_nonneg_right (by dsimp [C]; linarith) (norm_nonneg _))) have hJInvA := mapLittle A hA' have hJInvR := mapLittle R (by simpa [R] using hMoment) have hsum := hJInvA.add_one hJInvR have hB : IsLittleOp (fun n ω => ‖B n ω‖) (fun _ => (1 : ℝ)) μ := by refine IsLittleOp.of_abs_le_const_mul_one (C := 1) zero_lt_one hsum ?_ intro n ω simp only [abs_of_nonneg (norm_nonneg _), one_mul] have hBident : B n ω = -reg.J₀_inv (A n ω) + reg.J₀_inv (R n ω) := by simp [A, B, R, Finset.sum_sub_distrib, map_sub, map_smul, map_sum, hJ_left] module rw [abs_of_nonneg (add_nonneg (norm_nonneg _) (norm_nonneg _))] rw [hBident] simpa only [norm_neg] using norm_add_le (-reg.J₀_inv (A n ω)) (reg.J₀_inv (R n ω)) simpa [B, Finset.card_range] using hB

theorem zEstimator_tendsto_normal (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S θn) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) (hθn_meas : ∀ n, AEMeasurable (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n) μ) : Tendsto (β := ProbabilityMeasure E) (fun n => ⟨μ.map (IsAsymLinearVec.rescaledEstimator θn θ₀ (fun m => range m) n), Measure.isProbabilityMeasure_map (hθn_meas n)⟩) atTop (𝓝 ⟨gaussianLimit (reg.influenceFunction ψ θ₀ P).measurable (reg.influenceFunction ψ θ₀ P).finite_var, inferInstance⟩) := by have hAL := zEstimator_asymLinear ψ θ₀ P reg S θn hConsistent hStochEquicont hMoment exact hAL.tendsto_normal_vec_clt (reg.influenceFunction ψ θ₀ P).measurable (gaussianLimit (reg.influenceFunction ψ θ₀ P).measurable (reg.influenceFunction ψ θ₀ P).finite_var) (gaussianLimit_charFun (reg.influenceFunction ψ θ₀ P).measurable (reg.influenceFunction ψ θ₀ P).finite_var) hθn_meas

theorem zEstimator_rootRate (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) [IsProbabilityMeasure μ] (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (hStochEquicont : StochEquicontAt ψ θ₀ P μ S θn) (hMoment : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖) (fun _ => (1 : ℝ)) μ) : IsBigOp (fun n ω => sqrt (n : ℝ) * ‖θn n ω - θ₀‖) (fun _ => (1 : ℝ)) μ := by let B : ℕ → Ω → ℝ := fun n ω => ‖(sqrt (n : ℝ))⁻¹ • ∑ i ∈ range n, ψ (θn n ω) (S.Z i ω)‖ apply zEstimator_rootRate_of_scoreBound ψ θ₀ P reg S θn hConsistent hStochEquicont (fun _ _ => 0) B · simpa using (show IsLittleOp (fun (_ : ℕ) (_ : Ω) => (0 : ℝ)) (fun _ => (1 : ℝ)) μ by intro ε hε simpa [not_le.mpr hε]) · exact hMoment.isBigOp_one · intro n ω exact le_rfl · intro n ω exact norm_nonneg _ · intro n ω simp [B]