Stat.Empirical­Process.Equicontinuity

theorem empProcVec_eq_stochEquicont_gap (S : IIDSample Ω X μ P) (ψ : E → X → E) (θ θ₀ : E) (n : ℕ) (ω : Ω) : S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω = (sqrt (n : ℝ))⁻¹ • (∑ i ∈ range n, (ψ θ (S.Z i ω) - ψ θ₀ (S.Z i ω))) - sqrt (n : ℝ) • ∫ z, (ψ θ z - ψ θ₀ z) ∂P := rfl

theorem empProcVec_atEstimator_tendsto_zero (ψ : E → X → E) (θ₀ : E) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) (ε : ℝ) (hε : 0 < ε) : Tendsto (fun n => μ {ω | ε < ‖S.empProcVec (fun z => ψ (θn n ω) z - ψ θ₀ z) n ω‖}) atTop (𝓝 0) := by 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 set η : ℝ := γ.toReal / 2 with hη have hηpos : 0 < η := by positivity obtain ⟨δ, hδpos, hAEC_event⟩ := hAEC ε hε η hηpos have hδhalf : 0 < δ / 2 := by positivity have hCons_event := (ENNReal.tendsto_nhds_zero.mp (hConsistent (δ / 2) hδhalf)) (ofReal η) (ENNReal.ofReal_pos.mpr hηpos) have hsum_le : ofReal η + ofReal η ≤ γ := by rw [← ENNReal.ofReal_add hηpos.le hηpos.le] have : η + η = γ.toReal := by rw [hη]; ring rw [this, ENNReal.ofReal_toReal hγtop] filter_upwards [hAEC_event, hCons_event] with n hAEC_n hCons_n -- `{ε < ‖R_n‖} ⊆ {δ/2 < ‖θn − θ₀‖} ∪ {∃ θ, ‖θ − θ₀‖ < δ ∧ ε < ‖Gₙ‖}` have hsub : {ω | ε < ‖S.empProcVec (fun z => ψ (θn n ω) z - ψ θ₀ z) n ω‖} ⊆ {ω | δ / 2 < ‖θn n ω - θ₀‖} ∪ {ω | ∃ θ : E, ‖θ - θ₀‖ < δ ∧ ε < ‖S.empProcVec (fun z => ψ θ z - ψ θ₀ z) n ω‖} := by intro ω hω by_cases hθ : ‖θn n ω - θ₀‖ < δ · exact inr ⟨θn n ω, hθ, hω⟩ · refine inl ?_ have hδle : δ ≤ ‖θn n ω - θ₀‖ := not_lt.mp hθ change δ / 2 < ‖θn n ω - θ₀‖ linarith refine le_trans (measure_mono hsub) (le_trans (measure_union_le _ _) ?_) exact le_trans (add_le_add hCons_n hAEC_n) hsum_le

theorem stochEquicontAt_of_asymptoticEquicont (ψ : E → X → E) (θ₀ : E) (S : IIDSample Ω X μ P) (θn : ℕ → Ω → E) (hAEC : AsymptoticEquicont ψ θ₀ P μ S) (hConsistent : ∀ ε > 0, Tendsto (fun n => μ {ω | ε < ‖θn n ω - θ₀‖}) atTop (𝓝 0)) : StochEquicontAt ψ θ₀ P μ S θn := by intro ε hε refine ⟨1, one_pos, ?_⟩ have hgap := empProcVec_atEstimator_tendsto_zero ψ θ₀ S θn hAEC hConsistent ε hε refine ENNReal.tendsto_nhds_zero.mpr ?_ intro γ hγ filter_upwards [(ENNReal.tendsto_nhds_zero.mp hgap) γ hγ] with n hn refine le_trans (measure_mono ?_) hn intro ω hω exact hω.2

theorem empProcVec_isLittleOp_of_L2 [IsProbabilityMeasure μ] [IsProbabilityMeasure P] (ψ : E → X → E) (θ₀ : E) (θn : ℕ → E) (S : IIDSample Ω X μ P) (hψ_meas : ∀ θ, Measurable (fun x => ψ θ x - ψ θ₀ x)) (hψ_L2 : ∀ θ, MemLp (fun x => ψ θ x - ψ θ₀ x) 2 P) (hmod : Tendsto (fun n => ∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) atTop (𝓝 0)) : IsLittleOp (fun n ω => ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖) (fun _ => (1 : ℝ)) μ := by intro ε hε have hεsq : (0 : ℝ) < ε ^ 2 := by positivity have hset : ∀ n, {ω | ε * (fun _ => (1 : ℝ)) n < |‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖|} = {ω | ε < ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖} := by intro n; ext ω; simp only [Set.mem_setOf_eq, mul_one, abs_norm] simp_rw [hset] have hbound : ∀ n, μ {ω | ε < ‖S.empProcVec (fun z => ψ (θn n) z - ψ θ₀ z) n ω‖} ≤ ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal (ε ^ 2) := fun n => empProcVec_chebyshev S (fun z => ψ (θn n) z - ψ θ₀ z) (hψ_meas (θn n)) (hψ_L2 (θn n)) n hε have hdiv : Tendsto (fun n => ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal (ε ^ 2)) atTop (𝓝 0) := by have hreal : Tendsto (fun n => (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ε ^ 2) atTop (𝓝 0) := by simpa using hmod.div_const (ε ^ 2) have heq : ∀ n, ofReal (∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ofReal (ε ^ 2) = ofReal ((∫ x, ‖ψ (θn n) x - ψ θ₀ x‖ ^ 2 ∂P) / ε ^ 2) := fun n => (ENNReal.ofReal_div_of_pos hεsq).symm simp_rw [heq] rw [← ENNReal.ofReal_zero] exact (ENNReal.continuous_ofReal.tendsto 0).comp hreal exact tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds hdiv (fun n => zero_le) hbound

theorem empProcVec_sq_lintegral_le [IsProbabilityMeasure μ] [IsProbabilityMeasure P] [MeasurableSpace E] [BorelSpace E] (S : IIDSample Ω X μ P) (f : X → E) (hf_meas : Measurable f) (hf_L2 : MemLp f 2 P) (n : ℕ) : ∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ ≤ ofReal (∫ x, ‖f x‖ ^ 2 ∂P) := by classical rcases Nat.eq_zero_or_pos n with hn | hn · -- `n = 0`: the process is `0`. subst hn have h0 : ∀ ω, S.empProcVec f 0 ω = 0 := fun ω => by simp [IIDSample.empProcVec] simp only [h0, norm_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, ENNReal.ofReal_zero, lintegral_zero] exact zero_le -- `n ≥ 1`. have hf_int : Integrable f P := hf_L2.integrable (by norm_num) set b := stdOrthonormalBasis ℝ E with hb -- coordinate functions `g j x = ⟪b j, f x⟫` set g : _ → X → ℝ := fun j x => inner ℝ (b j) (f x) with hg have hg_meas : ∀ j, Measurable (g j) := fun j => ((innerSL ℝ (b j)).continuous.measurable).comp hf_meas have hbnorm : ∀ j, ‖b j‖ = 1 := fun j => b.orthonormal.norm_eq_one j -- each coordinate function is in `L²(P)` have hg_L2 : ∀ j, MemLp (g j) 2 P := by intro j refine hf_L2.mono (hg_meas j).aestronglyMeasurable (Filter.Eventually.of_forall fun x => ?_) calc ‖g j x‖ ≤ ‖b j‖ * ‖f x‖ := norm_inner_le_norm _ _ _ = ‖f x‖ := by rw [hbnorm j, one_mul] -- `(eLpNorm (g j) 2 P)² = ∫ (g j)² dP` have hsq_eLpNorm : ∀ j, (eLpNorm (g j) 2 P).toReal ^ 2 = ∫ x, (g j x) ^ 2 ∂P := by intro j have hpow := (hg_L2 j).eLpNorm_eq_integral_rpow_norm (by norm_num : (2 : ENNReal) ≠ 0) (by norm_num : (2 : ENNReal) ≠ ⊤) rw [hpow] simp only [ENNReal.toReal_ofNat] have hroot_nonneg : 0 ≤ (∫ a, ‖g j a‖ ^ (2 : ℝ) ∂P) ^ (2 : ℝ)⁻¹ := Real.rpow_nonneg (integral_nonneg fun x => by positivity) _ rw [ENNReal.toReal_ofReal hroot_nonneg] have hint_eq : (∫ a, ‖g j a‖ ^ (2 : ℝ) ∂P) = ∫ x, (g j x) ^ 2 ∂P := by congr with x; rw [Real.rpow_two, Real.norm_eq_abs, sq_abs] rw [hint_eq, ← Real.rpow_natCast ((∫ x, (g j x) ^ 2 ∂P) ^ (2 : ℝ)⁻¹) 2, ← Real.rpow_mul (integral_nonneg fun z => sq_nonneg _), show ((2 : ℝ)⁻¹ * (2 : ℕ)) = 1 by norm_num, Real.rpow_one] -- coordinate second-moment bound from the scalar variance primitive have hcomp : ∀ j, ∫⁻ ω, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ ≤ ofReal ((eLpNorm (g j) 2 P).toReal ^ 2) := by intro j have hrw : (fun ω => ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2)) = (fun ω => ofReal (((sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, (g j (S.Z i ω) - ∫ x, g j x ∂P)) ^ 2)) := by funext ω rw [IIDSample.inner_empProcVec S f hf_int (b j) hn ω] simp only [Finset.card_range] rfl rw [hrw] have hbound := iid_centered_sum_sq_lintegral_le (μ := μ) (P := P) (s := range n) (by simpa [Finset.card_range] using hn) (W := S.Z) (fun i _ => S.meas i) (m_A := ⊥) (hm_A_le := bot_le) (hW_indep_A := ProbabilityTheory.indep_bot_left _) (hW_iid_pi := S.iid_pi_law n) (g := fun _ x => g j x) (hg_uncurry_meas := (hg_meas j).comp measurable_snd) (hg_memLp := fun _ => hg_L2 j) refine hbound.trans ?_ rw [lintegral_const] simp -- measurability of each coordinate integrand in `ω` have hmeas_int : ∀ j, Measurable (fun ω => ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2)) := by intro j have hproc : Measurable (fun ω => S.empProcVec f n ω) := S.measurable_empProcVec f hf_meas n exact (((innerSL ℝ (b j)).continuous.measurable.comp hproc).pow_const 2).ennreal_ofReal -- assembly: Parseval coordinate-wise, then sum the bounds calc ∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ = ∫⁻ ω, ∑ j, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ := by refine lintegral_congr fun ω => ?_ rw [← b.sum_sq_inner_right (S.empProcVec f n ω), ENNReal.ofReal_sum_of_nonneg fun j _ => sq_nonneg _] _ = ∑ j, ∫⁻ ω, ofReal (inner ℝ (b j) (S.empProcVec f n ω) ^ 2) ∂μ := lintegral_finset_sum _ fun j _ => hmeas_int j _ ≤ ∑ j, ofReal ((eLpNorm (g j) 2 P).toReal ^ 2) := Finset.sum_le_sum fun j _ => hcomp j _ = ofReal (∑ j, (eLpNorm (g j) 2 P).toReal ^ 2) := (ENNReal.ofReal_sum_of_nonneg fun j _ => sq_nonneg _).symm _ = ofReal (∫ x, ‖f x‖ ^ 2 ∂P) := by congr 1 simp_rw [hsq_eLpNorm] rw [← integral_finset_sum] · refine integral_congr_ae (Filter.Eventually.of_forall fun x => ?_) exact b.sum_sq_inner_right (f x) · intro j _ have : (fun x => (g j x) ^ 2) = (fun x => ‖g j x‖ ^ 2) := by funext x; rw [Real.norm_eq_abs, sq_abs] rw [this] exact (hg_L2 j).integrable_norm_rpow (by norm_num) (by norm_num) |>.congr (Filter.Eventually.of_forall fun x => by simp)

theorem empProcVec_chebyshev [IsProbabilityMeasure μ] [IsProbabilityMeasure P] [MeasurableSpace E] [BorelSpace E] (S : IIDSample Ω X μ P) (f : X → E) (hf_meas : Measurable f) (hf_L2 : MemLp f 2 P) (n : ℕ) {ε : ℝ} (hε : 0 < ε) : μ {ω | ε < ‖S.empProcVec f n ω‖} ≤ ofReal (∫ x, ‖f x‖ ^ 2 ∂P) / ofReal (ε ^ 2) := by have hεsq : (0 : ℝ) < ε ^ 2 := by positivity have hne0 : ofReal (ε ^ 2) ≠ 0 := by rw [Ne, ENNReal.ofReal_eq_zero]; linarith have hnetop : ofReal (ε ^ 2) ≠ ⊤ := ENNReal.ofReal_ne_top have haemeas : AEMeasurable (fun ω => ofReal (‖S.empProcVec f n ω‖ ^ 2)) μ := (((S.measurable_empProcVec f hf_meas n).norm.pow_const 2).ennreal_ofReal).aemeasurable have hsub : {ω | ε < ‖S.empProcVec f n ω‖} ⊆ {ω | ofReal (ε ^ 2) ≤ ofReal (‖S.empProcVec f n ω‖ ^ 2)} := by intro ω hω refine ENNReal.ofReal_le_ofReal ?_ have hω' : ε < ‖S.empProcVec f n ω‖ := hω exact pow_le_pow_left₀ hε.le hω'.le 2 calc μ {ω | ε < ‖S.empProcVec f n ω‖} ≤ μ {ω | ofReal (ε ^ 2) ≤ ofReal (‖S.empProcVec f n ω‖ ^ 2)} := measure_mono hsub _ ≤ (∫⁻ ω, ofReal (‖S.empProcVec f n ω‖ ^ 2) ∂μ) / ofReal (ε ^ 2) := meas_ge_le_lintegral_div haemeas hne0 hnetop _ ≤ ofReal (∫ x, ‖f x‖ ^ 2 ∂P) / ofReal (ε ^ 2) := by gcongr exact empProcVec_sq_lintegral_le S f hf_meas hf_L2 n