Stat.MEstimation

lemma poissonCell_linear_coercive_bound (m x : ℝ) (hm : 0 < m) : m * x - exp x ≤ (m + 1) ^ 2 / 2 - min m 1 * |x| := by have hc0 : 0 < min m 1 := lt_min hm zero_lt_one by_cases hx : x ≤ 0 · rw [abs_of_nonpos hx] have he : 0 ≤ exp x := (Real.exp_pos x).le have hc : min m 1 ≤ m := min_le_left _ _ have hK : 0 ≤ (m + 1) ^ 2 / 2 := div_nonneg (sq_nonneg _) (by norm_num) nlinarith · have hx0 : 0 ≤ x := le_of_not_ge hx have he := Real.pow_div_factorial_le_exp x hx0 2 norm_num [factorial] at he have hc : min m 1 ≤ 1 := min_le_right _ _ have hs : 0 ≤ (x - (m + 1)) ^ 2 := sq_nonneg _ rw [abs_of_nonneg hx0] nlinarith

lemma poissonCell_strictConcave_midpoint (q m x y : ℝ) (hq : 0 < q) (hxy : x ≠ y) : (q * (m * x - exp x) + q * (m * y - exp y)) / 2 < q * (m * ((x + y) / 2) - exp ((x + y) / 2)) := by have hconv := strictConvexOn_exp.2 (Set.mem_univ x) (Set.mem_univ y) hxy (show 0 < (1 / 2 : ℝ) by norm_num) (show 0 < (1 / 2 : ℝ) by norm_num) (by norm_num : (1 / 2 : ℝ) + 1 / 2 = 1) simp only [smul_eq_mul] at hconv have := mul_lt_mul_of_pos_left hconv hq have harg : (1 / 2 : ℝ) * x + (1 / 2 : ℝ) * y = (x + y) / 2 := by ring rw [harg] at this calc _ = q * (m * ((x + y) / 2) - (exp x + exp y) / 2) := by ring _ < q * (m * ((x + y) / 2) - exp ((x + y) / 2)) := by nlinarith

lemma finitePoissonObjective_continuous {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Fintype I] (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) : Continuous (finitePoissonObjective q m A) := by unfold finitePoissonObjective fun_prop

lemma finitePoissonObjective_score {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [Fintype I] (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (x d : E) (hx : ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A x) : ∑ i, q i * A d i * (m i - exp (A x i)) = 0 := by let path : ℝ → E := fun s => x + s • d have heta (i : I) : HasDerivAt (fun s => A (path s) i) (A d i) 0 := by have hfun : (fun s : ℝ => A (path s) i) = fun s : ℝ => A x i + s * A d i := by funext s simp [path, map_add, map_smul, smul_eq_mul] rw [hfun] have h : HasDerivAt (fun s : ℝ => A x i + s * A d i) (0 + 1 * A d i) 0 := (hasDerivAt_const (𝕜 := ℝ) 0 (A x i)).fun_add ((hasDerivAt_id (𝕜 := ℝ) 0).mul_const (A d i)) simpa using h have hderiv : HasDerivAt (fun s => finitePoissonObjective q m A (path s)) (∑ i, q i * A d i * (m i - exp (A x i))) 0 := by have hraw : HasDerivAt (fun s : ℝ => ∑ i, q i * (m i * A (path s) i - exp (A (path s) i))) (∑ i, q i * (m i * A d i - exp (A (path 0) i) * A d i)) 0 := HasDerivAt.fun_sum (u := univ) (fun i _ => (((heta i).const_mul (m i)).sub (heta i).exp).const_mul (q i)) have hpath0 : path 0 = x := by simp [path] have hval : (∑ i, q i * (m i * A d i - exp (A (path 0) i) * A d i)) = ∑ i, q i * A d i * (m i - exp (A x i)) := by rw [hpath0] exact Finset.sum_congr rfl fun i _ => by ring have hfe : (fun s : ℝ => finitePoissonObjective q m A (path s)) = fun s : ℝ => ∑ i, q i * (m i * A (path s) i - exp (A (path s) i)) := rfl rw [hfe, ← hval] exact hraw have hlocal : IsLocalMax (fun s => finitePoissonObjective q m A (path s)) 0 := Filter.Eventually.of_forall fun s => by simpa [path] using hx (path s) exact hlocal.hasDerivAt_eq_zero hderiv

lemma finitePoissonObjective_isMax_of_score {E I : Type*} [AddCommGroup E] [Module ℝ E] [Fintype I] (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (x : E) (hq : ∀ i, 0 ≤ q i) (hscore : ∀ d : E, ∑ i, q i * A d i * (m i - exp (A x i)) = 0) : ∀ y, finitePoissonObjective q m A y ≤ finitePoissonObjective q m A x := by intro y have hterm (i : I) : q i * (m i * A y i - exp (A y i)) - q i * (m i * A x i - exp (A x i)) ≤ q i * A (y - x) i * (m i - exp (A x i)) := by have he : 1 + (A y i - A x i) ≤ exp (A y i - A x i) := by simpa [add_comm] using Real.add_one_le_exp (A y i - A x i) have hexp : exp (A x i) * (1 + (A y i - A x i)) ≤ exp (A y i) := by calc exp (A x i) * (1 + (A y i - A x i)) ≤ exp (A x i) * exp (A y i - A x i) := mul_le_mul_of_nonneg_left he (Real.exp_pos _).le _ = exp (A y i) := by rw [← Real.exp_add] congr 1 ring have hqexp := mul_le_mul_of_nonneg_left hexp (hq i) simp only [map_sub, Pi.sub_apply] nlinarith unfold finitePoissonObjective have hsum := Finset.sum_le_sum fun i (_ : i ∈ univ) => hterm i rw [hscore (y - x), Finset.sum_sub_distrib] at hsum linarith

lemma uniqueGlobalMax_maximizerOrZero {E : Type*} [Zero E] (f : E → ℝ) (h : ∃! x : E, ∀ y, f y ≤ f x) : IsUniqueGlobalMax f (maximizerOrZero f) := by obtain ⟨x, hx, huniq⟩ := h have hex : ∃ z, ∀ y, f y ≤ f z := ⟨x, hx⟩ have hsel : maximizerOrZero f = x := by rw [maximizerOrZero, dif_pos hex] exact huniq _ (Classical.choose_spec hex) rw [hsel] exact ⟨hx, fun y hy => huniq y (fun z => (hx z).trans_eq hy.symm)⟩

theorem score_diff_L2_isLittleOp_sqrt (ψ : 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)) : IsLittleOp (fun n ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖^2) (fun _ => (1 : ℝ)) μ := by 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 / 4 have hαpos : 0 < α := by dsimp [α] linarith rcases reg.score_envelope with ⟨δenv, hδenv, F, hFmeas, hFnonneg, hFint, hFbound⟩ let K : ℝ := ∫ z, F z ^ 2 ∂P have hK_nonneg : 0 ≤ K := by dsimp [K] exact integral_nonneg fun z => sq_nonneg (F z) let M : ℝ := (K + 1) / α have hK1pos : 0 < K + 1 := by linarith have hMpos : 0 < M := div_pos hK1pos hαpos have hKM_nonneg : 0 ≤ K / M := div_nonneg hK_nonneg (le_of_lt hMpos) have hKM_le : K / M ≤ α := by dsimp [M] field_simp [hαpos.ne', hK1pos.ne'] nlinarith [hK_nonneg, hαpos] let τ : ℝ := min δenv (sqrt (ε / (M + 1))) have hM1pos : 0 < M + 1 := by linarith have hτpos : 0 < τ := by dsimp [τ] exact lt_min hδenv (Real.sqrt_pos.mpr (div_pos hε hM1pos)) have hτhalf_pos : 0 < τ / 2 := by linarith have hτ_le_env : τ ≤ δenv := by dsimp [τ] exact min_le_left _ _ have hτ_le_sqrt : τ ≤ sqrt (ε / (M + 1)) := by dsimp [τ] exact min_le_right _ _ have hτsq_le : τ ^ 2 ≤ ε / (M + 1) := by have hs := pow_le_pow_left₀ (le_of_lt hτpos) hτ_le_sqrt 2 simpa [Real.sq_sqrt (div_nonneg (le_of_lt hε) (le_of_lt hM1pos))] using hs have hτsqM_lt : τ ^ 2 * M < ε := by have hmul := mul_le_mul_of_nonneg_right hτsq_le (le_of_lt hMpos) have hfrac : ε / (M + 1) * M < ε := by rw [div_mul_eq_mul_div] rw [div_lt_iff₀ hM1pos] nlinarith [hε, hMpos] exact lt_of_le_of_lt hmul hfrac let Mn : ℕ → Ω → ℝ := fun n ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, F (S.Z i ω) ^ 2 have hFpow_meas : Measurable fun z => F z ^ 2 := hFmeas.pow_const 2 have hmap_i : ∀ i, μ.map (S.Z i) = P := by intro i calc μ.map (S.Z i) = μ.map (S.Z 0) := (S.identDist i).map_eq.symm _ = P := S.law have hint_i : ∀ i, Integrable (fun ω => F (S.Z i ω) ^ 2) μ := by intro i have hi : Integrable (fun z => F z ^ 2) (μ.map (S.Z i)) := by simpa [hmap_i i] using hFint simpa [Function.comp_def] using hi.comp_measurable (S.meas i) have hint_eq_i : ∀ i, (∫ ω, F (S.Z i ω) ^ 2 ∂μ) = K := by intro i calc (∫ ω, F (S.Z i ω) ^ 2 ∂μ) = ∫ z, F z ^ 2 ∂(μ.map (S.Z i)) := by exact (integral_map (S.meas i).aemeasurable hFpow_meas.aestronglyMeasurable).symm _ = K := by rw [hmap_i i] have hMn_nonneg_point : ∀ n ω, 0 ≤ Mn n ω := by intro n ω dsimp [Mn] exact mul_nonneg (inv_nonneg.mpr (Nat.cast_nonneg n)) (sum_nonneg fun i _hi => sq_nonneg (F (S.Z i ω))) have hMn_nonneg : ∀ n, 0 ≤ᵐ[μ] Mn n := by intro n exact Eventually.of_forall (hMn_nonneg_point n) have hMn_int : ∀ n, Integrable (Mn n) μ := by intro n dsimp [Mn] exact (integrable_finset_sum (range n) (fun i _hi => hint_i i)).const_mul _ have hMn_integral_le : ∀ n, (∫ ω, Mn n ω ∂μ) ≤ K := by intro n by_cases hn : n = 0 · subst n dsimp [Mn, K] simpa using hK_nonneg · have hnpos : 0 < n := Nat.pos_of_ne_zero hn have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn dsimp [Mn] rw [integral_const_mul] rw [MeasureTheory.integral_finset_sum (range n)] · simp_rw [hint_eq_i] simp [Finset.sum_const, hnR] · intro i _hi exact hint_i i have hMn_markov : ∀ n, μ {ω | M < Mn n ω} ≤ ofReal (K / M) := by intro n have hge_real : (μ {ω | M ≤ Mn n ω}).toReal ≤ K / M := by have hmark := MeasureTheory.mul_meas_ge_le_integral_of_nonneg (hMn_nonneg n) (hMn_int n) M have hdiv : μ.real {ω | M ≤ Mn n ω} ≤ (∫ ω, Mn n ω ∂μ) / M := by rw [measureReal_def] exact (le_div_iff₀ hMpos).mpr (by simpa [measureReal_def, mul_comm] using hmark) exact le_trans hdiv (div_le_div_of_nonneg_right (hMn_integral_le n) (le_of_lt hMpos)) exact le_trans (measure_mono (by intro ω hω change M ≤ Mn n ω exact le_of_lt hω)) ((ENNReal.le_ofReal_iff_toReal_le (measure_ne_top μ _) hKM_nonneg).mpr hge_real) have hCons_le := (ENNReal.tendsto_nhds_zero.mp (hConsistent (τ / 2) hτhalf_pos)) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have htwo_alpha_lt_gamma : ofReal (2 * α) < γ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hγpos] · exact hγtop filter_upwards [hCons_le] with n hnCons exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |(n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2|} ≤ μ ({ω | τ / 2 < ‖θn n ω - θ₀‖} ∪ {ω | M < Mn n ω}) := by apply measure_mono_ae have hFbound_i : ∀ i : ℕ, ∀ᵐ ω ∂μ, ∀ θ : E, ‖θ - θ₀‖ < δenv → ‖ψ θ (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ≤ ‖θ - θ₀‖ * F (S.Z i ω) := by intro i have hbound_map : ∀ᵐ z ∂(μ.map (S.Z i)), ∀ θ : E, ‖θ - θ₀‖ < δenv → ‖ψ θ z - ψ θ₀ z‖ ≤ ‖θ - θ₀‖ * F z := by simpa [hmap_i i] using hFbound exact ae_of_ae_map (S.meas i).aemeasurable hbound_map have hFbound_all : ∀ᵐ ω ∂μ, ∀ i ∈ range n, ∀ θ : E, ‖θ - θ₀‖ < δenv → ‖ψ θ (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ≤ ‖θ - θ₀‖ * F (S.Z i ω) := by rw [Finset.eventually_all] intro i _hi exact hFbound_i i filter_upwards [hFbound_all] with ω hFboundω hω replace hω : ε * (fun _ => (1 : ℝ)) n < |(n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2| := hω by_cases hn0 : n = 0 · subst n have hω0 : ε < 0 := by simpa using hω exact elim (not_lt_of_ge hε.le hω0) · have hnR_nonneg : 0 ≤ (n : ℝ)⁻¹ := inv_nonneg.mpr (Nat.cast_nonneg n) have hT_nonneg : 0 ≤ (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2 := by exact mul_nonneg hnR_nonneg (sum_nonneg fun i _hi => sq_nonneg _) have hTgt : ε < (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2 := by have hω' : ε < |(n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2| := by simpa using hω simpa [abs_of_nonneg hT_nonneg] using hω' by_cases hθsmall : ‖θn n ω - θ₀‖ ≤ τ / 2 · by_cases hMsmall : Mn n ω ≤ M · have hθ_lt_env : ‖θn n ω - θ₀‖ < δenv := by have hθ_lt_τ : ‖θn n ω - θ₀‖ < τ := by linarith [hθsmall, hτpos] exact lt_of_lt_of_le hθ_lt_τ hτ_le_env have hsum_le : (∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2) ≤ ‖θn n ω - θ₀‖ ^ 2 * ∑ i ∈ range n, F (S.Z i ω) ^ 2 := by rw [Finset.mul_sum] refine Finset.sum_le_sum ?_ intro i _hi have henv := hFboundω i _hi (θn n ω) hθ_lt_env have hrhs_nonneg : 0 ≤ ‖θn n ω - θ₀‖ * F (S.Z i ω) := mul_nonneg (norm_nonneg _) (hFnonneg _) have hsquare : ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2 ≤ (‖θn n ω - θ₀‖ * F (S.Z i ω)) ^ 2 := by have hnorm_nonneg : 0 ≤ ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ := norm_nonneg _ exact sq_le_sq' (by linarith) henv simpa [mul_pow] using hsquare have hT_le : (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2 ≤ ‖θn n ω - θ₀‖ ^ 2 * Mn n ω := by have hmul := mul_le_mul_of_nonneg_left hsum_le hnR_nonneg dsimp [Mn] nlinarith have hθsq_le : ‖θn n ω - θ₀‖ ^ 2 ≤ τ ^ 2 := by exact pow_le_pow_left₀ (norm_nonneg _) (by linarith) 2 have hprod_le : ‖θn n ω - θ₀‖ ^ 2 * Mn n ω ≤ τ ^ 2 * M := by have hMn_nonnegω : 0 ≤ Mn n ω := hMn_nonneg_point n ω exact mul_le_mul hθsq_le hMsmall hMn_nonnegω (sq_nonneg τ) have hT_lt : (n : ℝ)⁻¹ * ∑ i ∈ range n, ‖ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω)‖ ^ 2 < ε := lt_of_le_of_lt (le_trans hT_le hprod_le) hτsqM_lt exact elim (not_lt_of_ge hT_lt.le hTgt) · exact inr (lt_of_not_ge hMsmall) · exact inl (lt_of_not_ge hθsmall) _ ≤ μ {ω | τ / 2 < ‖θn n ω - θ₀‖} + μ {ω | M < Mn n ω} := MeasureTheory.measure_union_le _ _ _ ≤ ofReal α + ofReal (K / M) := add_le_add hnCons (hMn_markov n) _ ≤ ofReal α + ofReal α := add_le_add le_rfl (ENNReal.ofReal_le_ofReal hKM_le) _ = ofReal (2 * α) := by rw [← ENNReal.ofReal_add] · congr 1 -- … truncated; follow the source link for the rest …

theorem empiricalScoreDiff_isLittleOp_sqrt (ψ : 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) : IsLittleOp (fun n ω => ‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖) (fun _ => (1 : ℝ)) μ := by 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 / 4 have hαpos : 0 < α := by dsimp [α] linarith rcases hStochEquicont ε hε with ⟨δ, hδ_pos, hStoch⟩ have hδhalf_pos : 0 < δ / 2 := by linarith have hStoch_le := (ENNReal.tendsto_nhds_zero.mp hStoch) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have hCons_le := (ENNReal.tendsto_nhds_zero.mp (hConsistent (δ / 2) hδhalf_pos)) (ofReal α) (ENNReal.ofReal_pos.mpr hαpos) have htwo_alpha_lt_gamma : ofReal (2 * α) < γ := by rw [ENNReal.ofReal_lt_iff_lt_toReal] · dsimp [α] linarith · dsimp [α] linarith [le_of_lt hγpos] · exact hγtop filter_upwards [hStoch_le, hCons_le] with n hnStoch hnCons exact le_of_lt <| calc μ {ω | ε * (fun _ => (1 : ℝ)) n < |‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖|} ≤ μ ({ω | ‖θn n ω - θ₀‖ < δ ∧ ε < ‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖} ∪ {ω | δ / 2 < ‖θn n ω - θ₀‖}) := by apply measure_mono intro ω hω have hR : ε < ‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖ := by simpa [abs_of_nonneg (norm_nonneg _)] using hω by_cases hθ : ‖θn n ω - θ₀‖ < δ · exact inl ⟨hθ, hR⟩ · exact inr (by have hδle : δ ≤ ‖θn n ω - θ₀‖ := le_of_not_gt hθ have hhalf_lt_delta : δ / 2 < δ := by linarith [hδ_pos] exact lt_of_lt_of_le hhalf_lt_delta hδle) _ ≤ μ {ω | ‖θn n ω - θ₀‖ < δ ∧ ε < ‖(sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ (θn n ω) (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ (θn n ω) z - ψ θ₀ z) ∂P‖} + μ {ω | δ / 2 < ‖θn n ω - θ₀‖} := MeasureTheory.measure_union_le _ _ _ ≤ ofReal α + ofReal α := add_le_add hnStoch hnCons _ = ofReal (2 * α) := by rw [← ENNReal.ofReal_add] · congr 1 ring · linarith · linarith _ < γ := htwo_alpha_lt_gamma

theorem populationScoreDiff_eq_jacobian_plus_remainder (ψ : E → X → E) (θ₀ : E) (P : Measure X) (reg : ZEstimatorRegularity ψ θ₀ P) : (fun θ => ∫ z, (ψ θ z - ψ θ₀ z) ∂P - reg.J₀ (θ - θ₀)) =o[𝓝 θ₀] fun θ => ‖θ - θ₀‖ := by rcases reg.psi_int_neighborhood with ⟨δ, hδ_pos, hδ_int⟩ have hψ₀ : Integrable (ψ θ₀) P := by exact hδ_int θ₀ (by simpa using hδ_pos) have hbase : (fun θ => (∫ z, ψ θ z ∂P) - (∫ z, ψ θ₀ z ∂P) - reg.J₀ (θ - θ₀)) =o[𝓝 θ₀] fun θ => θ - θ₀ := reg.J₀_spec.isLittleO have hbase_norm : (fun θ => (∫ z, ψ θ z ∂P) - (∫ z, ψ θ₀ z ∂P) - reg.J₀ (θ - θ₀)) =o[𝓝 θ₀] fun θ => ‖θ - θ₀‖ := (Asymptotics.isLittleO_norm_right).mpr hbase refine hbase_norm.congr' ?_ EventuallyEq.rfl have hnear : ∀ᶠ θ in 𝓝 θ₀, ‖θ - θ₀‖ < δ := by refine Metric.eventually_nhds_iff.mpr ⟨δ, hδ_pos, ?_⟩ intro θ hθ simpa [dist_eq_norm] using hθ filter_upwards [hnear] with θ hθ rw [MeasureTheory.integral_sub (hδ_int θ (by simpa [dist_eq_norm] using hθ)) hψ₀]

theorem consistent_lt_norm_of_le_dist {E : Type*} [NormedAddCommGroup E] (θn : ℕ → Ω → E) (θ₀ : E) (h : ∀ ε : ℝ, 0 < ε → Tendsto (fun n => μ {ω | ε ≤ dist (θn n ω) θ₀}) atTop (𝓝 0)) : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0) := by intro ε hε refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (h ε hε) (Eventually.of_forall fun n => zero_le) (Eventually.of_forall fun n => measure_mono ?_) intro ω hω simp only [Set.mem_setOf_eq, dist_eq_norm] at hω ⊢ exact le_of_lt hω

lemma finitePoissonObjective_tendstoUniformlyOn {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Fintype I] (qN mN : ℕ → I → ℝ) (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (K : Set E) (hK : IsCompact K) (hq : ∀ i, Tendsto (fun N => qN N i) atTop (nhds (q i))) (hm : ∀ i, Tendsto (fun N => mN N i) atTop (nhds (m i))) : TendstoUniformlyOn (fun N => finitePoissonObjective (qN N) (mN N) A) (finitePoissonObjective q m A) atTop K := by let cN : ℕ → (I → ℝ) × (I → ℝ) := fun N => (qN N, mN N) let c : (I → ℝ) × (I → ℝ) := (q, m) let F : ((I → ℝ) × (I → ℝ)) → E → ℝ := fun p x => finitePoissonObjective p.1 p.2 A x have hc : Tendsto cN atTop (nhds c) := by exact (tendsto_pi_nhds.mpr hq).prodMk_nhds (tendsto_pi_nhds.mpr hm) let U := closedBall c 1 letI : ProperSpace ((I → ℝ) × (I → ℝ)) := FiniteDimensional.proper_real _ have hU : IsCompact U := ProperSpace.isCompact_closedBall c 1 have hcU : c ∈ U := by simp [U] have hevent : ∀ᶠ N in atTop, cN N ∈ U := by have := (Metric.tendsto_nhds.mp hc 1 zero_lt_one) filter_upwards [this] with N hN exact Metric.mem_closedBall.mpr hN.le have hcWithin : Tendsto cN atTop (nhdsWithin c U) := by rw [nhdsWithin] exact tendsto_inf.2 ⟨hc, tendsto_principal.2 hevent⟩ have hcont : Continuous (uncurry F) := by unfold F finitePoissonObjective fun_prop have hUC : UniformContinuousOn (uncurry F) (U ×ˢ K) := (hU.prod hK).uniformContinuousOn_of_continuous hcont.continuousOn have hlocal : TendstoUniformlyOn F (F c) (nhdsWithin c U) K := hUC.tendstoUniformlyOn hcU intro V hV exact hcWithin.eventually (hlocal V hV)

lemma finitePoissonObjective_eventually_common_compact {E I : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [Fintype I] (qN mN : ℕ → I → ℝ) (q m : I → ℝ) (A : E →ₗ[ℝ] (I → ℝ)) (argmax : ℕ → 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))) (hmax : ∀ᶠ N in atTop, ∀ y, finitePoissonObjective (qN N) (mN N) A y ≤ finitePoissonObjective (qN N) (mN N) A (argmax N)) : ∃ K : Set E, IsCompact K ∧ ∀ᶠ N in atTop, argmax N ∈ K := by classical let w : I → ℝ := fun i => q i / 2 * min (m i / 2) 1 let B : E →ₗ[ℝ] (I → ℝ) := { toFun := fun x i => w i * A x i map_add' := by intro x y; funext i; simp; ring map_smul' := by intro c x; funext i; simp; ring } have hwpos : ∀ i, 0 < w i := by intro i exact mul_pos (half_pos (hqpos i)) (lt_min (half_pos (hmpos i)) zero_lt_one) have hB : Injective B := by intro x y hxy apply hA funext i have hi := congrFun hxy i dsimp [B] at hi exact (mul_left_cancel₀ (ne_of_gt (hwpos i)) hi) obtain ⟨L, hL, hanti⟩ := (LinearMap.injective_iff_antilipschitz B).mp hB let kappa : ℝ := L⁻¹ have hkappa : 0 < kappa := inv_pos.mpr hL 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‖ ≤ (L : ℝ) * ‖B x‖ := by simpa [edist_dist, dist_eq_norm, ENNReal.toReal_mul] using hh change (L : ℝ)⁻¹ * ‖x‖ ≤ ‖B x‖ calc (L : ℝ)⁻¹ * ‖x‖ ≤ (L : ℝ)⁻¹ * ((L : ℝ) * ‖B x‖) := mul_le_mul_of_nonneg_left h' (inv_nonneg.mpr hL.le) _ = ((L : ℝ)⁻¹ * (L : ℝ)) * ‖B x‖ := by ring _ = ‖B x‖ := by rw [inv_mul_cancel₀ (show (L : ℝ) ≠ 0 by exact_mod_cast ne_of_gt hL)] simp have hbounds : ∀ᶠ N in atTop, ∀ i, q i / 2 < qN N i ∧ qN N i < 2 * q i ∧ m i / 2 < mN N i ∧ mN N i < 2 * m i := by rw [Filter.eventually_all] intro i filter_upwards [ (tendsto_order.1 (hq i)).1 (q i / 2) (by linarith [hqpos i]), (tendsto_order.1 (hq i)).2 (2 * q i) (by linarith [hqpos i]), (tendsto_order.1 (hm i)).1 (m i / 2) (by linarith [hmpos i]), (tendsto_order.1 (hm i)).2 (2 * m i) (by linarith [hmpos i])] with N hqlo hqhi hmlo hmhi exact ⟨hqlo, hqhi, hmlo, hmhi⟩ let M : ℝ := ∑ i, (2 * q i) * ((2 * m i + 1) ^ 2 / 2) let Q : ℝ := ∑ i, 2 * q i have hM : 0 ≤ M := sum_nonneg fun i _ => mul_nonneg (mul_nonneg (by norm_num) (hqpos i).le) (div_nonneg (sq_nonneg _) (by norm_num)) have hQ : 0 ≤ Q := sum_nonneg fun i _ => mul_nonneg (by norm_num) (hqpos i).le let R : ℝ := (M + Q) / kappa have hR : 0 ≤ R := div_nonneg (add_nonneg hM hQ) hkappa.le let K : Set E := closedBall 0 R letI : ProperSpace E := proper_real E refine ⟨K, ProperSpace.isCompact_closedBall 0 R, ?_⟩ filter_upwards [hbounds, hmax] with N hb hmaxN have htail (x : E) : finitePoissonObjective (qN N) (mN N) A x ≤ M - ‖B x‖ := by have hterm : ∀ i, qN N i * (mN N i * A x i - exp (A x i)) ≤ (2 * q i) * ((2 * m i + 1) ^ 2 / 2) - |B x i| := by intro i have hc := poissonCell_linear_coercive_bound (mN N i) (A x i) (lt_trans (half_pos (hmpos i)) (hb i).2.2.1) have hqn : 0 ≤ qN N i := (lt_trans (half_pos (hqpos i)) (hb i).1).le have hlower : w i ≤ qN N i * min (mN N i) 1 := by exact mul_le_mul (le_of_lt (hb i).1) (min_le_min (le_of_lt (hb i).2.2.1) le_rfl) (le_min (half_pos (hmpos i)).le zero_le_one) hqn have habs : |B x i| = w i * |A x i| := by dsimp [B] rw [abs_mul, abs_of_pos (hwpos i)] rw [habs] have hcoarse := mul_le_mul_of_nonneg_left hc hqn have hconst : qN N i * ((mN N i + 1) ^ 2 / 2) ≤ (2 * q i) * ((2 * m i + 1) ^ 2 / 2) := by have hmn0 : 0 ≤ mN N i := (lt_trans (half_pos (hmpos i)) (hb i).2.2.1).le have hmupper := (hb i).2.2.2 have hsq : (mN N i + 1) ^ 2 ≤ (2 * m i + 1) ^ 2 := by nlinarith exact mul_le_mul (le_of_lt (hb i).2.1) (div_le_div_of_nonneg_right hsq (by norm_num)) (div_nonneg (sq_nonneg _) (by norm_num)) (mul_nonneg (by norm_num) (hqpos i).le) nlinarith [mul_le_mul_of_nonneg_right hlower (abs_nonneg (A x i))] calc finitePoissonObjective (qN N) (mN N) A x ≤ ∑ i, ((2 * q i) * ((2 * m i + 1) ^ 2 / 2) - |B x i|) := Finset.sum_le_sum fun i _ => hterm i _ = M - ∑ i, |B x i| := by rw [Finset.sum_sub_distrib] _ ≤ M - ‖B x‖ := by gcongr rw [Pi.norm_def] have hnn : (Finset.univ.sup fun i => ‖B x i‖₊) ≤ ∑ i, ‖B x i‖₊ := Finset.sup_le fun i _ => Finset.single_le_sum (f := fun j => ‖B x j‖₊) (fun j _ => zero_le) (Finset.mem_univ i) calc ((Finset.univ.sup fun i => ‖B x i‖₊ : NNReal) : ℝ) ≤ ((∑ i, ‖B x i‖₊ : NNReal) : ℝ) := NNReal.coe_le_coe.mpr hnn _ = ∑ i, |B x i| := by simp [Real.norm_eq_abs] have hzero : -Q ≤ finitePoissonObjective (qN N) (mN N) A 0 := by unfold finitePoissonObjective simp only [map_zero, Pi.zero_apply, mul_zero, Real.exp_zero, zero_sub, mul_neg, mul_one, Finset.sum_neg_distrib, neg_le_neg_iff] exact Finset.sum_le_sum fun i _ => (hb i).2.1.le have hchain := (hzero.trans (hmaxN 0)).trans (htail (argmax N)) have hbn := hBnorm (argmax N) have hnorm : ‖argmax N‖ ≤ R := by dsimp [R] apply (le_div_iff₀ hkappa).2 linarith simpa [K, Metric.mem_closedBall, dist_eq_norm] using hnorm