Stat.Concentration.Matrix

theorem localWeight_integrable {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (hqmeas : Measurable q) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) : Integrable q P := by refine (integrable_const (μ := P) (1 : ℝ)).mono' hqmeas.aestronglyMeasurable ?_ filter_upwards [hq] with x hx simpa [Real.norm_eq_abs, abs_of_nonneg hx.1] using hx.2

theorem localWeight_centered_envelope {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) {p : ℝ} (hp : ∫ x, q x ∂P = p) : ∀ᵐ x ∂P, |q x - p| ≤ 1 := by have hp_bounds : 0 ≤ p ∧ p ≤ 1 := by rw [← hp] constructor · exact integral_nonneg_of_ae (hq.mono fun x hx ↦ hx.1) · by_cases hqint : Integrable q P · calc ∫ x, q x ∂P ≤ ∫ _ : X, (1 : ℝ) ∂P := integral_mono_ae hqint (integrable_const (μ := P) (1 : ℝ)) (hq.mono fun x hx ↦ hx.2) _ = 1 := by simp · rw [integral_undef hqint] norm_num filter_upwards [hq] with x hx rw [abs_le] constructor <;> linarith [hx.1, hx.2, hp_bounds.1, hp_bounds.2]

-- Proof route: use `E[(q-Eq)^2] = E[q^2]-(Eq)^2 ≤ E[q^2]` and `q^2 ≤ q`. theorem localWeight_centered_secondMoment_le {X : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (hqmeas : Measurable q) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) {p : ℝ} (hp : ∫ x, q x ∂P = p) : ∫ x, (q x - ∫ y, q y ∂P) ^ 2 ∂P ≤ p := by have hqint : Integrable q P := localWeight_integrable P q hqmeas hq have hqLp : MemLp q 2 P := memLp_of_bounded hq hqmeas.aestronglyMeasurable 2 have hq_sq_le : ∀ᵐ x ∂P, q x ^ 2 ≤ q x := by filter_upwards [hq] with x hx nlinarith [mul_nonneg hx.1 (sub_nonneg.mpr hx.2)] calc ∫ x, (q x - ∫ y, q y ∂P) ^ 2 ∂P = variance q P := (variance_eq_integral hqmeas.aemeasurable).symm _ = ∫ x, q x ^ 2 ∂P - (∫ x, q x ∂P) ^ 2 := by simpa only [Pi.pow_apply] using variance_eq_sub hqLp _ ≤ ∫ x, q x ^ 2 ∂P := by nlinarith [sq_nonneg (∫ x, q x ∂P)] _ ≤ ∫ x, q x ∂P := integral_mono_ae hqLp.integrable_sq hqint hq_sq_le _ = p := hp

theorem localGram_centered_envelope {X κ : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (phi : κ → X → ℝ) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) {B : ℝ} (hB : 0 ≤ B) (hphi : ∀ j, ∀ᵐ x ∂P, |phi j x| ≤ B) (j k : κ) : ∀ᵐ x ∂P, |q x * phi j x * phi k x - ∫ y, q y * phi j y * phi k y ∂P| ≤ 2 * B ^ 2 := by have hcoord_bound : ∀ᵐ x ∂P, |q x * phi j x * phi k x| ≤ B ^ 2 := by filter_upwards [hq, hphi j, hphi k] with x hx hphi_j hphi_k have hprod : |phi j x| * |phi k x| ≤ B * B := mul_le_mul hphi_j hphi_k (abs_nonneg _) hB calc |q x * phi j x * phi k x| = q x * (|phi j x| * |phi k x|) := by rw [abs_mul, abs_mul, abs_of_nonneg hx.1] ring _ ≤ 1 * (B * B) := mul_le_mul hx.2 hprod (mul_nonneg (abs_nonneg _) (abs_nonneg _)) (by norm_num) _ = B ^ 2 := by ring have hmean_bound : |∫ y, q y * phi j y * phi k y ∂P| ≤ B ^ 2 := by by_cases hcoord_int : Integrable (fun y ↦ q y * phi j y * phi k y) P · calc |∫ y, q y * phi j y * phi k y ∂P| ≤ ∫ y, |q y * phi j y * phi k y| ∂P := abs_integral_le_integral_abs _ ≤ ∫ _ : X, B ^ 2 ∂P := integral_mono_ae hcoord_int.abs (integrable_const (μ := P) (B ^ 2)) hcoord_bound _ = B ^ 2 := by simp · rw [integral_undef hcoord_int, abs_zero] positivity filter_upwards [hcoord_bound] with x hx calc |q x * phi j x * phi k x - ∫ y, q y * phi j y * phi k y ∂P| ≤ |q x * phi j x * phi k x| + |∫ y, q y * phi j y * phi k y ∂P| := abs_sub _ _ _ ≤ B ^ 2 + B ^ 2 := add_le_add hx hmean_bound _ = 2 * B ^ 2 := by ring

-- Proof route: discard the nonnegative squared mean from the variance identity, then use -- `(q φ_j φ_k)^2 ≤ B^4 q`, which follows from `q^2 ≤ q`. theorem localGram_centered_secondMoment_le {X κ : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (phi : κ → X → ℝ) (hqmeas : Measurable q) (hphimeas : ∀ j, Measurable (phi j)) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) {B p : ℝ} (hB : 0 ≤ B) (hphi : ∀ j, ∀ᵐ x ∂P, |phi j x| ≤ B) (hp : ∫ x, q x ∂P = p) (j k : κ) : ∫ x, (q x * phi j x * phi k x - ∫ y, q y * phi j y * phi k y ∂P) ^ 2 ∂P ≤ B ^ 4 * p := by let coord : X → ℝ := fun x ↦ q x * phi j x * phi k x have hcoord_meas : Measurable coord := (hqmeas.mul (hphimeas j)).mul (hphimeas k) have hcoord_bound : ∀ᵐ x ∂P, |coord x| ≤ B ^ 2 := by filter_upwards [hq, hphi j, hphi k] with x hx hphi_j hphi_k have hprod : |phi j x| * |phi k x| ≤ B * B := mul_le_mul hphi_j hphi_k (abs_nonneg _) hB calc |coord x| = q x * (|phi j x| * |phi k x|) := by simp only [coord, abs_mul, abs_of_nonneg hx.1] ring _ ≤ 1 * (B * B) := mul_le_mul hx.2 hprod (mul_nonneg (abs_nonneg _) (abs_nonneg _)) (by norm_num) _ = B ^ 2 := by ring have hcoordLp : MemLp coord 2 P := memLp_of_bounded (hcoord_bound.mono fun _ hx ↦ (abs_le.mp hx)) hcoord_meas.aestronglyMeasurable 2 have hqint : Integrable q P := localWeight_integrable P q hqmeas hq have hsquare_bound : ∀ᵐ x ∂P, coord x ^ 2 ≤ B ^ 4 * q x := by filter_upwards [hq, hphi j, hphi k] with x hx hphi_j hphi_k have hq_sq : q x ^ 2 ≤ q x := by nlinarith [mul_nonneg hx.1 (sub_nonneg.mpr hx.2)] have hj_sq : (phi j x) ^ 2 ≤ B ^ 2 := by rw [sq_le_sq] simpa [abs_of_nonneg hB] using hphi_j have hk_sq : (phi k x) ^ 2 ≤ B ^ 2 := by rw [sq_le_sq] simpa [abs_of_nonneg hB] using hphi_k have hprod_sq : (phi j x) ^ 2 * (phi k x) ^ 2 ≤ B ^ 2 * B ^ 2 := mul_le_mul hj_sq hk_sq (sq_nonneg _) (sq_nonneg _) calc coord x ^ 2 = q x ^ 2 * ((phi j x) ^ 2 * (phi k x) ^ 2) := by simp only [coord] ring _ ≤ q x * (B ^ 2 * B ^ 2) := mul_le_mul hq_sq hprod_sq (mul_nonneg (sq_nonneg _) (sq_nonneg _)) hx.1 _ = B ^ 4 * q x := by ring have hmajorant_int : Integrable (fun x ↦ B ^ 4 * q x) P := by simpa only [smul_eq_mul] using hqint.const_mul (B ^ 4) change ∫ x, (coord x - ∫ y, coord y ∂P) ^ 2 ∂P ≤ B ^ 4 * p calc ∫ x, (coord x - ∫ y, coord y ∂P) ^ 2 ∂P = variance coord P := (variance_eq_integral hcoord_meas.aemeasurable).symm _ = ∫ x, coord x ^ 2 ∂P - (∫ x, coord x ∂P) ^ 2 := by simpa only [Pi.pow_apply] using variance_eq_sub hcoordLp _ ≤ ∫ x, coord x ^ 2 ∂P := by nlinarith [sq_nonneg (∫ x, coord x ∂P)] _ ≤ ∫ x, B ^ 4 * q x ∂P := integral_mono_ae hcoordLp.integrable_sq hmajorant_int hsquare_bound _ = B ^ 4 * ∫ x, q x ∂P := by rw [integral_const_mul] _ = B ^ 4 * p := by rw [hp]

theorem localGram_integrable {X κ : Type*} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (phi : κ → X → ℝ) (hqmeas : Measurable q) (hphimeas : ∀ j, Measurable (phi j)) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) {B : ℝ} (hB : 0 ≤ B) (hphi : ∀ j, ∀ᵐ x ∂P, |phi j x| ≤ B) (j k : κ) : Integrable (fun x ↦ q x * phi j x * phi k x) P := by refine (integrable_const (μ := P) (B ^ 2)).mono' ((hqmeas.mul (hphimeas j)).mul (hphimeas k)).aestronglyMeasurable ?_ filter_upwards [hq, hphi j, hphi k] with x hx hphi_j hphi_k have hprod : |phi j x| * |phi k x| ≤ B * B := mul_le_mul hphi_j hphi_k (abs_nonneg _) hB calc ‖q x * phi j x * phi k x‖ = q x * (|phi j x| * |phi k x|) := by rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_of_nonneg hx.1] ring _ ≤ 1 * (B * B) := mul_le_mul hx.2 hprod (mul_nonneg (abs_nonneg _) (abs_nonneg _)) (by norm_num) _ = B ^ 2 := by ring

-- Proof route: triangle inequality, the entrywise bound, then -- `(∑ |v j|)^2 ≤ card κ * ∑ (v j)^2` by finite Cauchy--Schwarz. theorem entrywise_to_quadratic {κ : Type*} [Fintype κ] (E : κ → κ → ℝ) (v : κ → ℝ) {epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hE : ∀ j k, |E j k| ≤ epsilon) : |∑ j, ∑ k, v j * v k * E j k| ≤ (Fintype.card κ : ℝ) * epsilon * ∑ j, (v j) ^ 2 := by have hinner (j : κ) : (∑ k, |v j| * |v k| * epsilon) = |v j| * ((∑ k, |v k|) * epsilon) := by rw [Finset.sum_mul, Finset.mul_sum] apply Finset.sum_congr rfl intro k hk ring calc |∑ j, ∑ k, v j * v k * E j k| ≤ ∑ j, |∑ k, v j * v k * E j k| := by exact Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ j, ∑ k, |v j * v k * E j k| := by gcongr with j exact Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ j, ∑ k, |v j| * |v k| * epsilon := by gcongr with j k rw [abs_mul, abs_mul] exact mul_le_mul_of_nonneg_left (hE j k) (mul_nonneg (abs_nonneg _) (abs_nonneg _)) _ = epsilon * (∑ j, |v j|) ^ 2 := by simp_rw [hinner] rw [← Finset.sum_mul] ring _ ≤ epsilon * ((Fintype.card κ : ℝ) * ∑ j, |v j| ^ 2) := by gcongr simpa using (sq_sum_le_card_mul_sum_sq (s := univ) (f := fun j : κ => |v j|)) _ = (Fintype.card κ : ℝ) * epsilon * ∑ j, (v j) ^ 2 := by simp only [sq_abs] ring

theorem entrywise_gram_lower_bound {κ : Type*} [Fintype κ] (G M : κ → κ → ℝ) (v : κ → ℝ) {scale epsilon : ℝ} (hepsilon : 0 ≤ epsilon) (hentry : ∀ j k, |G j k - scale * M j k| ≤ epsilon) : scale * (∑ j, ∑ k, v j * v k * M j k) - (Fintype.card κ : ℝ) * epsilon * ∑ j, (v j) ^ 2 ≤ ∑ j, ∑ k, v j * v k * G j k := by let C : ℝ := (Fintype.card κ : ℝ) * epsilon * ∑ j, (v j) ^ 2 have habs : |∑ j, ∑ k, v j * v k * (G j k - scale * M j k)| ≤ C := by exact entrywise_to_quadratic (fun j k => G j k - scale * M j k) v hepsilon hentry have hscale : (∑ j, ∑ k, v j * v k * (scale * M j k)) = scale * (∑ j, ∑ k, v j * v k * M j k) := by calc (∑ j, ∑ k, v j * v k * (scale * M j k)) = ∑ j, ∑ k, scale * (v j * v k * M j k) := by apply Finset.sum_congr rfl intro j hj apply Finset.sum_congr rfl intro k hk ring _ = scale * (∑ j, ∑ k, v j * v k * M j k) := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro j hj rw [Finset.mul_sum] have hdiff : (∑ j, ∑ k, v j * v k * (G j k - scale * M j k)) = (∑ j, ∑ k, v j * v k * G j k) - scale * (∑ j, ∑ k, v j * v k * M j k) := by simp_rw [mul_sub, Finset.sum_sub_distrib] rw [hscale] have hneg := neg_le_of_abs_le habs rw [hdiff] at hneg dsimp [C] at hneg ⊢ linarith

theorem localizedGram_failure_subset_deviations {N : ℕ} {κ X : Type*} [Fintype κ] [Nonempty κ] (q : X → ℝ) (phi : κ → X → ℝ) (M : κ → κ → ℝ) {p lambda : ℝ} (hN : 0 < N) (hp : 0 < p) (hlambda : 0 < lambda) (hcoercive : ∀ v : κ → ℝ, lambda * p * (∑ j, (v j) ^ 2) ≤ ∑ j, ∑ k, v j * v k * M j k) : {omega : Fin N → X | ¬ LocalizedGramGood lambda q phi omega} ⊆ {omega : Fin N → X | (N : ℝ) * p / 2 ≤ |localCount q omega - (N : ℝ) * p| ∨ ∃ j k, lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ)) ≤ |localGramEntry q phi omega j k - (N : ℝ) * M j k|} := by intro omega hfailure change ¬ LocalizedGramGood lambda q phi omega at hfailure change (N : ℝ) * p / 2 ≤ |localCount q omega - (N : ℝ) * p| ∨ ∃ j k, lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ)) ≤ |localGramEntry q phi omega j k - (N : ℝ) * M j k| by_contra hdeviations have hcount : |localCount q omega - (N : ℝ) * p| < (N : ℝ) * p / 2 := by exact lt_of_not_ge (fun hge => hdeviations (inl hge)) have hentry : ∀ j k, |localGramEntry q phi omega j k - (N : ℝ) * M j k| < lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ)) := by intro j k exact lt_of_not_ge (fun hge => hdeviations (inr ⟨j, k, hge⟩)) exact hfailure (localizedGram_good_of_entrywise q phi M hN hp hlambda hcoercive omega hcount hentry)

theorem integral_sum_pi_eq {N : ℕ} {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : Integrable g μ) : ∫ ω, (∑ i : Fin N, g (ω i)) ∂(Measure.pi (fun _ : Fin N => μ)) = N * ∫ ω, g ω ∂μ := by let π : Measure (Fin N → Ω) := Measure.pi (fun _ : Fin N => μ) have hπ : ∀ i : Fin N, MeasurePreserving (Function.eval i) π μ := by intro i simpa [π] using measurePreserving_eval (fun _ : Fin N => μ) i change ∫ ω, (∑ i : Fin N, g (ω i)) ∂π = N * ∫ ω, g ω ∂μ calc ∫ ω, (∑ i : Fin N, g (ω i)) ∂π = ∑ i : Fin N, ∫ ω, g (ω i) ∂π := by rw [integral_finset_sum] intro i _ simpa [Function.comp_def] using (hπ i).integrable_comp_of_integrable hg _ = ∑ _i : Fin N, ∫ ω, g ω ∂μ := by apply Finset.sum_congr rfl intro i _ calc ∫ ω, g (ω i) ∂π = ∫ ω, g ω ∂Measure.map (Function.eval i) π := by refine (integral_map (hπ i).measurable.aemeasurable ?_).symm simpa [(hπ i).map_eq] using hg.aestronglyMeasurable _ = ∫ ω, g ω ∂μ := by rw [(hπ i).map_eq] _ = N * ∫ ω, g ω ∂μ := by simp [Finset.sum_const, nsmul_eq_mul]

theorem variance_sum_pi_eq {N : ℕ} {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (hg : MemLp g 2 μ) : Var[fun ω => ∑ i : Fin N, g (ω i); Measure.pi (fun _ : Fin N => μ)] = N * Var[g; μ] := by rw [show (fun ω : Fin N → Ω => ∑ i : Fin N, g (ω i)) = (∑ i : Fin N, fun ω : Fin N → Ω => g (ω i)) by ext ω simp [Finset.sum_apply]] simpa [Finset.sum_const, nsmul_eq_mul] using (ProbabilityTheory.variance_sum_pi (μ := fun _ : Fin N => μ) (X := fun _ : Fin N => g) (fun _ : Fin N => hg))

theorem linftyOp_abs_entry_le {α β R : Type*} [Fintype α] [Fintype β] [NormedAddCommGroup R] (A : Matrix α β R) (i : α) (j : β) : ‖A i j‖ ≤ ‖A‖ := by rw [Matrix.linfty_opNorm_def] have hrow : ‖A i j‖₊ ≤ ∑ k, ‖A i k‖₊ := Finset.single_le_sum (s := univ) (f := fun k => ‖A i k‖₊) (fun _ _ => zero_le) (Finset.mem_univ j) have hsup : (∑ k, ‖A i k‖₊) ≤ Finset.univ.sup (fun i => ∑ k, ‖A i k‖₊) := Finset.le_sup (s := univ) (f := fun i => ∑ k, ‖A i k‖₊) (Finset.mem_univ i) exact_mod_cast le_trans hrow hsup

theorem linftyOp_norm_le_of_rowsum {α β R : Type*} [Fintype α] [Fintype β] [NormedAddCommGroup R] {A : Matrix α β R} {c : ℝ} (hc : 0 ≤ c) (h : ∀ i, (∑ j, ‖A i j‖) ≤ c) : ‖A‖ ≤ c := by rw [Matrix.linfty_opNorm_def] have hsup : Finset.univ.sup (fun i => ∑ j, ‖A i j‖₊) ≤ c.toNNReal := by refine Finset.sup_le ?_ intro i _ exact NNReal.coe_le_coe.mp (by rw [NNReal.coe_sum, Real.coe_toNNReal c hc] simpa using h i) calc ↑(Finset.univ.sup fun i => ∑ j, ‖A i j‖₊) ≤ (c.toNNReal : ℝ) := NNReal.coe_le_coe.mpr hsup _ = c := Real.coe_toNNReal c hc

theorem linftyOp_norm_le_of_entry {q : ℕ} {A : Matrix (Fin (p + 1)) (Fin (q + 1)) ℝ} {η : ℝ} (h : ∀ i j, |A i j| ≤ η) : ‖A‖ ≤ (q + 1 : ℕ) * η := by have hη : 0 ≤ η := le_trans (abs_nonneg (A 0 0)) (h 0 0) apply linftyOp_norm_le_of_rowsum (mul_nonneg (by positivity) hη) intro i calc ∑ j, |A i j| ≤ ∑ _j : Fin (q + 1), η := Finset.sum_le_sum (fun j _ => h i j) _ = (q + 1 : ℕ) * η := by simp [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]

theorem designInv_perturb (S M : Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) (hS : IsUnit S.det) {η c : ℝ} (hSrow : ∀ i, (∑ j, |S⁻¹ i j|) ≤ c) (hclose : ∀ j k, |M j k - S j k| ≤ η) (hsmall : c * ((p + 1 : ℕ) * η) ≤ 1 / 2) {i j : Fin (p + 1)} : IsUnit M.det ∧ |M⁻¹ i j - S⁻¹ i j| ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by haveI : CompleteSpace (Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ) := completeSpace_matrix_linftyOp let R := Matrix (Fin (p + 1)) (Fin (p + 1)) ℝ have hSu : IsUnit S := (Matrix.isUnit_iff_isUnit_det S).mpr hS set Su : Rˣ := hSu.unit with hSu_def have hval : (↑Su : R) = S := by rw [hSu_def] exact hSu.unit_spec have hinv : (↑Su⁻¹ : R) = S⁻¹ := by rw [Matrix.coe_units_inv, hval] have hc : 0 ≤ c := le_trans (sum_nonneg fun _ _ => abs_nonneg _) (hSrow 0) have hSinv_norm : ‖(↑Su⁻¹ : R)‖ ≤ c := by rw [hinv] exact linftyOp_norm_le_of_rowsum hc hSrow have hMS_norm : ‖M - S‖ ≤ (p + 1 : ℕ) * η := linftyOp_norm_le_of_entry (by intro i j simpa [Matrix.sub_apply] using hclose i j) have hη : 0 ≤ η := le_trans (abs_nonneg (M 0 0 - S 0 0)) (hclose 0 0) have hdimη : 0 ≤ (p + 1 : ℕ) * η := mul_nonneg (by positivity) hη set u : R := (↑Su⁻¹ : R) * (S - M) with hu_def have hu_le : ‖u‖ ≤ c * ((p + 1 : ℕ) * η) := by calc ‖u‖ = ‖(↑Su⁻¹ : R) * (S - M)‖ := by rw [hu_def] _ ≤ ‖(↑Su⁻¹ : R)‖ * ‖S - M‖ := norm_mul_le _ _ _ = ‖(↑Su⁻¹ : R)‖ * ‖M - S‖ := by rw [norm_sub_rev S M] _ ≤ c * ((p + 1 : ℕ) * η) := by simpa [mul_comm] using mul_le_mul hMS_norm hSinv_norm (norm_nonneg _) hdimη have huhalf : ‖u‖ ≤ 1 / 2 := le_trans hu_le hsmall have hu1 : ‖u‖ < 1 := by have hunonneg : 0 ≤ ‖u‖ := norm_nonneg u nlinarith set v : Rˣ := Units.oneSub u hu1 with hv_def have hinvS : (↑Su⁻¹ : R) * S = 1 := by rw [← hval] exact_mod_cast Su.inv_mul have hSmulinv : S * (↑Su⁻¹ : R) = 1 := by rw [← hval] exact Su.mul_inv have hvval : (↑v : R) = (↑Su⁻¹ : R) * M := by rw [hv_def] change (1 : R) - u = (↑Su⁻¹ : R) * M rw [hu_def] calc (1 : R) - (↑Su⁻¹ : R) * (S - M) = (↑Su⁻¹ : R) * S - (↑Su⁻¹ : R) * (S - M) := by rw [hinvS] _ = (↑Su⁻¹ : R) * (S - (S - M)) := by rw [← mul_sub] _ = (↑Su⁻¹ : R) * M := by simp set Munit : Rˣ := Su * v with hM_def have hMval : (↑Munit : R) = M := by rw [hM_def] change ((↑Su : R) * (↑v : R)) = M rw [hval, hvval, ← mul_assoc, hSmulinv, one_mul] have hMunit : IsUnit M := hMval ▸ Munit.isUnit have hMdet : IsUnit M.det := (Matrix.isUnit_iff_isUnit_det M).mp hMunit have hMinv_eq : (↑Munit⁻¹ : R) = M⁻¹ := by rw [Matrix.coe_units_inv, hMval] have hvinv_norm : ‖(↑v⁻¹ : R)‖ ≤ (1 - ‖u‖)⁻¹ := by rw [hv_def] change ‖∑' n : ℕ, u ^ n‖ ≤ (1 - ‖u‖)⁻¹ have hgeo := tsum_geometric_le_of_norm_lt_one u hu1 rw [norm_one, sub_self, zero_add] at hgeo exact hgeo have hvinv2 : ‖(↑v⁻¹ : R)‖ ≤ 2 := by have hhalf_le : (1 / 2 : ℝ) ≤ 1 - ‖u‖ := by linarith have hhalf_pos : 0 < (1 / 2 : ℝ) := by norm_num have hinv_le : (1 - ‖u‖)⁻¹ ≤ 2 := by have hden_pos : 0 < 1 - ‖u‖ := by linarith calc (1 - ‖u‖)⁻¹ ≤ ((1 / 2 : ℝ)⁻¹) := (inv_le_inv₀ hden_pos hhalf_pos).mpr hhalf_le _ = 2 := by norm_num exact le_trans hvinv_norm hinv_le have hMunitinv_norm : ‖(↑Munit⁻¹ : R)‖ ≤ 2 * c := by calc ‖(↑Munit⁻¹ : R)‖ = ‖(↑v⁻¹ : R) * (↑Su⁻¹ : R)‖ := by rw [hM_def] rw [_root_.mul_inv_rev] rfl _ ≤ ‖(↑v⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ := norm_mul_le _ _ _ ≤ 2 * c := by exact mul_le_mul hvinv2 hSinv_norm (norm_nonneg _) (by norm_num) have hdiff_norm : ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by have hres := norm_unitInv_sub_unitInv_le Munit Su calc ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ ≤ ‖(↑Munit⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ * ‖(↑Munit : R) - ↑Su‖ := hres _ ≤ (2 * c) * c * ((p + 1 : ℕ) * η) := by have hdiff_mat : ‖(↑Munit : R) - ↑Su‖ ≤ (p + 1 : ℕ) * η := by simpa [hMval, hval] using hMS_norm have hAB : ‖(↑Munit⁻¹ : R)‖ * ‖(↑Su⁻¹ : R)‖ ≤ (2 * c) * c := mul_le_mul hMunitinv_norm hSinv_norm (norm_nonneg _) (by positivity) have hD_nonneg : 0 ≤ ‖(↑Munit : R) - ↑Su‖ := norm_nonneg _ have hC_nonneg : 0 ≤ (2 * c) * c := by positivity exact le_trans (mul_le_mul_of_nonneg_right hAB hD_nonneg) (mul_le_mul_of_nonneg_left hdiff_mat hC_nonneg) _ = 2 * c ^ 2 * ((p + 1 : ℕ) * η) := by ring refine ⟨hMdet, ?_⟩ calc |M⁻¹ i j - S⁻¹ i j| = |(((↑Munit⁻¹ : R) - ↑Su⁻¹) i j)| := by rw [← hMinv_eq, ← hinv, Matrix.sub_apply] _ ≤ ‖(↑Munit⁻¹ : R) - ↑Su⁻¹‖ := linftyOp_abs_entry_le ((↑Munit⁻¹ : R) - ↑Su⁻¹) i j _ ≤ 2 * c ^ 2 * ((p + 1 : ℕ) * η) := hdiff_norm

theorem localized_empiricalGram_coercive_of_pos {N : ℕ} {κ X : Type*} [Fintype κ] [Nonempty κ] [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] (q : X → ℝ) (phi : κ → X → ℝ) (hqmeas : Measurable q) (hphimeas : ∀ j, Measurable (phi j)) {p lambda B : ℝ} (hN : 0 < N) (hp : 0 < p) (hlambda : 0 < lambda) (hB : 0 ≤ B) (hq : ∀ᵐ x ∂P, 0 ≤ q x ∧ q x ≤ 1) (hphi : ∀ j, ∀ᵐ x ∂P, |phi j x| ≤ B) (hmass : ∫ x, q x ∂P = p) (hcoercive : ∀ v : κ → ℝ, lambda * p * (∑ j, (v j) ^ 2) ≤ ∑ j, ∑ k, v j * v k * ∫ x, q x * phi j x * phi k x ∂P) : (Measure.pi (fun _ : Fin N ↦ P)).real {omega : Fin N → X | ¬ LocalizedGramGood lambda q phi omega} ≤ 2 * (1 + (Fintype.card κ : ℝ) * (Fintype.card κ : ℝ)) * exp (-(N : ℝ) * p * localizedGramRate κ lambda B) := by let M : κ → κ → ℝ := fun j k ↦ ∫ x, q x * phi j x * phi k x ∂P let ι := Option (κ × κ) let g : ι → X → ℝ := fun a x ↦ match a with | none => q x | some jk => q x * phi jk.1 x * phi jk.2 x let b : ι → ℝ := fun a ↦ match a with | none => 1 | some _ => 2 * B ^ 2 let sigma2 : ι → ℝ := fun a ↦ match a with | none => p | some _ => B ^ 4 * p let eta : ι → ℝ := fun a ↦ match a with | none => (N : ℝ) * p / 2 | some _ => lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ)) have hNreal : (0 : ℝ) < (N : ℝ) := by exact_mod_cast hN have hNp : 0 < (N : ℝ) * p := mul_pos hNreal hp have hd : (0 : ℝ) < (Fintype.card κ : ℝ) := by exact_mod_cast Fintype.card_pos have hgmeas : ∀ a, Measurable (g a) := by intro a cases a with | none => simpa [g] using hqmeas | some jk => change Measurable (fun x ↦ q x * phi jk.1 x * phi jk.2 x) exact (hqmeas.mul (hphimeas jk.1)).mul (hphimeas jk.2) have hgint : ∀ a, Integrable (g a) P := by intro a cases a with | none => simpa [g] using localWeight_integrable P q hqmeas hq | some jk => simpa [g] using localGram_integrable P q phi hqmeas hphimeas hq hB hphi jk.1 jk.2 have hb : ∀ a, 0 ≤ b a := by intro a cases a <;> simp [b, sq_nonneg] have hsigma2 : ∀ a, 0 ≤ sigma2 a := by intro a cases a · simpa [sigma2] using le_of_lt hp · dsimp [sigma2] positivity have heta : ∀ a, 0 < eta a := by intro a cases a · simpa [eta] using div_pos hNp (by norm_num : (0 : ℝ) < 2) · dsimp [eta] positivity have henvelope : ∀ a, ∀ᵐ x ∂P, |g a x - ∫ y, g a y ∂P| ≤ b a := by intro a cases a with | none => simpa [g, b, hmass] using localWeight_centered_envelope P q hq hmass | some jk => simpa [g, b] using localGram_centered_envelope P q phi hq hB hphi jk.1 jk.2 have hvariance : ∀ a, ∫ x, (g a x - ∫ y, g a y ∂P) ^ 2 ∂P ≤ sigma2 a := by intro a cases a with | none => simpa [g, sigma2] using localWeight_centered_secondMoment_le P q hqmeas hq hmass | some jk => simpa [g, sigma2] using localGram_centered_secondMoment_le P q phi hqmeas hphimeas hq hB hphi hmass jk.1 jk.2 have hbern := iid_sum_bernstein_union_bound P g hgmeas hgint b sigma2 eta hb hsigma2 heta hN henvelope hvariance have hsubset : {omega : Fin N → X | ¬ LocalizedGramGood lambda q phi omega} ⊆ {omega : Fin N → X | ∃ a, eta a ≤ |(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|} := by intro omega hfail have hdev := localizedGram_failure_subset_deviations q phi M hN hp hlambda hcoercive hfail rcases hdev with hcount | ⟨j, k, hentry⟩ · refine ⟨none, ?_⟩ simpa [eta, g, localCount, hmass] using hcount · refine ⟨some (j, k), ?_⟩ simpa [eta, g, M, localGramEntry] using hentry calc (Measure.pi (fun _ : Fin N ↦ P)).real {omega : Fin N → X | ¬ LocalizedGramGood lambda q phi omega} ≤ (Measure.pi (fun _ : Fin N ↦ P)).real {omega : Fin N → X | ∃ a, eta a ≤ |(∑ i, g a (omega i)) - (N : ℝ) * ∫ x, g a x ∂P|} := measureReal_mono hsubset _ ≤ ∑ a, 2 * exp (-(eta a) ^ 2 / (2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) := hbern _ ≤ 2 * (1 + (Fintype.card κ : ℝ) * (Fintype.card κ : ℝ)) * exp (-(N : ℝ) * p * localizedGramRate κ lambda B) := by by_cases hB0 : B = 0 · have hrate0 : localizedGramRate κ lambda B = 0 := by simp [localizedGramRate, hB0] calc ∑ a, 2 * exp (-(eta a) ^ 2 / (2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) ≤ ∑ _a : ι, 2 * 1 := by apply Finset.sum_le_sum intro a ha gcongr rw [Real.exp_le_one_iff] have hden : 0 ≤ 2 * (2 * (N : ℝ) * sigma2 a + b a * eta a) := by exact mul_nonneg (by norm_num) (add_nonneg (mul_nonneg (mul_nonneg (by norm_num) (le_of_lt hNreal)) (hsigma2 a)) (mul_nonneg (hb a) (le_of_lt (heta a)))) exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) hden _ = 2 * (1 + (Fintype.card κ : ℝ) * (Fintype.card κ : ℝ)) := by simp [ι, Fintype.card_option, Fintype.card_prod] ring _ = 2 * (1 + (Fintype.card κ : ℝ) * (Fintype.card κ : ℝ)) * exp (-(N : ℝ) * p * localizedGramRate κ lambda B) := by rw [hrate0] simp · have hBpos : 0 < B := lt_of_le_of_ne hB (Ne.symm hB0) have hrate_count : localizedGramRate κ lambda B ≤ (1 / 20 : ℝ) := min_le_left _ _ have hrate_entry : localizedGramRate κ lambda B ≤ lambda ^ 2 / (16 * (Fintype.card κ : ℝ) * (4 * (Fintype.card κ : ℝ) * B ^ 4 + B ^ 2 * lambda)) := min_le_right _ _ have hcoord : ∀ a, (N : ℝ) * p * localizedGramRate κ lambda B ≤ (eta a) ^ 2 / (2 * (2 * (N : ℝ) * sigma2 a + b a * eta a)) := by intro a cases a with | none => have hmul := mul_le_mul_of_nonneg_left hrate_count (le_of_lt hNp) dsimp [eta, sigma2, b] have hid : (((N : ℝ) * p / 2) ^ 2 / (2 * (2 * (N : ℝ) * p + 1 * ((N : ℝ) * p / 2)))) = (N : ℝ) * p * (1 / 20 : ℝ) := by field_simp [ne_of_gt hNreal, ne_of_gt hp] ring rw [hid] exact hmul | some jk => have hmul := mul_le_mul_of_nonneg_left hrate_entry (le_of_lt hNp) dsimp [eta, sigma2, b] have hid : ((lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ))) ^ 2 / (2 * (2 * (N : ℝ) * (B ^ 4 * p) + 2 * B ^ 2 * (lambda * (N : ℝ) * p / (4 * (Fintype.card κ : ℝ)))))) = (N : ℝ) * p * (lambda ^ 2 / (16 * (Fintype.card κ : ℝ) * (4 * (Fintype.card κ : ℝ) * B ^ 4 + B ^ 2 * lambda))) := by field_simp [ne_of_gt hNreal, ne_of_gt hp, ne_of_gt hd, ne_of_gt hBpos, ne_of_gt hlambda] ring rw [hid] exact hmul calc ∑ a, 2 * exp (-(eta a) ^ 2 / (2 * (2 * (N : ℝ) * sigma2 a + b a * eta a))) ≤ ∑ _a : ι, 2 * exp (-(N : ℝ) * p * localizedGramRate κ lambda B) := by apply Finset.sum_le_sum intro a ha gcongr calc -(eta a) ^ 2 / (2 * (2 * (N : ℝ) * sigma2 a + b a * eta a)) ≤ -((N : ℝ) * p * localizedGramRate κ lambda B) := by simpa only [neg_div] using neg_le_neg (hcoord a) _ = -(N : ℝ) * p * localizedGramRate κ lambda B := by ring _ = 2 * (1 + (Fintype.card κ : ℝ) * (Fintype.card κ : ℝ)) * exp (-(N : ℝ) * p * localizedGramRate κ lambda B) := by simp [ι, Fintype.card_option, Fintype.card_prod] ring