Stat.Concentration.Hilbert.Empirical­Mean

theorem centeredEmpiricalMean_eq_inv_smul_sum_centered (P : Measure X) [IsProbabilityMeasure P] (f : X → H) {m : ℕ} (hm : 0 < m) (z : Fin m → X) : centeredEmpiricalMean P f m z = (m : ℝ)⁻¹ • ∑ r, (f (z r) - populationMean P f) := by unfold centeredEmpiricalMean empiricalMean rw [Finset.sum_sub_distrib, smul_sub] congr 1 simp only [Finset.sum_const, Finset.card_fin] rw [← Nat.cast_smul_eq_nsmul ℝ, smul_smul] simp [hm.ne']

@[fun_prop] theorem measurable_centeredEmpiricalMeanNorm (P : Measure X) (f : X → H) (hf : StronglyMeasurable f) (m : ℕ) : Measurable (centeredEmpiricalMeanNorm P f m) := by unfold centeredEmpiricalMeanNorm centeredEmpiricalMean empiricalMean populationMean have hsum : StronglyMeasurable (fun z : Fin m → X => ∑ r, f (z r)) := by rw [← Finset.sum_fn] apply Finset.stronglyMeasurable_sum intro r _ change StronglyMeasurable (f ∘ fun z : Fin m → X => z r) exact hf.comp_measurable (measurable_pi_apply r) exact ((hsum.const_smul (m : ℝ)⁻¹).sub stronglyMeasurable_const).norm.measurable

theorem centeredEmpiricalMeanNorm_boundedDifference (P : Measure X) (f : X → H) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 0 < m) (i : Fin m) (z : Fin m → X) (x' : X) : |centeredEmpiricalMeanNorm P f m z - centeredEmpiricalMeanNorm P f m (update z i x')| ≤ 2 / (m : ℝ) := by have hsum : (∑ r, f (z r)) - ∑ r, f (update z i x' r) = f (z i) - f x' := by have hupdate : (fun r => f (update z i x' r)) = update (fun r => f (z r)) i (f x') := by funext r by_cases hri : r = i <;> simp [hri] rw [hupdate, Finset.sum_update_of_mem (Finset.mem_univ i)] rw [Finset.sdiff_singleton_eq_erase] rw [← Finset.sum_erase_add univ (fun r => f (z r)) (Finset.mem_univ i)] abel calc |centeredEmpiricalMeanNorm P f m z - centeredEmpiricalMeanNorm P f m (update z i x')| ≤ ‖centeredEmpiricalMean P f m z - centeredEmpiricalMean P f m (update z i x')‖ := abs_norm_sub_norm_le _ _ _ = ‖(m : ℝ)⁻¹ • (f (z i) - f x')‖ := by unfold centeredEmpiricalMean empiricalMean rw [sub_sub_sub_cancel_right, ← smul_sub, hsum] _ = (m : ℝ)⁻¹ * ‖f (z i) - f x'‖ := by rw [norm_smul] simp _ ≤ (m : ℝ)⁻¹ * 2 := by gcongr calc ‖f (z i) - f x'‖ ≤ ‖f (z i)‖ + ‖f x'‖ := norm_sub_le _ _ _ ≤ 1 + 1 := add_le_add (hbound _) (hbound _) _ = 2 := by norm_num _ = 2 / (m : ℝ) := by ring

theorem norm_sum_sq_eq_sum_inner {ι : Type*} [Fintype ι] (v : ι → H) : ‖∑ i, v i‖ ^ 2 = ∑ i, ∑ j, inner ℝ (v i) (v j) := by rw [← real_inner_self_eq_norm_sq] simp_rw [sum_inner, inner_sum]

theorem integral_sub_populationMean_eq_zero (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : Integrable f P) : ∫ x, (f x - populationMean P f) ∂P = 0 := by rw [integral_sub hf (integrable_const _)] simp [populationMean]

theorem integral_norm_centered_coordinate_sq_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf_L2 : MemLp f 2 P) {m : ℕ} (i : Fin m) : ∫ z : Fin m → X, ‖f (z i) - populationMean P f‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := by exact hf_L2.sub (memLp_const (populationMean P f)) have hg_sq : Integrable (fun x => ‖g x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hg_L2.aestronglyMeasurable).1 hg_L2 exact integral_comp_eval (μ := fun _ : Fin m => P) (i := i) hg_sq.aestronglyMeasurable

theorem integral_inner_centered_coordinates_eq_zero (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf_L2 : MemLp f 2 P) {m : ℕ} {i j : Fin m} (hij : i ≠ j) : ∫ z : Fin m → X, inner ℝ (f (z i) - populationMean P f) (f (z j) - populationMean P f) ∂(Measure.pi (fun _ : Fin m => P)) = 0 := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := by exact hf_L2.sub (memLp_const (populationMean P f)) have hg : Integrable g P := hg_L2.integrable (by norm_num) have hIndep : (fun z : Fin m → X => z i) ⟂ᵢ[Measure.pi (fun _ : Fin m => P)] (fun z : Fin m → X => z j) := (iIndepFun_pi (X := fun _ : Fin m => id) (fun _ => aemeasurable_id)).indepFun hij have hgi : Integrable g ((Measure.pi (fun _ : Fin m => P)).map (fun z : Fin m → X => z i)) := by rw [(measurePreserving_eval (fun _ : Fin m => P) i).map_eq] exact hg have hgj : Integrable g ((Measure.pi (fun _ : Fin m => P)).map (fun z : Fin m → X => z j)) := by rw [(measurePreserving_eval (fun _ : Fin m => P) j).map_eq] exact hg rw [show (fun z : Fin m → X => inner ℝ (f (z i) - populationMean P f) (f (z j) - populationMean P f)) = fun z => (innerSL ℝ) (g (z i)) (g (z j)) by rfl] rw [hIndep.integral_bilin_comp_comp (measurable_pi_apply i).aemeasurable (measurable_pi_apply j).aemeasurable hgi hgj (innerSL ℝ)] rw [integral_comp_eval (μ := fun _ : Fin m => P) hg.aestronglyMeasurable, integral_comp_eval (μ := fun _ : Fin m => P) hg.aestronglyMeasurable] change inner ℝ (∫ x, f x - populationMean P f ∂P) (∫ x, f x - populationMean P f ∂P) = 0 rw [integral_sub_populationMean_eq_zero P f (hf_L2.integrable (by norm_num))] simp

theorem population_centered_secondMoment_le (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf_L2 : MemLp f 2 P) : ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P ≤ ∫ x, ‖f x‖ ^ 2 ∂P := by have hfi : Integrable f P := hf_L2.integrable (by norm_num) have hsq : Integrable (fun x => ‖f x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hf_L2.aestronglyMeasurable).1 hf_L2 have hinner : Integrable (fun x => inner ℝ (populationMean P f) (f x)) P := hfi.const_inner (populationMean P f) have hcross : Integrable (fun x => 2 * inner ℝ (populationMean P f) (f x)) P := hinner.const_mul 2 have hconst : Integrable (fun _ : X => ‖populationMean P f‖ ^ 2) P := integrable_const _ have hpoint : ∀ x, ‖f x - populationMean P f‖ ^ 2 = ‖f x‖ ^ 2 - 2 * inner ℝ (populationMean P f) (f x) + ‖populationMean P f‖ ^ 2 := by intro x rw [norm_sub_sq_real, real_inner_comm] rw [integral_congr_ae (ae_of_all P hpoint)] change (∫ x, ((fun x => ‖f x‖ ^ 2) - (fun x => 2 * inner ℝ (populationMean P f) (f x)) + (fun _ : X => ‖populationMean P f‖ ^ 2)) x ∂P) ≤ _ rw [integral_add' (hsq.sub hcross) hconst, integral_sub' hsq hcross, integral_const_mul, integral_inner hfi, integral_const, probReal_univ, one_smul] rw [show ∫ x, f x ∂P = populationMean P f by rfl, real_inner_self_eq_norm_sq] nlinarith [sq_nonneg ‖populationMean P f‖]

theorem centeredSum_secondMoment_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf_L2 : MemLp f 2 P) (m : ℕ) : ∫ z : Fin m → X, ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = (m : ℝ) * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by let g : X → H := fun x => f x - populationMean P f have hg_L2 : MemLp g 2 P := hf_L2.sub (memLp_const (populationMean P f)) have hcoord (i : Fin m) : MemLp (fun z : Fin m → X => g (z i)) 2 (Measure.pi (fun _ : Fin m => P)) := by change MemLp (g ∘ (Function.eval i : (Fin m → X) → X)) 2 _ exact hg_L2.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m => P) i) have hinner (i j : Fin m) : Integrable (fun z : Fin m → X => inner ℝ (g (z i)) (g (z j))) (Measure.pi (fun _ : Fin m => P)) := by let gi : (Fin m → X) →₂[Measure.pi (fun _ : Fin m => P)] H := (hcoord i).toLp (fun z : Fin m → X => g (z i)) let gj : (Fin m → X) →₂[Measure.pi (fun _ : Fin m => P)] H := (hcoord j).toLp (fun z : Fin m → X => g (z j)) apply (L2.integrable_inner gi gj).congr filter_upwards [(hcoord i).coeFn_toLp, (hcoord j).coeFn_toLp] with z hzi hzj change gi z = g (z i) at hzi change gj z = g (z j) at hzj rw [hzi, hzj] have hterm (i j : Fin m) : (∫ z : Fin m → X, inner ℝ (g (z i)) (g (z j)) ∂(Measure.pi (fun _ : Fin m => P))) = if i = j then ∫ x, ‖g x‖ ^ 2 ∂P else 0 := by by_cases hij : i = j · subst j rw [if_pos rfl] simpa only [g, real_inner_self_eq_norm_sq] using integral_norm_centered_coordinate_sq_eq P f hf_L2 i · rw [if_neg hij] simpa only [g] using integral_inner_centered_coordinates_eq_zero P f hf_L2 hij rw [show (fun z : Fin m → X => ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2) = fun z => ∑ i, ∑ j, inner ℝ (g (z i)) (g (z j)) by funext z exact norm_sum_sq_eq_sum_inner (fun r => f (z r) - populationMean P f)] rw [integral_finsetSum univ (by intro i hi exact integrable_finsetSum univ (fun j _ => hinner i j))] simp_rw [integral_finsetSum univ (fun j _ => hinner _ j), hterm] simp [g]

theorem centeredEmpiricalMean_secondMoment_eq (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hf_L2 : MemLp f 2 P) {m : ℕ} (hm : 0 < m) : ∫ z : Fin m → X, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂(Measure.pi (fun _ : Fin m => P)) = (m : ℝ)⁻¹ * ∫ x, ‖f x - populationMean P f‖ ^ 2 ∂P := by have hpoint (z : Fin m → X) : ‖centeredEmpiricalMean P f m z‖ ^ 2 = ((m : ℝ)⁻¹) ^ 2 * ‖∑ r, (f (z r) - populationMean P f)‖ ^ 2 := by rw [centeredEmpiricalMean_eq_inv_smul_sum_centered P f hm z, norm_smul] rw [mul_pow] congr 2 simp rw [integral_congr_ae (ae_of_all _ hpoint), integral_const_mul, centeredSum_secondMoment_eq P f hf_L2 m] field_simp

theorem integral_norm_le_sqrt_integral_norm_sq (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → H) (hg : StronglyMeasurable g) (hg_sq : Integrable (fun ω => ‖g ω‖ ^ 2) μ) : ∫ ω, ‖g ω‖ ∂μ ≤ sqrt (∫ ω, ‖g ω‖ ^ 2 ∂μ) := by have hg_L2 : MemLp g 2 μ := (memLp_two_iff_integrable_sq_norm hg.aestronglyMeasurable).2 hg_sq exact integral_abs_le_sqrt_integral_sq μ g hg_L2

theorem centeredEmpiricalMean_norm_integral_le_inv_sqrt (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 1 ≤ m) : ∫ z : Fin m → X, ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ∂(Measure.pi (fun _ : Fin m => P)) ≤ 1 / sqrt m := by let Q : Measure (Fin m → X) := Measure.pi (fun _ : Fin m => P) have hf_L2 : MemLp f 2 P := memLp_two_of_norm_le_one P f hf hbound have hcoord_L2 (i : Fin m) : MemLp (fun z : Fin m → X => f (z i)) 2 Q := by change MemLp (f ∘ (Function.eval i : (Fin m → X) → X)) 2 Q exact hf_L2.comp_measurePreserving (measurePreserving_eval (fun _ : Fin m => P) i) have hsum_L2 : MemLp (fun z : Fin m → X => ∑ r, f (z r)) 2 Q := by simpa only [Finset.sum_apply] using memLp_finsetSum univ (fun i _ => hcoord_L2 i) have hmean_L2 : MemLp (centeredEmpiricalMean P f m) 2 Q := by unfold centeredEmpiricalMean empiricalMean populationMean exact (hsum_L2.const_smul (m : ℝ)⁻¹).sub (memLp_const _) have hsum_sm : StronglyMeasurable (fun z : Fin m → X => ∑ r, f (z r)) := by rw [← Finset.sum_fn] apply Finset.stronglyMeasurable_sum intro i _ exact hf.comp_measurable (measurable_pi_apply i) have hmean_sm : StronglyMeasurable (centeredEmpiricalMean P f m) := by unfold centeredEmpiricalMean empiricalMean populationMean exact (hsum_sm.const_smul (m : ℝ)⁻¹).sub stronglyMeasurable_const have hmean_sq : Integrable (fun z => ‖centeredEmpiricalMean P f m z‖ ^ 2) Q := (memLp_two_iff_integrable_sq_norm hmean_sm.aestronglyMeasurable).1 hmean_L2 have hraw_sq : Integrable (fun x => ‖f x‖ ^ 2) P := (memLp_two_iff_integrable_sq_norm hf.aestronglyMeasurable).1 hf_L2 have hraw : (∫ x, ‖f x‖ ^ 2 ∂P) ≤ 1 := by calc (∫ x, ‖f x‖ ^ 2 ∂P) ≤ ∫ _x : X, (1 : ℝ) ∂P := by apply integral_mono hraw_sq (integrable_const _) intro x nlinarith [norm_nonneg (f x), hbound x] _ = 1 := by simp have hm_pos : 0 < m := Nat.lt_of_lt_of_le Nat.zero_lt_one hm have hsecond : (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) ≤ (m : ℝ)⁻¹ := by calc (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) ≤ (m : ℝ)⁻¹ * ∫ x, ‖f x‖ ^ 2 ∂P := by simpa only [Q] using centeredEmpiricalMean_secondMoment_le P f hf hf_L2 hm_pos _ ≤ (m : ℝ)⁻¹ * 1 := mul_le_mul_of_nonneg_left hraw (by positivity) _ = (m : ℝ)⁻¹ := mul_one _ calc (∫ z : Fin m → X, ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖ ∂(Measure.pi (fun _ : Fin m => P))) ≤ sqrt (∫ z, ‖centeredEmpiricalMean P f m z‖ ^ 2 ∂Q) := by simpa only [Q, centeredEmpiricalMean, empiricalMean, populationMean] using integral_norm_le_sqrt_integral_norm_sq Q (centeredEmpiricalMean P f m) hmean_sm hmean_sq _ ≤ sqrt ((m : ℝ)⁻¹) := Real.sqrt_le_sqrt hsecond _ = 1 / sqrt m := by rw [Real.sqrt_inv]; simp

theorem centeredEmpiricalMean_norm_tail_le (P : Measure X) [IsProbabilityMeasure P] (f : X → H) (hf : StronglyMeasurable f) (hbound : ∀ x, ‖f x‖ ≤ 1) {m : ℕ} (hm : 1 ≤ m) {δ : ℝ} (hδ : 0 < δ) (hδ_one : δ < 1) : ((Measure.pi (fun _ : Fin m => P)) {z | 1 / sqrt m + sqrt (2 * log (1 / δ) / m) < ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖}).toReal ≤ δ := by let _ : Nonempty X := nonempty_of_isProbabilityMeasure P have hm_pos : 0 < m := Nat.lt_of_lt_of_le Nat.zero_lt_one hm have hmR : 0 < (m : ℝ) := by exact_mod_cast hm_pos have hlog : 0 < log (1 / δ) := Real.log_pos (one_lt_one_div hδ hδ_one) have hrad : 0 ≤ 2 * log (1 / δ) / (m : ℝ) := by positivity have hsum : (∑ _i : Fin m, (2 / (m : ℝ)) ^ 2) = 4 / (m : ℝ) := by simp only [Finset.sum_const, Finset.card_fin, nsmul_eq_mul] field_simp ring have ht : (m : ℝ) / 4 * ∑ _i : Fin m, (2 / (m : ℝ)) ^ 2 ≤ 1 := by rw [hsum] field_simp norm_num have hmc := mcdiarmid_inequality_pos' (μ := P) (ι := Fin m) (X' := id) measurable_id (f' := centeredEmpiricalMeanNorm P f m) (c' := fun _ : Fin m => 2 / (m : ℝ)) (fun i z x' => centeredEmpiricalMeanNorm_boundedDifference P f hbound hm_pos i z x') (measurable_centeredEmpiricalMeanNorm P f hf m) (ε := sqrt (2 * log (1 / δ) / (m : ℝ))) (Real.sqrt_nonneg _) (t := (m : ℝ) / 4) ht simp only at hmc have hInt : ∫ z : Fin m → X, centeredEmpiricalMeanNorm P f m z ∂(Measure.pi (fun _ : Fin m => P)) ≤ 1 / sqrt m := by simpa only [centeredEmpiricalMeanNorm, centeredEmpiricalMean, empiricalMean, populationMean] using centeredEmpiricalMean_norm_integral_le_inv_sqrt P f hf hbound hm calc ((Measure.pi (fun _ : Fin m => P)) {z | 1 / sqrt m + sqrt (2 * log (1 / δ) / m) < ‖(m : ℝ)⁻¹ • ∑ r, f (z r) - ∫ x, f x ∂P‖}).toReal ≤ ((Measure.pi (fun _ : Fin m => P)) {z | centeredEmpiricalMeanNorm P f m z - ∫ x, centeredEmpiricalMeanNorm P f m x ∂(Measure.pi (fun _ : Fin m => P)) ≥ sqrt (2 * log (1 / δ) / (m : ℝ))}).toReal := by apply ENNReal.toReal_mono (measure_ne_top _ _) apply measure_mono intro z hz change sqrt (2 * log (1 / δ) / (m : ℝ)) ≤ centeredEmpiricalMeanNorm P f m z - ∫ x, centeredEmpiricalMeanNorm P f m x ∂(Measure.pi (fun _ : Fin m => P)) change 1 / sqrt (m : ℝ) + sqrt (2 * log (1 / δ) / (m : ℝ)) < centeredEmpiricalMeanNorm P f m z at hz linarith _ ≤ exp (-2 * (sqrt (2 * log (1 / δ) / (m : ℝ))) ^ 2 * ((m : ℝ) / 4)) := hmc _ = δ := by rw [Real.sq_sqrt hrad] have harg : -2 * (2 * log (1 / δ) / (m : ℝ)) * ((m : ℝ) / 4) = log δ := by rw [show log (1 / δ) = -log δ by simp only [one_div, Real.log_inv]] field_simp ring rw [harg, Real.exp_log hδ]