Stat.Concentration

theorem ProbabilityTheory.Kernel.iIndepFun.ae_iIndepFun_real {α Ω ι : Type*} [MeasurableSpace α] [MeasurableSpace Ω] {κ : Kernel α Ω} {ν : Measure α} [Finite ι] {X : ι → Ω → ℝ} (hX : ∀ i, Measurable (X i)) (h : iIndepFun X κ ν) : ∀ᵐ a ∂ν, iIndepFun X (κ a) := by classical let cuts : Set (Set ℝ) := ⋃ q : ℚ, {Iic (q : ℝ)} have hident : ∀ᵐ a ∂ν, ∀ (S : Finset ι) (q : ι → ℚ), κ a (⋂ i ∈ S, X i ⁻¹' Iic (q i : ℝ)) = ∏ i ∈ S, κ a (X i ⁻¹' Iic (q i : ℝ)) := by rw [ae_all_iff] intro S rw [ae_all_iff] intro q exact (ProbabilityTheory.Kernel.iIndepFun_iff_measure_inter_preimage_eq_mul (fun _ : ι ↦ borel ℝ) X).mp h S (fun i _ ↦ measurableSet_Iic) filter_upwards [h.ae_isProbabilityMeasure, hident] with a hprob ha let π : ι → Set (Set Ω) := fun i ↦ (fun s : Set ℝ ↦ X i ⁻¹' s) '' cuts have hπ_pi : ∀ i, IsPiSystem (π i) := by intro i convert Real.isPiSystem_Iic_rat.comap (X i) using 1 rfl have hπ_gen : ∀ i, comap (X i) (borel ℝ) = MeasurableSpace.generateFrom (π i) := by intro i rw [Real.borel_eq_generateFrom_Iic_rat, MeasurableSpace.comap_generateFrom] have hπ_ind : ProbabilityTheory.iIndepSets π (κ a) := by rw [ProbabilityTheory.iIndepSets_iff] intro S sets hsets have hrat (i : ι) (hi : i ∈ S) : ∃ q : ℚ, X i ⁻¹' Iic (q : ℝ) = sets i := by rcases hsets i hi with ⟨t, ht, htset⟩ simp only [cuts, Set.mem_iUnion, Set.mem_singleton_iff] at ht obtain ⟨q, hq⟩ := ht subst t exact ⟨q, htset⟩ let q : ι → ℚ := fun i ↦ if hi : i ∈ S then choose (hrat i hi) else 0 have hset (i : ι) (hi : i ∈ S) : sets i = X i ⁻¹' Iic (q i : ℝ) := by simp only [q, dif_pos hi] exact (Classical.choose_spec (hrat i hi)).symm have hinter : (⋂ i ∈ S, sets i) = ⋂ i ∈ S, X i ⁻¹' Iic (q i : ℝ) := by apply Set.iInter_congr intro i apply Set.iInter_congr intro hi exact hset i hi have hprod : (∏ i ∈ S, κ a (sets i)) = ∏ i ∈ S, κ a (X i ⁻¹' Iic (q i : ℝ)) := by apply Finset.prod_congr rfl intro i hi rw [hset i hi] rw [hinter, hprod] exact ha S q haveI : IsProbabilityMeasure (κ a) := hprob have hspaces : ProbabilityTheory.iIndep (fun i ↦ comap (X i) (borel ℝ)) (κ a) := ProbabilityTheory.iIndepSets.iIndep (fun i ↦ comap_le (hX i)) π hπ_pi hπ_gen hπ_ind exact hspaces

theorem ae_ae_condExpKernel_of_ae {Ω : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {p : Ω → Prop} (hp : ∀ᵐ ω ∂μ, p ω) : ∀ᵐ ω ∂μ.trim hm, ∀ᵐ ω' ∂ProbabilityTheory.condExpKernel (mΩ := mΩ) μ m ω, p ω' := by apply Measure.ae_ae_of_ae_comp rwa [ProbabilityTheory.condExpKernel_comp_trim (mΩ := mΩ) hm]

theorem ae_eq_const_condExpKernel_of_measurable {Ω : Type*} [mΩ : MeasurableSpace Ω] [StandardBorelSpace Ω] {μ : Measure Ω} [IsFiniteMeasure μ] {m : MeasurableSpace Ω} (hm : m ≤ mΩ) {β : Type*} [MeasurableSpace β] [MeasurableEq β] {f : Ω → β} (hf : Measurable[m] f) : ∀ᵐ ω ∂μ.trim hm, ∀ᵐ ω' ∂ProbabilityTheory.condExpKernel (mΩ := mΩ) μ m ω, f ω' = f ω := by refine @Measure.ae_ae_of_ae_compProd Ω Ω m mΩ (μ.trim hm) (condExpKernel (mΩ := mΩ) μ m) _ _ (fun pair ↦ f pair.2 = f pair.1) ?_ rw [ProbabilityTheory.compProd_trim_condExpKernel (mΩ := mΩ) hm] rw [ae_map_iff] · exact Filter.Eventually.of_forall fun ω ↦ rfl · have hfirst : @Measurable Ω Ω mΩ m id := measurable_id'' hm have hsecond : @Measurable Ω Ω mΩ mΩ id := measurable_id have hdiag : @Measurable Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) := by refine Measurable.of_comap_le ?_ rw [prod, MeasurableSpace.comap_sup, MeasurableSpace.comap_comp] apply sup_le · change m.comap (Prod.fst ∘ fun ω ↦ (ω, ω)) ≤ mΩ rw [show (Prod.fst ∘ fun ω : Ω ↦ (ω, ω)) = id by rfl, MeasurableSpace.comap_id] exact hm · rw [MeasurableSpace.comap_comp] rw [show (Prod.snd ∘ fun ω : Ω ↦ (id ω, id ω)) = id by rfl, MeasurableSpace.comap_id] exact @aemeasurable Ω (Ω × Ω) mΩ (m.prod mΩ) (fun ω ↦ (id ω, id ω)) μ hdiag · have hfst : @Measurable (Ω × Ω) Ω (m.prod mΩ) m Prod.fst := measurable_fst have hsnd : @Measurable (Ω × Ω) Ω (m.prod mΩ) mΩ Prod.snd := measurable_snd have hf' : @Measurable Ω β mΩ _ f := hf.mono hm le_rfl exact measurableSet_eq_fun (hf'.comp hsnd) (hf.comp hfst)

lemma exists_internal_net_card_le (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (A : Set E) (hA : ∀ x ∈ A, ‖x‖ ≤ 1) {v : ℝ} (hv : 0 < v) : ∃ N : Finset E, (∀ y ∈ N, y ∈ A) ∧ (∀ x ∈ A, ∃ y ∈ N, ‖x - y‖ ≤ v) ∧ (N.card : ℝ) ≤ (1 + 2 / v) ^ finrank ℝ E := by classical let ε : ℝ≥0 := ⟨v, hv.le⟩ have hε : (ε : ℝ≥0∞) = ofReal v := by exact ENNReal.coe_nnreal_eq ε have hAball : A ⊆ closedBall (0 : E) 1 := fun x hx ↦ by simpa [mem_closedBall, dist_zero_right] using hA x hx obtain ⟨M, hM⟩ : ∃ M : Set E, Maximal (fun N ↦ N ⊆ A ∧ Metric.IsSeparated ε N) M := by apply zorn_subset intro c hc hchain refine ⟨⋃₀ c, ?_, fun s hs ↦ subset_sUnion_of_mem hs⟩ constructor · exact sUnion_subset fun s hs ↦ (hc hs).1 · rw [Metric.IsSeparated, hchain.pairwise_sUnion] exact fun s hs ↦ (hc hs).2 have hMsub : M ⊆ A := hM.prop.1 have hMsep : Metric.IsSeparated ε M := hM.prop.2 have hMcover : Metric.IsCover ε A M := Metric.IsCover.of_maximal_isSeparated hM obtain ⟨t, _htB, htfinite, htcover⟩ := finite_cover_balls_of_compact (isCompact_closedBall (0 : E) 1) (half_pos hv) have hsmall : ∀ c : E, (M ∩ ball c (v / 2)).Subsingleton := by intro c x hx y hy by_contra hxy have hsep := hMsep hx.1 hy.1 hxy have hdist : dist x y < v := by calc dist x y ≤ dist x c + dist y c := dist_triangle_right x y c _ < v / 2 + v / 2 := add_lt_add (mem_ball.mp hx.2) (mem_ball.mp hy.2) _ = v := by ring have hdist' : edist x y < (ε : ℝ≥0∞) := by rw [edist_dist, hε, ENNReal.ofReal_lt_ofReal_iff hv] exact hdist exact (not_lt_of_ge hsep.le) hdist' have hMfinite : M.Finite := by have hUfinite : (⋃ c ∈ t, M ∩ ball c (v / 2)).Finite := htfinite.biUnion fun c _ ↦ (hsmall c).finite apply hUfinite.subset intro x hx obtain ⟨c, hct, hxc⟩ := mem_iUnion₂.mp (htcover (hAball (hMsub hx))) exact mem_iUnion₂.mpr ⟨c, hct, hx, hxc⟩ let N : Finset E := hMfinite.toFinset have hNsub : ∀ y ∈ N, y ∈ A := fun y hy ↦ hMsub (by simpa [N] using hy) have hNmem : ∀ y ∈ N, ‖y‖ ≤ 1 := fun y hy ↦ hA y (hNsub y hy) have hNcover : ∀ x ∈ A, ∃ y ∈ N, ‖x - y‖ ≤ v := by intro x hx obtain ⟨y, hyM, hxy⟩ := hMcover hx refine ⟨y, by simpa [N] using hyM, ?_⟩ change edist x y ≤ (ε : ℝ≥0∞) at hxy rw [edist_dist, hε, ENNReal.ofReal_le_ofReal_iff hv.le] at hxy simpa [dist_eq_norm] using hxy refine ⟨N, hNsub, hNcover, ?_⟩ borelize E let μ : Measure E := Measure.addHaar let δ : ℝ := v / 2 let ρ : ℝ := 1 + v / 2 have hδ : 0 < δ := div_pos hv (by norm_num) have hρ : 0 < ρ := by positivity set U := ⋃ c ∈ N, ball (c : E) δ with hU have hdisj : Pairwise (N : Set E) (Disjoint on fun c ↦ ball (c : E) δ) := by rintro c hc d hd hcd apply ball_disjoint_ball have hsep := hMsep (by simpa [N] using hc) (by simpa [N] using hd) hcd have hdist : v < dist c d := by change (ε : ℝ≥0∞) < edist c d at hsep rw [edist_dist, hε, ENNReal.ofReal_lt_ofReal_iff_of_nonneg hv.le] at hsep exact hsep simpa [δ] using hdist.le have hUsub : U ⊆ ball (0 : E) ρ := by refine iUnion₂_subset fun x hx ↦ ?_ apply ball_subset_ball' calc δ + dist x 0 ≤ δ + 1 := by rw [dist_zero_right] exact add_le_add le_rfl (hNmem x hx) _ = ρ := by simp [δ, ρ, add_comm] have hvol : (N.card : ℝ≥0∞) * ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) ≤ ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1) := calc (N.card : ℝ≥0∞) * ofReal (δ ^ finrank ℝ E) * μ (ball 0 1) = μ U := by rw [hU, measure_biUnion_finset hdisj fun c _ ↦ measurableSet_ball] simp only [μ.addHaar_ball_of_pos _ hδ, Finset.sum_const, nsmul_eq_mul, mul_assoc] _ ≤ μ (ball (0 : E) ρ) := measure_mono hUsub _ = ofReal (ρ ^ finrank ℝ E) * μ (ball 0 1) := by simp only [μ.addHaar_ball_of_pos _ hρ] have hcancel : (N.card : ℝ≥0∞) * ofReal (δ ^ finrank ℝ E) ≤ ofReal (ρ ^ finrank ℝ E) := (ENNReal.mul_le_mul_iff_left (measure_ball_pos μ (0 : E) zero_lt_one).ne' measure_ball_lt_top.ne).1 hvol have hreal : (N.card : ℝ) * δ ^ finrank ℝ E ≤ ρ ^ finrank ℝ E := by have h := (ENNReal.toReal_le_toReal (ENNReal.mul_ne_top (by simp) (by simp)) (by simp : ofReal (ρ ^ finrank ℝ E) ≠ ∞)).2 hcancel simpa [ENNReal.toReal_ofReal (pow_nonneg hδ.le _), ENNReal.toReal_ofReal (pow_nonneg hρ.le _)] using h have hδpow : 0 < δ ^ finrank ℝ E := pow_pos hδ _ calc (N.card : ℝ) ≤ ρ ^ finrank ℝ E / δ ^ finrank ℝ E := (le_div_iff₀ hδpow).2 hreal _ = (1 + 2 / v) ^ finrank ℝ E := by rw [← div_pow] congr 1 field_simp [δ, ρ, hv.ne'] ring

lemma exists_unit_ball_net_card_le (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] {v : ℝ} (hv : 0 < v) : ∃ N : Finset E, (∀ x : E, ‖x‖ ≤ 1 → ∃ y ∈ N, ‖x - y‖ ≤ v) ∧ (N.card : ℝ) ≤ (1 + 2 / v) ^ finrank ℝ E := by obtain ⟨N, _hNsub, hNcover, hNcard⟩ := exists_internal_net_card_le E {x : E | ‖x‖ ≤ 1} (by simp) hv exact ⟨N, by simpa using hNcover, hNcard⟩

theorem matrix_rank_le_of_gram_factor {R ι : Type*} [Nontrivial R] [CommRing R] [Fintype ι] {r : ℕ} (Pi : Matrix ι ι R) (vectors : Fin r → ι → R) (hfactor : ∀ i j, Pi i j = ∑ k, vectors k i * vectors k j) : rank Pi ≤ r := by let B : Matrix ι (Fin r) R := fun i k ↦ vectors k i have hPi : Pi = B * B.transpose := by ext i j simp only [Matrix.mul_apply, Matrix.transpose_apply, B] exact hfactor i j rw [hPi] exact (Matrix.rank_mul_le_left B B.transpose).trans <| by simpa using Matrix.rank_le_card_width B

lemma half_norm_lt_inner_of_mem_net {E : Type*} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {N : Finset E} {z : E} (V : Submodule ℝ E) (hnet : ∀ x ∈ V, ‖x‖ = 1 → ∃ v ∈ N, ‖x - v‖ ≤ (1 : ℝ) / 2) (hzV : z ∈ V) (hz : z ≠ 0) : ∃ v ∈ N, ‖z‖ / 2 ≤ ⟪v, z⟫ := by let x : E := ‖z‖⁻¹ • z have hxnorm : ‖x‖ = 1 := by simp [x, norm_smul, hz] obtain ⟨v, hvN, hv⟩ := hnet x (V.smul_mem _ hzV) hxnorm refine ⟨v, hvN, ?_⟩ have hinner : ⟪x - v, x⟫ ≤ (1 : ℝ) / 2 := by calc ⟪x - v, x⟫ ≤ |⟪x - v, x⟫| := le_abs_self _ _ ≤ ‖x - v‖ * ‖x‖ := abs_real_inner_le_norm _ _ _ ≤ ((1 : ℝ) / 2) * 1 := mul_le_mul hv hxnorm.le (norm_nonneg _) (by norm_num) _ = (1 : ℝ) / 2 := by norm_num have hvx : (1 : ℝ) / 2 ≤ ⟪v, x⟫ := by have hid : ⟪x - v, x⟫ = 1 - ⟪v, x⟫ := by rw [inner_sub_left, real_inner_self_eq_norm_sq, hxnorm] ring linarith have hzrepr : z = ‖z‖ • x := by simp [x, smul_smul, hz] rw [hzrepr, inner_smul_right, norm_smul, hxnorm] simp only [mul_one, Real.norm_eq_abs, abs_of_nonneg (norm_nonneg z)] have hmul := mul_le_mul_of_nonneg_left hvx (norm_nonneg z) simpa [div_eq_mul_inv, mul_comm] using hmul

theorem measure_norm_gt_le_of_half_net {Ω E : Type*} [MeasurableSpace Ω] [NormedAddCommGroup E] [InnerProductSpace ℝ E] (P : Measure Ω) [IsFiniteMeasure P] (Z : Ω → E) (V : Submodule ℝ E) (N : Finset E) (hnet : ∀ x ∈ V, ‖x‖ = 1 → ∃ v ∈ N, ‖x - v‖ ≤ (1 : ℝ) / 2) (hZV : ∀ᵐ ω ∂P, Z ω ∈ V) (hsubg : ∀ v ∈ N, HasSubgaussianMGF (fun ω ↦ ⟪v, Z ω⟫) 1 P) {t : ℝ} (ht : 0 ≤ t) : P.real {ω | 2 * t < ‖Z ω‖} ≤ (N.card : ℝ) * exp (-t ^ 2 / 2) := by let U : Set Ω := ⋃ v ∈ N, {ω | t ≤ ⟪v, Z ω⟫} have hAU : {ω | 2 * t < ‖Z ω‖} ≤ᵐ[P] U := by filter_upwards [hZV] with ω hω htail change 2 * t < ‖Z ω‖ at htail have hz : Z ω ≠ 0 := by intro hz simp [hz] at htail linarith obtain ⟨v, hvN, hv⟩ := half_norm_lt_inner_of_mem_net V hnet hω hz refine mem_iUnion₂.mpr ⟨v, hvN, ?_⟩ change t ≤ ⟪v, Z ω⟫ nlinarith calc P.real {ω | 2 * t < ‖Z ω‖} ≤ P.real U := by exact ENNReal.toReal_mono (measure_ne_top P U) (measure_mono_ae hAU) _ ≤ ∑ v ∈ N, P.real {ω | t ≤ ⟪v, Z ω⟫} := measureReal_biUnion_finset_le N _ _ ≤ ∑ _v ∈ N, exp (-t ^ 2 / 2) := by apply Finset.sum_le_sum intro v hv simpa using (hsubg v hv).measure_ge_le ht _ = (N.card : ℝ) * exp (-t ^ 2 / 2) := by rw [Finset.sum_const, nsmul_eq_mul]