PL1/SummingTransport.lean
All source files · Download exact source
SHA-256: 73f3e29b7e398a325ac677f3d97748ab45a8e65e5ffd2981dcd088df28a0abf0
1import PL1.ComplementedLatticeSumming2import PL1.EnfloStarbirdProjection3import PL1.ComplementedLatticeBandEstimates45/-!6# Operator-ideal estimates and transfer through an actual complemented copy78The two ambient uniform summing estimates remain explicit hypotheses. These9lemmas prove their elementary transport with the exact embedding/retraction10norm factors; they do not assert Grothendieck's theorem.11-/1213noncomputable section14open scoped BigOperators1516namespace PL1.ComplementedLattice1718section WeakBounds19variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]2021/-- Testing the zero functional supplies the nonnegative weak bound, even for an empty family. -/22theorem weak_one_bound_nonneg (n : ℕ) (x : Fin n → E) (M : ℝ)23 (h : ∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ≤ M) : 0 ≤ M := by24 simpa only [zero_apply, abs_zero, Finset.sum_const_zero] using25 h 0 (by simp)2627/-- Extension of a unit-dual-ball weak bound to every actual dual functional. -/28theorem weak_one_bound (n : ℕ) (x : Fin n → E) (M : ℝ)29 (h : ∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ≤ M)30 (φ : E →L[ℝ] ℝ) : ∑ i, |φ (x i)| ≤ ‖φ‖ * M := by31 by_cases hφ : φ = 032 · simp only [hφ, zero_apply, abs_zero, Finset.sum_const_zero,33 norm_zero, zero_mul, le_refl]34 have hn : ‖φ‖ ≠ 0 := norm_ne_zero_iff.mpr hφ35 let ψ : E →L[ℝ] ℝ := ‖φ‖⁻¹ • φ36 have hψ : ‖ψ‖ ≤ 1 := by37 simp only [ψ, norm_smul, Real.norm_eq_abs,38 abs_of_nonneg (inv_nonneg.mpr (norm_nonneg φ)), inv_mul_cancel₀ hn, le_refl]39 have he (i : Fin n) : ‖φ‖ * ψ (x i) = φ (x i) := by40 simp only [ψ, smul_apply, smul_eq_mul, ← mul_assoc,41 mul_inv_cancel₀ hn, one_mul]42 calc43 _ = ∑ i, ‖φ‖ * |ψ (x i)| := by44 apply Finset.sum_congr rfl45 intro i _46 rw [← he i, abs_mul, abs_of_nonneg (norm_nonneg φ)]47 _ = ‖φ‖ * ∑ i, |ψ (x i)| := (Finset.mul_sum _ _ _).symm48 _ ≤ _ := mul_le_mul_of_nonneg_left (h ψ hψ) (norm_nonneg φ)4950/-- Squared extension of a unit-dual-ball weak bound. -/51theorem weak_two_bound (n : ℕ) (x : Fin n → E) (M : ℝ)52 (h : ∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (x i)| ^ 2 ≤ M ^ 2)53 (φ : E →L[ℝ] ℝ) : ∑ i, |φ (x i)| ^ 2 ≤ ‖φ‖ ^ 2 * M ^ 2 := by54 by_cases hφ : φ = 055 · simp only [hφ, zero_apply, abs_zero, zero_pow (by norm_num : 2 ≠ 0),56 Finset.sum_const_zero, norm_zero, zero_mul, le_refl]57 have hn : ‖φ‖ ≠ 0 := norm_ne_zero_iff.mpr hφ58 let ψ : E →L[ℝ] ℝ := ‖φ‖⁻¹ • φ59 have hψ : ‖ψ‖ ≤ 1 := by60 simp only [ψ, norm_smul, Real.norm_eq_abs,61 abs_of_nonneg (inv_nonneg.mpr (norm_nonneg φ)), inv_mul_cancel₀ hn, le_refl]62 have he (i : Fin n) : ‖φ‖ * ψ (x i) = φ (x i) := by63 simp only [ψ, smul_apply, smul_eq_mul, ← mul_assoc,64 mul_inv_cancel₀ hn, one_mul]65 calc66 _ = ∑ i, ‖φ‖ ^ 2 * |ψ (x i)| ^ 2 := by67 apply Finset.sum_congr rfl68 intro i _69 rw [← he i, abs_mul, abs_of_nonneg (norm_nonneg φ), mul_pow]70 _ = ‖φ‖ ^ 2 * ∑ i, |ψ (x i)| ^ 2 := (Finset.mul_sum _ _ _).symm71 _ ≤ _ := mul_le_mul_of_nonneg_left (h ψ hψ) (sq_nonneg _)7273end WeakBounds7475section OperatorIdeal76variable {E F H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]77 [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup H] [NormedSpace ℝ H]7879theorem OneSummingWith.mono {T : E →L[ℝ] F} {C D : ℝ}80 (hT : OneSummingWith T C) (hCD : C ≤ D) : OneSummingWith T D := by81 refine ⟨hT.1.trans hCD, ?_⟩82 intro n x M hM83 exact (hT.2 n x M hM).trans84 (mul_le_mul_of_nonneg_right hCD (weak_one_bound_nonneg n x M hM))8586theorem TwoSummingWith.mono {T : E →L[ℝ] F} {C D : ℝ}87 (hT : TwoSummingWith T C) (hCD : C ≤ D) : TwoSummingWith T D := by88 refine ⟨hT.1.trans hCD, ?_⟩89 intro n x M hM hx90 exact (hT.2 n x M hM hx).trans91 (mul_le_mul_of_nonneg_right (pow_le_pow_left₀ hT.1 hCD 2) (sq_nonneg M))9293/-- Precomposition has exactly its ordinary operator-norm cost. -/94theorem OneSummingWith.precomp {T : E →L[ℝ] F} {C : ℝ}95 (hT : OneSummingWith T C) (A : H →L[ℝ] E) :96 OneSummingWith (T.comp A) (C * ‖A‖) := by97 refine ⟨mul_nonneg hT.1 (norm_nonneg A), ?_⟩98 intro n x M hx99 have hM := weak_one_bound_nonneg n x M hx100 have hweak : ∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 → ∑ i, |φ (A (x i))| ≤ ‖A‖ * M := by101 intro φ hφ102 have hc : ‖φ.comp A‖ ≤ ‖A‖ :=103 (ContinuousLinearMap.opNorm_comp_le _ _).trans (by104 simpa only [one_mul] using mul_le_mul_of_nonneg_right hφ (norm_nonneg A))105 exact (weak_one_bound n x M hx (φ.comp A)).trans106 (mul_le_mul_of_nonneg_right hc hM)107 simpa only [ContinuousLinearMap.comp_apply, mul_assoc] using108 hT.2 n (fun i => A (x i)) (‖A‖ * M) hweak109110/-- Postcomposition has exactly its ordinary operator-norm cost. -/111theorem OneSummingWith.postcomp {T : E →L[ℝ] F} {C : ℝ}112 (hT : OneSummingWith T C) (B : F →L[ℝ] H) :113 OneSummingWith (B.comp T) (‖B‖ * C) := by114 refine ⟨mul_nonneg (norm_nonneg B) hT.1, ?_⟩115 intro n x M hx116 calc117 _ ≤ ∑ i, ‖B‖ * ‖T (x i)‖ := Finset.sum_le_sum (fun i _ => B.le_opNorm _)118 _ = ‖B‖ * ∑ i, ‖T (x i)‖ := (Finset.mul_sum _ _ _).symm119 _ ≤ ‖B‖ * (C * M) := mul_le_mul_of_nonneg_left (hT.2 n x M hx) (norm_nonneg B)120 _ = _ := (mul_assoc _ _ _).symm121122/-- Precomposition for the squared two-summing inequality. -/123theorem TwoSummingWith.precomp {T : E →L[ℝ] F} {C : ℝ}124 (hT : TwoSummingWith T C) (A : H →L[ℝ] E) :125 TwoSummingWith (T.comp A) (C * ‖A‖) := by126 refine ⟨mul_nonneg hT.1 (norm_nonneg A), ?_⟩127 intro n x M hM hx128 have hweak : ∀ φ : E →L[ℝ] ℝ, ‖φ‖ ≤ 1 →129 ∑ i, |φ (A (x i))| ^ 2 ≤ (‖A‖ * M) ^ 2 := by130 intro φ hφ131 have hc : ‖φ.comp A‖ ≤ ‖A‖ :=132 (ContinuousLinearMap.opNorm_comp_le _ _).trans (by133 simpa only [one_mul] using mul_le_mul_of_nonneg_right hφ (norm_nonneg A))134 have h := (weak_two_bound n x M hx (φ.comp A)).trans135 (mul_le_mul_of_nonneg_right136 (pow_le_pow_left₀ (norm_nonneg _) hc 2) (sq_nonneg M))137 simpa only [ContinuousLinearMap.comp_apply, mul_pow] using h138 simpa only [ContinuousLinearMap.comp_apply, mul_pow, mul_assoc] using139 hT.2 n (fun i => A (x i)) (‖A‖ * M) (mul_nonneg (norm_nonneg A) hM) hweak140141/-- Postcomposition for the squared two-summing inequality. -/142theorem TwoSummingWith.postcomp {T : E →L[ℝ] F} {C : ℝ}143 (hT : TwoSummingWith T C) (B : F →L[ℝ] H) :144 TwoSummingWith (B.comp T) (‖B‖ * C) := by145 refine ⟨mul_nonneg (norm_nonneg B) hT.1, ?_⟩146 intro n x M hM hx147 calc148 _ ≤ ∑ i, ‖B‖ ^ 2 * ‖T (x i)‖ ^ 2 := by149 apply Finset.sum_le_sum150 intro i _151 simpa only [mul_pow, ContinuousLinearMap.comp_apply] using pow_le_pow_left₀ (norm_nonneg _) (B.le_opNorm (T (x i))) 2152 _ = ‖B‖ ^ 2 * ∑ i, ‖T (x i)‖ ^ 2 := (Finset.mul_sum _ _ _).symm153 _ ≤ ‖B‖ ^ 2 * (C ^ 2 * M ^ 2) :=154 mul_le_mul_of_nonneg_left (hT.2 n x M hM hx) (sq_nonneg _)155 _ = _ := by ring156157end OperatorIdeal158159section Complemented160variable {E Y F H : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]161 [NormedAddCommGroup Y] [NormedSpace ℝ Y]162 [NormedAddCommGroup F] [NormedSpace ℝ F]163 [NormedAddCommGroup H] [NormedSpace ℝ H]164165/-- One-summing estimates descend through the actual embedding and retraction. -/166theorem complemented_oneSumming (Q : EnfloStarbird.ComplementedCopy ℝ E Y)167 {G : ℝ} (hG : 0 ≤ G)168 (hY : ∀ S : Y →L[ℝ] F, OneSummingWith S (G * ‖S‖)) (S : E →L[ℝ] F) :169 OneSummingWith S ((G * ‖Q.embedding‖ * ‖Q.retraction‖) * ‖S‖) := by170 have ht := (hY (S.comp Q.retraction)).precomp Q.embedding171 have he : (S.comp Q.retraction).comp Q.embedding = S := by172 ext x173 change S (Q.retraction (Q.embedding x)) = S x174 rw [Q.left_inv x]175 rw [he] at ht176 apply ht.mono177 calc178 _ ≤ (G * (‖S‖ * ‖Q.retraction‖)) * ‖Q.embedding‖ :=179 mul_le_mul_of_nonneg_right180 (mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) hG)181 (norm_nonneg _)182 _ = _ := by ring183184/-- Two-summing estimates descend through the actual embedding and retraction. -/185theorem complemented_twoSumming (Q : EnfloStarbird.ComplementedCopy ℝ E Y)186 {G : ℝ} (hG : 0 ≤ G)187 (hY : ∀ T : H →L[ℝ] Y, TwoSummingWith T (G * ‖T‖)) (T : H →L[ℝ] E) :188 TwoSummingWith T ((G * ‖Q.embedding‖ * ‖Q.retraction‖) * ‖T‖) := by189 have ht := (hY (Q.embedding.comp T)).postcomp Q.retraction190 have he : Q.retraction.comp (Q.embedding.comp T) = T := by191 ext x192 exact Q.left_inv (T x)193 rw [he] at ht194 apply ht.mono195 calc196 _ ≤ ‖Q.retraction‖ * (G * (‖Q.embedding‖ * ‖T‖)) :=197 mul_le_mul_of_nonneg_left198 (mul_le_mul_of_nonneg_left (ContinuousLinearMap.opNorm_comp_le _ _) hG)199 (norm_nonneg _)200 _ = _ := by ring201202/-- The two finite-dimensional hypotheses used by the lattice band estimate203transfer with the same dimension-independent constant. -/204theorem uniform_finite_summing_estimates (Q : EnfloStarbird.ComplementedCopy ℝ E Y)205 {G : ℝ} (hG : 0 ≤ G)206 (hOne : ∀ (n : ℕ) (S : Y →L[ℝ] EuclideanSpace ℝ (Fin n)), OneSummingWith S (G * ‖S‖))207 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] Y), TwoSummingWith T (G * ‖T‖)) :208 let C := G * ‖Q.embedding‖ * ‖Q.retraction‖209 0 ≤ C ∧210 (∀ (n : ℕ) (S : E →L[ℝ] EuclideanSpace ℝ (Fin n)), OneSummingWith S (C * ‖S‖)) ∧211 (∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] E), TwoSummingWith T (C * ‖T‖)) := by212 refine ⟨mul_nonneg (mul_nonneg hG (norm_nonneg _)) (norm_nonneg _), ?_, ?_⟩213 · intro n S214 exact complemented_oneSumming Q hG (hOne n) S215 · intro n T216 exact complemented_twoSumming Q hG (hTwo n) T217218end Complemented219220section LatticeConsequence221variable {E Y : Type*} [NormedAddCommGroup E] [Lattice E]222 [IsOrderedAddMonoid E] [NormedVectorLattice E] [HasPrincipalProjectionProperty E]223 [NormedAddCommGroup Y] [NormedSpace ℝ Y]224225/-- The existing finite-band estimate, directly from an actual complemented226copy and the two ambient summing hypotheses. Principal projections remain227an explicit assumption and are not inferred from the Banach lattice axioms. -/228theorem disjoint_sum_norm_le_of_complemented_ambient_estimates229 (Q : EnfloStarbird.ComplementedCopy ℝ E Y) {G : ℝ} (hG : 0 ≤ G)230 (hOne : ∀ (n : ℕ) (S : Y →L[ℝ] EuclideanSpace ℝ (Fin n)), OneSummingWith S (G * ‖S‖))231 (hTwo : ∀ (n : ℕ) (T : (Fin n → ℝ) →L[ℝ] Y), TwoSummingWith T (G * ‖T‖))232 (n : ℕ) (x : Fin n → E) (hx : Pairwise fun i j => IsVLDisjoint (x i) (x j)) :233 ∑ i, ‖x i‖ ≤ (G * ‖Q.embedding‖ * ‖Q.retraction‖) ^ 2 * ‖∑ i, x i‖ := by234 obtain ⟨hC, hOneE, hTwoE⟩ := uniform_finite_summing_estimates Q hG hOne hTwo235 exact disjoint_sum_norm_le_of_summing_estimates _ hC hOneE hTwoE n x hx236237end LatticeConsequence238239#print axioms OneSummingWith.precomp240#print axioms OneSummingWith.postcomp241#print axioms TwoSummingWith.precomp242#print axioms TwoSummingWith.postcomp243#print axioms uniform_finite_summing_estimates244#print axioms disjoint_sum_norm_le_of_complemented_ambient_estimates245246end PL1.ComplementedLattice247