PL1/FiniteGrothendieck.lean
All source files · Download exact source
SHA-256: 77c3c86b6dab1ce5732fcd3f6534f56c4f809d3a64c8a9a6292355b8068179f4
1import PL1.FiniteGrothendieckNormalization23/-! A dimension-independent real finite Grothendieck inequality with constant 128,4using concrete finite Rademacher moments, clipping at 8, and a bounded supremum. -/5noncomputable section6set_option backward.isDefEq.respectTransparency false7open scoped BigOperators8namespace PL1.FiniteGrothendieck9open PL1.Bonami PL1.FiniteRademacherClipping1011def form {r c d : ℕ} (a : Fin r → Fin c → ℝ)12 (u : Fin r → Fin d → ℝ) (v : Fin c → Fin d → ℝ) : ℝ :=13 ∑ i, ∑ j, a i j * (∑ l, u i l * v j l)1415def values {r c : ℕ} (a : Fin r → Fin c → ℝ) : Set ℝ :=16 {z | ∃ (d : ℕ) (u : Fin r → Fin d → ℝ) (v : Fin c → Fin d → ℝ),17 (∀ i, ∑ l, (u i l) ^ 2 ≤ 1) ∧ (∀ j, ∑ l, (v j l) ^ 2 ≤ 1) ∧ z = |form a u v|}1819theorem zero_mem_values {r c : ℕ} (a : Fin r → Fin c → ℝ) : 0 ∈ values a := by20 refine ⟨0, fun _ _ => 0, fun _ _ => 0, ?_, ?_, ?_⟩ <;> simp [form]2122theorem inner_le_one {d : ℕ} (u v : Fin d → ℝ)23 (hu : ∑ l, (u l)^2 ≤ 1) (hv : ∑ l, (v l)^2 ≤ 1) :24 |∑ l, u l * v l| ≤ 1 := by25 have h := Finset.sum_mul_sq_le_sq_mul_sq (Finset.univ : Finset (Fin d)) u v26 have hv0 : 0 ≤ ∑ l, (v l)^2 := Finset.sum_nonneg (fun _ _ => sq_nonneg _)27 have hh := mul_le_mul_of_nonneg_right hu hv028 have ha := abs_nonneg (∑ l, u l * v l)29 rw [← sq_abs] at h30 nlinarith3132theorem values_bddAbove {r c : ℕ} (a : Fin r → Fin c → ℝ) : BddAbove (values a) := by33 refine ⟨∑ i, ∑ j, |a i j|, ?_⟩34 rintro z ⟨d, u, v, hu, hv, rfl⟩35 calc36 |form a u v| ≤ ∑ i, |∑ j, a i j * (∑ l, u i l * v j l)| :=37 Finset.abs_sum_le_sum_abs _ _38 _ ≤ ∑ i, ∑ j, |a i j| := by39 apply Finset.sum_le_sum40 intro i _41 calc42 _ ≤ ∑ j, |a i j * (∑ l, u i l * v j l)| := Finset.abs_sum_le_sum_abs _ _43 _ ≤ _ := Finset.sum_le_sum (fun j _ => by44 rw [abs_mul]45 exact (mul_le_mul_of_nonneg_left (inner_le_one _ _ (hu i) (hv j))46 (abs_nonneg _)).trans_eq (mul_one _))4748def bound {r c : ℕ} (a : Fin r → Fin c → ℝ) : ℝ := sSup (values a)4950theorem bound_nonneg {r c : ℕ} (a : Fin r → Fin c → ℝ) : 0 ≤ bound a :=51 le_csSup (values_bddAbove a) (zero_mem_values a)5253theorem form_le_bound {r c d : ℕ} (a : Fin r → Fin c → ℝ)54 (u : Fin r → Fin d → ℝ) (v : Fin c → Fin d → ℝ)55 (hu : ∀ i, ∑ l, (u i l)^2 ≤ 1) (hv : ∀ j, ∑ l, (v j l)^2 ≤ 1) :56 |form a u v| ≤ bound a :=57 le_csSup (values_bddAbove a) ⟨d, u, v, hu, hv, rfl⟩5859def cubeForm {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)60 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ) : ℝ :=61 average n (fun x => ∑ i, ∑ j, a i j * (f i x * g j x))6263theorem cubeForm_eq {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)64 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ) :65 cubeForm a n f g = form a (fun i => coordinates n (f i)) (fun j => coordinates n (g j)) := by66 simp only [cubeForm, form, average_sum, average_mul, coordinates_product]6768theorem cubeForm_le_bound {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)69 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ)70 (hf : ∀ i, average n (fun x => (f i x)^2) ≤ 1)71 (hg : ∀ j, average n (fun x => (g j x)^2) ≤ 1) :72 |cubeForm a n f g| ≤ bound a := by73 rw [cubeForm_eq]74 exact form_le_bound a _ _ (by simpa only [coordinates_square] using hf)75 (by simpa only [coordinates_square] using hg)7677theorem cubeForm_mul_left {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)78 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ) (t : ℝ) :79 cubeForm a n (fun i x => t * f i x) g = t * cubeForm a n f g := by80 simp only [cubeForm, ← average_mul, Finset.mul_sum]81 apply average_congr82 intro x83 apply Finset.sum_congr rfl84 intro i _85 apply Finset.sum_congr rfl86 intro j _87 ring8889theorem cubeForm_mul_right {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)90 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ) (t : ℝ) :91 cubeForm a n f (fun j x => t * g j x) = t * cubeForm a n f g := by92 simp only [cubeForm, ← average_mul, Finset.mul_sum]93 apply average_congr94 intro x95 apply Finset.sum_congr rfl96 intro i _97 apply Finset.sum_congr rfl98 intro j _99 ring100101102103theorem cubeForm_clipping_le {r c : ℕ} (a : Fin r → Fin c → ℝ) (n : ℕ)104 (f : Fin r → Cube n → ℝ) (g : Fin c → Cube n → ℝ) (D : ℝ)105 (hscalar : ∀ (s : Fin r → ℝ) (t : Fin c → ℝ),106 (∀ i, |s i| ≤ 1) → (∀ j, |t j| ≤ 1) →107 |∑ i, ∑ j, a i j * s i * t j| ≤ D)108 (hf : ∀ i, average n (fun x => (f i x)^2) ≤ 1)109 (hg : ∀ j, average n (fun x => (g j x)^2) ≤ 1)110 (hr : ∀ i, average n (fun x => (f i x - clipEight (f i x))^2) ≤ 1 / 16)111 (hs : ∀ j, average n (fun x => (g j x - clipEight (g j x))^2) ≤ 1 / 16) :112 |cubeForm a n f g| ≤ 64 * D + bound a / 2 := by113 let C : Fin r → Cube n → ℝ := fun i x => clipEight (f i x)114 let E : Fin c → Cube n → ℝ := fun j x => clipEight (g j x)115 let R : Fin r → Cube n → ℝ := fun i x => f i x - C i x116 let S : Fin c → Cube n → ℝ := fun j x => g j x - E j x117 have hC (i) : average n (fun x => (C i x)^2) ≤ 1 :=118 (average_mono n (fun x => clipEight_sq_le (f i x))).trans (hf i)119 have hR (i) : average n (fun x => (4 * R i x)^2) ≤ 1 := by120 have he : (fun x => (4 * R i x)^2) = (fun x => 16 * (R i x)^2) := by funext x; ring121 rw [he, average_mul]122 have hh := hr i123 change average n (fun x => (R i x)^2) ≤ 1 / 16 at hh124 linarith125 have hS (j) : average n (fun x => (4 * S j x)^2) ≤ 1 := by126 have he : (fun x => (4 * S j x)^2) = (fun x => 16 * (S j x)^2) := by funext x; ring127 rw [he, average_mul]128 have hh := hs j129 change average n (fun x => (S j x)^2) ≤ 1 / 16 at hh130 linarith131 have hresL : |cubeForm a n R g| ≤ bound a / 4 := by132 have h := cubeForm_le_bound a n (fun i x => 4 * R i x) g hR hg133 rw [cubeForm_mul_left, abs_mul] at h134 norm_num at h135 linarith136 have hresR : |cubeForm a n C S| ≤ bound a / 4 := by137 have h := cubeForm_le_bound a n C (fun j x => 4 * S j x) hC hS138 rw [cubeForm_mul_right, abs_mul] at h139 norm_num at h140 linarith141 have hclip : |cubeForm a n C E| ≤ 64 * D := by142 apply abs_average_le143 intro x144 have hc (z : ℝ) : |clipEight z / 8| ≤ 1 := by145 rw [abs_div]146 norm_num147 exact (div_le_one (by norm_num : (0 : ℝ) < 8)).mpr (abs_clipEight_le z)148 have h := hscalar (fun i => C i x / 8) (fun j => E j x / 8)149 (fun i => hc (f i x)) (fun j => hc (g j x))150 have he : (∑ i, ∑ j, a i j * (C i x * E j x)) =151 64 * (∑ i, ∑ j, a i j * (C i x / 8) * (E j x / 8)) := by152 simp only [Finset.mul_sum]153 apply Finset.sum_congr rfl154 intro i _155 apply Finset.sum_congr rfl156 intro j _157 ring158 rw [he, abs_mul]159 norm_num160 nlinarith161 have he : cubeForm a n f g = cubeForm a n C E + cubeForm a n R g + cubeForm a n C S := by162 simp only [cubeForm, ← average_add, ← Finset.sum_add_distrib]163 apply average_congr164 intro x165 apply Finset.sum_congr rfl166 intro i _167 apply Finset.sum_congr rfl168 intro j _169 dsimp [R, S]170 ring171 rw [he]172 calc173 _ ≤ |cubeForm a n C E + cubeForm a n R g| + |cubeForm a n C S| := abs_add_le _ _174 _ ≤ (|cubeForm a n C E| + |cubeForm a n R g|) + |cubeForm a n C S| :=175 add_le_add (abs_add_le _ _) le_rfl176 _ ≤ 64 * D + bound a / 2 := by linarith177178theorem form_clipping_le {r c d : ℕ} (a : Fin r → Fin c → ℝ)179 (u : Fin r → Fin d → ℝ) (v : Fin c → Fin d → ℝ) (D : ℝ)180 (hu : ∀ i, ∑ l, (u i l)^2 ≤ 1) (hv : ∀ j, ∑ l, (v j l)^2 ≤ 1)181 (hscalar : ∀ (s : Fin r → ℝ) (t : Fin c → ℝ),182 (∀ i, |s i| ≤ 1) → (∀ j, |t j| ≤ 1) →183 |∑ i, ∑ j, a i j * s i * t j| ≤ D) :184 |form a u v| ≤ 64 * D + bound a / 2 := by185 let f := fun i => rademacherSum d (finExtend (u i))186 let g := fun j => rademacherSum d (finExtend (v j))187 have hf i : energy d (finExtend (u i)) ≤ 1 := by rw [energy_extend]; exact hu i188 have hg j : energy d (finExtend (v j)) ≤ 1 := by rw [energy_extend]; exact hv j189 have he : cubeForm a d f g = form a u v := by190 simp only [cubeForm, form, f, g, average_sum, average_mul, mixed_extend]191 rw [← he]192 exact cubeForm_clipping_le a d f g D hscalar193 (fun i => by dsimp [f]; rw [second_moment]; exact hf i)194 (fun j => by dsimp [g]; rw [second_moment]; exact hg j)195 (fun i => residual_second_moment_le d _ (hf i))196 (fun j => residual_second_moment_le d _ (hg j))197198theorem bound_le {r c : ℕ} (a : Fin r → Fin c → ℝ) (D : ℝ)199 (hscalar : ∀ (s : Fin r → ℝ) (t : Fin c → ℝ),200 (∀ i, |s i| ≤ 1) → (∀ j, |t j| ≤ 1) →201 |∑ i, ∑ j, a i j * s i * t j| ≤ D) : bound a ≤ 128 * D := by202 have h : bound a ≤ 64 * D + bound a / 2 := by203 apply csSup_le ⟨0, zero_mem_values a⟩204 rintro z ⟨d, u, v, hu, hv, rfl⟩205 exact form_clipping_le a u v D hu hv hscalar206 linarith207208end PL1.FiniteGrothendieck209210namespace PL1.FiniteSumming211open PL1.FiniteGrothendieck212213theorem matrixGrothendieckWith_128 : MatrixGrothendieckWith 128 := by214 refine ⟨by norm_num, ?_⟩215 intro r c d a u v D hu hv hscalar216 exact (form_le_bound a u v hu hv).trans (bound_le a D hscalar)217218theorem twoSumming_128 (d k : ℕ) (T : (Fin d → ℝ) →L[ℝ] EllOne k) :219 PL1.ComplementedLattice.TwoSummingWith T (128 * ‖T‖) :=220 twoSumming_of_matrix matrixGrothendieckWith_128 d k T221222theorem oneSumming_128 (d k : ℕ) (S : EllOne d →L[ℝ] EuclideanSpace ℝ (Fin k)) :223 PL1.ComplementedLattice.OneSummingWith S (128 * ‖S‖) :=224 oneSumming_of_matrix matrixGrothendieckWith_128 d k S225226#print axioms matrixGrothendieckWith_128227#print axioms twoSumming_128228#print axioms oneSumming_128229end PL1.FiniteSumming230231232233