PL1/ComplementedLatticeSumming.lean
All source files · Download exact source
SHA-256: 20ac7196db0e89ffad9227cb595144f5070cc9563da65c58a6b91f219bcbb934
1import BanLat.Disjoint2import Mathlib.Analysis.Normed.Module.HahnBanach3import Mathlib.Analysis.InnerProductSpace.PiL24import Mathlib.LinearAlgebra.Finsupp.LinearCombination5import Mathlib.Tactic.Positivity6import Mathlib.Tactic.Linarith78/-! # Finite summing estimates for the complemented-lattice classification910The definitions express quantitative absolute summability through universal11bounds on dual evaluations, avoiding a choice of a maximizing functional.12The deep Grothendieck estimates are not assumed as instances or axioms.13-/1415noncomputable section16open scoped BigOperators1718namespace PL1.ComplementedLattice1920section General21variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]22 [NormedAddCommGroup F] [NormedSpace ℝ F]2324/-- The usual 1-summing inequality, with an explicit upper bound for the25weak 1-norm of each finite family. -/26def OneSummingWith (T : E →L[ℝ] F) (C : ℝ) : Prop :=27 0 ≤ C ∧ ∀ (n : ℕ) (x : Fin n → E) (M : ℝ),28 (∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ≤ M) →29 ∑ i, ‖T (x i)‖ ≤ C * M3031/-- The usual 2-summing inequality in squared form. -/32def TwoSummingWith (T : E →L[ℝ] F) (C : ℝ) : Prop :=33 0 ≤ C ∧ ∀ (n : ℕ) (x : Fin n → E) (M : ℝ), 0 ≤ M →34 (∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ^ 2 ≤ M ^ 2) →35 ∑ i, ‖T (x i)‖ ^ 2 ≤ C ^ 2 * M ^ 23637end General3839section Lattice4041variable {E F : Type*} [NormedAddCommGroup E] [Lattice E] [IsOrderedAddMonoid E]42 [NormedVectorLattice E] [NormedAddCommGroup F] [NormedSpace ℝ F]4344theorem norm_signed_disjoint_sum (n : ℕ) (x : Fin n → E)45 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j))46 (a : Fin n → ℝ) (ha : ∀ i, |a i| = 1) :47 ‖∑ i, a i • x i‖ = ‖∑ i, x i‖ := by48 have hsum : |∑ i, x i| = ∑ i, |x i| := by49 simpa only [one_smul, abs_one] using50 (abs_sum_of_pairwise_isVLDisjoint (α := fun _ => (1 : ℝ)) hx)51 rw [← norm_abs_eq_norm, abs_sum_of_pairwise_isVLDisjoint hx]52 simp only [ha, one_smul]53 rw [← hsum, norm_abs_eq_norm]5455/-- The weak 1-norm of a finite disjoint family is exactly the norm of its56sum. This direction suffices for the 1-summing estimate in de Hevia et al.57Proposition 2.1 and needs no lattice structure on the dual. -/58theorem disjoint_dual_sum_le (n : ℕ) (x : Fin n → E)59 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) (φ : E →L[ℝ] ℝ) :60 ∑ i, |φ (x i)| ≤ ‖φ‖ * ‖∑ i, x i‖ := by61 classical62 let a : Fin n → ℝ := fun i => if 0 ≤ φ (x i) then 1 else -163 have ha (i : Fin n) : |a i| = 1 := by dsimp [a]; split <;> norm_num64 have he (i : Fin n) : a i * φ (x i) = |φ (x i)| := by65 dsimp [a]66 split_ifs with hi67 · simp only [one_mul, abs_of_nonneg hi]68 · simp only [neg_one_mul, abs_of_neg (lt_of_not_ge hi)]69 calc70 _ = φ (∑ i, a i • x i) := by simp only [map_sum, map_smul, smul_eq_mul, he]71 _ ≤ |φ (∑ i, a i • x i)| := le_abs_self _72 _ ≤ ‖φ‖ * ‖∑ i, a i • x i‖ := φ.le_opNorm _73 _ = _ := by rw [norm_signed_disjoint_sum n x hx a ha]7475theorem disjoint_dual_sum_le_of_norm_le_one (n : ℕ) (x : Fin n → E)76 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j))77 (φ : E →L[ℝ] ℝ) (hφ : ‖φ‖ ≤ 1) : ∑ i, |φ (x i)| ≤ ‖∑ i, x i‖ :=78 (disjoint_dual_sum_le n x hx φ).trans79 (by simpa only [one_mul] using mul_le_mul_of_nonneg_right hφ (norm_nonneg (∑ i, x i)))8081theorem OneSummingWith.disjoint_sum_le {T : E →L[ℝ] F} {C : ℝ}82 (hT : OneSummingWith T C) (n : ℕ) (x : Fin n → E)83 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :84 ∑ i, ‖T (x i)‖ ≤ C * ‖∑ i, x i‖ :=85 hT.2 n x ‖∑ i, x i‖ (disjoint_dual_sum_le_of_norm_le_one n x hx)8687theorem norm_disjoint_sum_le (n : ℕ) (x : Fin n → E)88 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) (a : Fin n → ℝ) :89 ‖∑ i, a i • x i‖ ≤ ‖∑ i, x i‖ * ‖a‖ := by90 have hsum : |∑ i, x i| = ∑ i, |x i| := by91 simpa only [one_smul, abs_one] using92 (abs_sum_of_pairwise_isVLDisjoint (α := fun _ => (1 : ℝ)) hx)93 have hab : |∑ i, a i • x i| ≤ ‖a‖ • |∑ i, x i| := by94 rw [abs_sum_of_pairwise_isVLDisjoint hx, hsum, Finset.smul_sum]95 apply Finset.sum_le_sum96 intro i _97 exact smul_le_smul_of_nonneg_right (norm_le_pi_norm a i) (abs_nonneg _)98 have hnorm := norm_le_norm_of_abs_le_abs (b := ‖a‖ • ∑ i, x i) (by99 simpa only [abs_smul', abs_of_nonneg (norm_nonneg a)] using hab)100 simpa only [norm_smul, Real.norm_eq_abs, abs_of_nonneg (norm_nonneg a), mul_comm] using hnorm101102/-- Synthesis of a disjoint family from finite ell-infinity, with its103dimension-independent lattice bound. -/104def disjointSynthesis (n : ℕ) (x : Fin n → E)105 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) : (Fin n → ℝ) →L[ℝ] E :=106 (Fintype.linearCombination ℝ x).mkContinuous ‖∑ i, x i‖ (by107 intro a108 simpa only [Fintype.linearCombination_apply] using norm_disjoint_sum_le n x hx a)109110theorem norm_disjointSynthesis_le (n : ℕ) (x : Fin n → E)111 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :112 ‖disjointSynthesis n x hx‖ ≤ ‖∑ i, x i‖ :=113 ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) (norm_disjoint_sum_le n x hx)114115@[simp] theorem disjointSynthesis_single (n : ℕ) (x : Fin n → E)116 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) (i : Fin n) :117 disjointSynthesis n x hx (Pi.single i 1) = x i := by118 change Fintype.linearCombination ℝ x (Pi.single i 1) = x i119 simp120121end Lattice122123theorem dual_sum_coordinate_units_le (n : ℕ) (φ : (Fin n → ℝ) →L[ℝ] ℝ) :124 ∑ i, |φ (Pi.single i 1)| ≤ ‖φ‖ := by125 classical126 let a : Fin n → ℝ := fun i => if 0 ≤ φ (Pi.single i 1) then 1 else -1127 have ha (i : Fin n) : |a i| = 1 := by dsimp [a]; split <;> norm_num128 have hnorm : ‖a‖ ≤ 1 := (pi_norm_le_iff_of_nonneg zero_le_one).mpr (fun i => (ha i).le)129 have he (i : Fin n) : a i * φ (Pi.single i 1) = |φ (Pi.single i 1)| := by130 dsimp [a]131 split_ifs with hi132 · simp only [one_mul, abs_of_nonneg hi]133 · simp only [neg_one_mul, abs_of_neg (lt_of_not_ge hi)]134 have hsum : ∑ i, a i • Pi.single i (1 : ℝ) = a := by135 ext j136 simp [Pi.single_apply, Finset.sum_apply]137 calc138 _ = φ (∑ i, a i • Pi.single i (1 : ℝ)) := by simp only [map_sum, map_smul, smul_eq_mul, he]139 _ = φ a := by rw [hsum]140 _ ≤ |φ a| := le_abs_self _141 _ ≤ ‖φ‖ * ‖a‖ := φ.le_opNorm _142 _ ≤ ‖φ‖ := by simpa only [mul_one] using mul_le_mul_of_nonneg_left hnorm (norm_nonneg φ)143144theorem dual_sq_sum_coordinate_units_le_one (n : ℕ)145 (φ : (Fin n → ℝ) →L[ℝ] ℝ) (hφ : ‖φ‖ ≤ 1) :146 ∑ i, |φ (Pi.single i 1)| ^ 2 ≤ (1 : ℝ) ^ 2 := by147 have hh := (dual_sum_coordinate_units_le n φ).trans hφ148 calc149 _ ≤ (∑ i, |φ (Pi.single i 1)|) ^ 2 := by150 exact Finset.sum_sq_le_sq_sum_of_nonneg (fun _ _ => abs_nonneg _)151 _ ≤ 1 ^ 2 := pow_le_pow_left₀ (Finset.sum_nonneg (fun _ _ => abs_nonneg _)) hh 2152153section TwoSumming154variable {E : Type*} [NormedAddCommGroup E] [Lattice E]155 [IsOrderedAddMonoid E] [NormedVectorLattice E]156157/-- The 2-summing step of Proposition 2.1 for a finite disjoint family.158The summing estimate is an explicit input, not a formalized Grothendieck theorem. -/159theorem disjoint_square_sum_le_of_twoSumming (n : ℕ) (x : Fin n → E)160 (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) {C : ℝ}161 (hT : TwoSummingWith (disjointSynthesis n x hx) C) :162 ∑ i, ‖x i‖ ^ 2 ≤ C ^ 2 := by163 simpa only [disjointSynthesis_single, one_pow, mul_one] using164 hT.2 n (fun i => Pi.single i 1) 1 zero_le_one (dual_sq_sum_coordinate_units_le_one n)165166end TwoSumming167168end PL1.ComplementedLattice169