PL1/FiniteSummingFromMatrix.lean
All source files · Download exact source
SHA-256: 6d4aa9ec79bd1f4593fba357aab9834d789a22abe5a8657469ab420fcf7cb91c
1import PL1.ComplementedLatticeSumming2import Mathlib.Analysis.Normed.Lp.PiLp3import Mathlib.Tactic.FieldSimp4import Mathlib.Tactic.Ring56/-!7Finite operator deductions. The matrix Grothendieck inequality8is an explicit hypothesis. No proof of that hypothesis is claimed here.9-/1011noncomputable section12open scoped BigOperators1314namespace PL1.FiniteSumming15open PL1.ComplementedLattice1617/-- Coordinate form of finite real Grothendieck: the square-sum hypotheses18are exactly Euclidean unit-ball constraints. All dimensions are independent. -/19def MatrixGrothendieckWith (G : ℝ) : Prop :=20 0 ≤ G ∧ ∀ (r c d : ℕ) (a : Fin r → Fin c → ℝ)21 (u : Fin r → Fin d → ℝ) (v : Fin c → Fin d → ℝ) (B : ℝ),22 (∀ i, ∑ l, (u i l) ^ 2 ≤ 1) →23 (∀ j, ∑ l, (v j l) ^ 2 ≤ 1) →24 (∀ (s : Fin r → ℝ) (t : Fin c → ℝ),25 (∀ i, |s i| ≤ 1) → (∀ j, |t j| ≤ 1) →26 |∑ i, ∑ j, a i j * s i * t j| ≤ B) →27 |∑ i, ∑ j, a i j * (∑ l, u i l * v j l)| ≤ G * B2829abbrev EllOne (k : ℕ) := PiLp 1 (fun _ : Fin k => ℝ)3031theorem norm_ellOne (k : ℕ) (x : EllOne k) : ‖x‖ = ∑ l, |x l| := by32 simpa only [Real.norm_eq_abs] using PiLp.norm_eq_of_L1 x3334def signOne (a : ℝ) : ℝ := if 0 ≤ a then 1 else -13536theorem signOne_sq (a : ℝ) : signOne a ^ 2 = 1 := by37 unfold signOne38 split <;> norm_num3940theorem signOne_mul (a : ℝ) : signOne a * a = |a| := by41 unfold signOne42 split_ifs with h43 · simp [abs_of_nonneg h]44 · simp [abs_of_neg (lt_of_not_ge h)]4546theorem scalar_expansion {d : ℕ} (φ : (Fin d → ℝ) →L[ℝ] ℝ) (x : Fin d → ℝ) :47 ∑ j, φ (Pi.single j 1) * x j = φ x := by48 have hx : ∑ j, x j • Pi.single j (1 : ℝ) = x := by49 ext i50 simp [Pi.single_apply, Finset.sum_apply]51 calc52 _ = φ (∑ j, x j • Pi.single j (1 : ℝ)) := by53 rw [map_sum]54 simp only [map_smul, smul_eq_mul]55 apply Finset.sum_congr rfl56 intro j _57 ring58 _ = φ x := by rw [hx]5960def entry {d k : ℕ} (T : (Fin d → ℝ) →L[ℝ] EllOne k) (l : Fin k) (j : Fin d) : ℝ :=61 T (Pi.single j 1) l6263theorem entry_apply {d k : ℕ} (T : (Fin d → ℝ) →L[ℝ] EllOne k)64 (x : Fin d → ℝ) (l : Fin k) : ∑ j, entry T l j * x j = T x l := by65 exact scalar_expansion ((PiLp.proj 1 (fun _ : Fin k => ℝ) l).comp T) x6667theorem entry_scalar_bound {d k : ℕ} (T : (Fin d → ℝ) →L[ℝ] EllOne k)68 (s : Fin k → ℝ) (t : Fin d → ℝ) (hs : ∀ l, |s l| ≤ 1) (ht : ∀ j, |t j| ≤ 1) :69 |∑ l, ∑ j, entry T l j * s l * t j| ≤ ‖T‖ := by70 have he : (∑ l, ∑ j, entry T l j * s l * t j) = ∑ l, s l * T t l := by71 apply Finset.sum_congr rfl72 intro l _73 rw [← entry_apply T t l, Finset.mul_sum]74 apply Finset.sum_congr rfl75 intro j _76 ring77 rw [he]78 calc79 _ ≤ ∑ l, |s l * T t l| := Finset.abs_sum_le_sum_abs _ _80 _ ≤ ∑ l, |T t l| := by81 apply Finset.sum_le_sum82 intro l _83 rw [abs_mul]84 exact mul_le_of_le_one_left (abs_nonneg _) (hs l)85 _ = ‖T t‖ := (norm_ellOne k _).symm86 _ ≤ ‖T‖ * ‖t‖ := T.le_opNorm _87 _ ≤ ‖T‖ := by88 have ht' : ‖t‖ ≤ 1 := (pi_norm_le_iff_of_nonneg zero_le_one).mpr ht89 simpa only [mul_one] using mul_le_mul_of_nonneg_left ht' (norm_nonneg T)9091theorem rearrange {k d n : ℕ} (a : Fin k → Fin d → ℝ)92 (u : Fin k → Fin n → ℝ) (v : Fin d → Fin n → ℝ) :93 (∑ l, ∑ j, a l j * (∑ i, u l i * v j i)) =94 ∑ i, ∑ l, u l i * (∑ j, a l j * v j i) := by95 simp_rw [Finset.mul_sum]96 calc97 _ = ∑ l, ∑ i, ∑ j, a l j * (u l i * v j i) := by98 apply Finset.sum_congr rfl99 intro l _100 exact Finset.sum_comm101 _ = ∑ i, ∑ l, ∑ j, a l j * (u l i * v j i) := Finset.sum_comm102 _ = _ := by103 apply Finset.sum_congr rfl104 intro i _105 apply Finset.sum_congr rfl106 intro l _107 apply Finset.sum_congr rfl108 intro j _109 ring110111theorem twoSumming_of_matrix {G : ℝ} (hG : MatrixGrothendieckWith G)112 (d k : ℕ) (T : (Fin d → ℝ) →L[ℝ] EllOne k) :113 TwoSummingWith T (G * ‖T‖) := by114 classical115 refine ⟨mul_nonneg hG.1 (norm_nonneg T), ?_⟩116 intro n x M hM hx117 have hc (j : Fin d) : ∑ i, (x i j) ^ 2 ≤ M ^ 2 := by118 let φ : (Fin d → ℝ) →L[ℝ] ℝ := ContinuousLinearMap.proj j119 have hφ : ‖φ‖ ≤ 1 := ContinuousLinearMap.opNorm_le_bound _ zero_le_one (fun z => by120 simpa only [φ, ContinuousLinearMap.proj_apply, one_mul] using norm_le_pi_norm z j)121 simpa only [φ, ContinuousLinearMap.proj_apply, sq_abs] using hx φ hφ122 by_cases hM0 : M = 0123 · have hz (i : Fin n) : x i = 0 := by124 ext j125 have hh := (Finset.single_le_sum (fun r _ => sq_nonneg (x r j)) (Finset.mem_univ i)).trans (hc j)126 rw [hM0, zero_pow (by norm_num : 2 ≠ 0)] at hh127 change x i j = 0128 nlinarith [sq_nonneg (x i j)]129 simp only [hz, map_zero, norm_zero, zero_pow (by norm_num : 2 ≠ 0),130 Finset.sum_const_zero, hM0, mul_zero, le_refl]131 have hMp : 0 < M := lt_of_le_of_ne hM (Ne.symm hM0)132 let L : ℝ := Real.sqrt (∑ i, ‖T (x i)‖ ^ 2)133 have hLs : L ^ 2 = ∑ i, ‖T (x i)‖ ^ 2 := Real.sq_sqrt (Finset.sum_nonneg (fun _ _ => sq_nonneg _))134 by_cases hL0 : L = 0135 · rw [← hLs, hL0, zero_pow (by norm_num : 2 ≠ 0)]136 exact mul_nonneg (sq_nonneg _) (sq_nonneg _)137 have hLp : 0 < L := lt_of_le_of_ne (Real.sqrt_nonneg _) (Ne.symm hL0)138 let u : Fin k → Fin n → ℝ := fun l i => (‖T (x i)‖ / L) * signOne (T (x i) l)139 let v : Fin d → Fin n → ℝ := fun j i => x i j / M140 have hu (l : Fin k) : ∑ i, (u l i) ^ 2 ≤ 1 := by141 simp only [u, mul_pow, signOne_sq, mul_one, div_pow]142 rw [← Finset.sum_div, ← hLs, div_self (pow_ne_zero _ hL0)]143 have hv (j : Fin d) : ∑ i, (v j i) ^ 2 ≤ 1 := by144 simp only [v, div_pow]145 rw [← Finset.sum_div]146 exact (div_le_one (sq_pos_of_pos hMp)).mpr (hc j)147 have hg := hG.2 k d n (entry T) u v ‖T‖ hu hv (entry_scalar_bound T)148 have he : (∑ l, ∑ j, entry T l j * (∑ i, u l i * v j i)) = L / M := by149 rw [rearrange]150 have hi (i : Fin n) : (∑ l, u l i * (∑ j, entry T l j * v j i)) =151 ‖T (x i)‖ ^ 2 / (L * M) := by152 calc153 _ = ∑ l, (‖T (x i)‖ / (L * M)) * |T (x i) l| := by154 apply Finset.sum_congr rfl155 intro l _156 have he' : (∑ j, entry T l j * v j i) = T (x i) l / M := by157 simp only [v, ← mul_div_assoc, ← Finset.sum_div, entry_apply]158 rw [he']159 dsimp only [u]160 rw [← signOne_mul (T (x i) l)]161 ring162 _ = _ := by rw [← Finset.mul_sum, ← norm_ellOne]; ring163 simp_rw [hi]164 rw [← Finset.sum_div, ← hLs]165 field_simp166 rw [he, abs_of_pos (div_pos hLp hMp)] at hg167 have hbound : L ≤ (G * ‖T‖) * M := (div_le_iff₀ hMp).mp hg168 rw [← hLs, ← mul_pow]169 exact pow_le_pow_left₀ hLp.le hbound 2170171#print axioms twoSumming_of_matrix172173def ellOneDual {d : ℕ} (t : Fin d → ℝ) : EllOne d →L[ℝ] ℝ :=174 ∑ j, t j • PiLp.proj 1 (fun _ : Fin d => ℝ) j175176theorem ellOneDual_apply {d : ℕ} (t : Fin d → ℝ) (x : EllOne d) :177 ellOneDual t x = ∑ j, t j * x j := by178 simp only [ellOneDual, sum_apply, smul_apply, PiLp.proj_apply, smul_eq_mul]179180theorem norm_ellOneDual_le {d : ℕ} (t : Fin d → ℝ) (ht : ∀ j, |t j| ≤ 1) :181 ‖ellOneDual t‖ ≤ 1 := by182 apply ContinuousLinearMap.opNorm_le_bound _ zero_le_one183 intro x184 rw [ellOneDual_apply, Real.norm_eq_abs, one_mul, norm_ellOne]185 calc186 _ ≤ ∑ j, |t j * x j| := Finset.abs_sum_le_sum_abs _ _187 _ ≤ _ := by188 apply Finset.sum_le_sum189 intro j _190 rw [abs_mul]191 exact mul_le_of_le_one_left (abs_nonneg _) (ht j)192193theorem ellOne_scalar_bound {d n : ℕ} (x : Fin n → EllOne d) (M : ℝ)194 (hx : ∀ φ : EllOne d →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ≤ M)195 (s : Fin n → ℝ) (t : Fin d → ℝ) (hs : ∀ i, |s i| ≤ 1) (ht : ∀ j, |t j| ≤ 1) :196 |∑ i, ∑ j, x i j * s i * t j| ≤ M := by197 have he : (∑ i, ∑ j, x i j * s i * t j) = ∑ i, s i * ellOneDual t (x i) := by198 apply Finset.sum_congr rfl199 intro i _200 rw [ellOneDual_apply, Finset.mul_sum]201 apply Finset.sum_congr rfl202 intro j _203 ring204 rw [he]205 calc206 _ ≤ ∑ i, |s i * ellOneDual t (x i)| := Finset.abs_sum_le_sum_abs _ _207 _ ≤ ∑ i, |ellOneDual t (x i)| := by208 apply Finset.sum_le_sum209 intro i _210 rw [abs_mul]211 exact mul_le_of_le_one_left (abs_nonneg _) (hs i)212 _ ≤ M := hx (ellOneDual t) (norm_ellOneDual_le t ht)213214theorem ellOne_image_coordinate {d k : ℕ} (S : EllOne d →L[ℝ] EuclideanSpace ℝ (Fin k))215 (x : EllOne d) (l : Fin k) :216 ∑ j, S (PiLp.single 1 j 1) l * x j = S x l := by217 let φ := (PiLp.proj 2 (fun _ : Fin k => ℝ) l).comp S218 have hx : ∑ j, x j • PiLp.single 1 j (1 : ℝ) = x := by219 simpa only [PiLp.basisFun_repr, PiLp.basisFun_apply] using220 (PiLp.basisFun 1 ℝ (Fin d)).sum_repr x221 change (∑ j, φ (PiLp.single 1 j 1) * x j) = φ x222 calc223 _ = φ (∑ j, x j • PiLp.single 1 j (1 : ℝ)) := by224 rw [map_sum]225 simp only [map_smul, smul_eq_mul]226 apply Finset.sum_congr rfl227 intro j _228 ring229 _ = φ x := by rw [hx]230231theorem normalized_sq_le {k : ℕ} (y : EuclideanSpace ℝ (Fin k)) :232 ∑ l, (y l / ‖y‖) ^ 2 ≤ 1 := by233 simp only [div_pow]234 rw [← Finset.sum_div, ← EuclideanSpace.real_norm_sq_eq]235 by_cases hy : ‖y‖ = 0236 · simp [hy]237 · rw [div_self (pow_ne_zero _ hy)]238239theorem oneSumming_of_matrix {G : ℝ} (hG : MatrixGrothendieckWith G)240 (d k : ℕ) (S : EllOne d →L[ℝ] EuclideanSpace ℝ (Fin k)) :241 OneSummingWith S (G * ‖S‖) := by242 classical243 refine ⟨mul_nonneg hG.1 (norm_nonneg S), ?_⟩244 intro n x M hx245 by_cases hS : S = 0246 · simp [hS]247 have hSp : 0 < ‖S‖ := norm_pos_iff.mpr hS248 let u : Fin n → Fin k → ℝ := fun i l => S (x i) l / ‖S (x i)‖249 let v : Fin d → Fin k → ℝ := fun j l => S (PiLp.single 1 j 1) l / ‖S‖250 have hu (i : Fin n) : ∑ l, (u i l) ^ 2 ≤ 1 := normalized_sq_le (S (x i))251 have hv (j : Fin d) : ∑ l, (v j l) ^ 2 ≤ 1 := by252 simp only [v, div_pow]253 rw [← Finset.sum_div, ← EuclideanSpace.real_norm_sq_eq]254 apply (div_le_one (sq_pos_of_pos hSp)).mpr255 apply pow_le_pow_left₀ (norm_nonneg _)256 simpa only [PiLp.norm_single, norm_one, mul_one] using S.le_opNorm (PiLp.single 1 j (1 : ℝ))257 have hg := hG.2 n d k (fun i j => x i j) u v M hu hv (ellOne_scalar_bound x M hx)258 have he : (∑ i, ∑ j, x i j * (∑ l, u i l * v j l)) =259 (∑ i, ‖S (x i)‖) / ‖S‖ := by260 rw [Finset.sum_div]261 apply Finset.sum_congr rfl262 intro i _263 simp_rw [Finset.mul_sum]264 rw [Finset.sum_comm]265 calc266 _ = ∑ l, (u i l / ‖S‖) * (∑ j, S (PiLp.single 1 j 1) l * x i j) := by267 apply Finset.sum_congr rfl268 intro l _269 rw [Finset.mul_sum]270 apply Finset.sum_congr rfl271 intro j _272 dsimp only [v]273 ring274 _ = ∑ l, (S (x i) l) ^ 2 / (‖S (x i)‖ * ‖S‖) := by275 simp_rw [ellOne_image_coordinate]276 apply Finset.sum_congr rfl277 intro l _278 dsimp only [u]279 ring280 _ = _ := by281 rw [← Finset.sum_div, ← EuclideanSpace.real_norm_sq_eq]282 by_cases hy : ‖S (x i)‖ = 0283 · simp [hy]284 · field_simp285 rw [he, abs_of_nonneg (div_nonneg (Finset.sum_nonneg (fun _ _ => norm_nonneg _)) hSp.le)] at hg286 have h := (div_le_iff₀ hSp).mp hg287 nlinarith288289#print axioms oneSumming_of_matrix290291end PL1.FiniteSumming292293-- Final supplementary type audit: the matrix hypothesis remains visible.294#print PL1.FiniteSumming.MatrixGrothendieckWith295#check @PL1.FiniteSumming.twoSumming_of_matrix296#check @PL1.FiniteSumming.oneSumming_of_matrix297298299