PL1/SchurApproximation.lean
All source files · Download exact source
SHA-256: 9a2fdafb06734ef120e04c5f3695e005cc8b6212d618c365468095da5aff4497
1import PL1.IntrinsicGraph2import PL1.L1Sum3import PL1.WeakSchur4import Mathlib.Analysis.Normed.Module.HahnBanach56/-!7# Coordinate approximation in countable `ℓ₁` sums89Uniform tails and coordinate norm convergence first give an elementary norm10convergence criterion. A full gliding-hump proof then shows that weak nullity11plus coordinate norm convergence already implies convergence in the actual12`ℓ₁` norm. This proves the Schur property for countable sums of a Schur space,13including genuine scalar `ℓ₁`, and gives the intrinsic graph's Schur property14when its coordinate operators are Dunford–Pettis.15-/1617noncomputable section18open Filter19open scoped Topology2021namespace PL1.L1Sum2223variable {Y : Type*} [NormedAddCommGroup Y]2425/-- Norm mass on the first `N` coordinates. -/26def headNorm (N : ℕ) (x : L1Sum Y) : ℝ :=27 ∑ n ∈ Finset.range N, ‖x n‖2829/-- Norm mass on all coordinates from `N` onward. -/30def tailNorm (N : ℕ) (x : L1Sum Y) : ℝ :=31 ∑' n : ℕ, ‖x (n + N)‖3233theorem headNorm_nonneg (N : ℕ) (x : L1Sum Y) : 0 ≤ headNorm N x :=34 Finset.sum_nonneg (fun _ _ => norm_nonneg _)3536theorem tailNorm_nonneg (N : ℕ) (x : L1Sum Y) : 0 ≤ tailNorm N x :=37 tsum_nonneg (fun _ => norm_nonneg _)3839theorem norm_eq_headNorm_add_tailNorm (N : ℕ) (x : L1Sum Y) :40 ‖x‖ = headNorm N x + tailNorm N x := by41 rw [norm_eq_tsum]42 exact ((summable_norm x).sum_add_tsum_nat_add N).symm4344/-- Every individual `ℓ₁` vector has vanishing tails. -/45theorem tailNorm_tendsto_zero (x : L1Sum Y) :46 Tendsto (fun N : ℕ => tailNorm N x) atTop (𝓝 0) := by47 have h := (summable_norm x).hasSum.tendsto_sum_nat48 rw [← norm_eq_tsum] at h49 have h' := (tendsto_const_nhds (x := ‖x‖)).sub h50 simp only [sub_self] at h'51 convert h' using 152 funext N53 have hN := norm_eq_headNorm_add_tailNorm N x54 dsimp [headNorm] at hN55 linarith5657/-- Uniform smallness of the norm mass outside one finite initial segment. -/58def HasUniformNormTails (x : ℕ → L1Sum Y) : Prop :=59 ∀ ε : ℝ, 0 < ε → ∃ N : ℕ, ∀ k : ℕ, tailNorm N (x k) < ε6061/-- Each fixed finite head converges in norm under coordinatewise convergence. -/62theorem headNorm_tendsto_zero {x : ℕ → L1Sum Y}63 (hx : ∀ n : ℕ, Tendsto (fun k => x k n) atTop (𝓝 0)) (N : ℕ) :64 Tendsto (fun k => headNorm N (x k)) atTop (𝓝 0) := by65 have h := tendsto_finsetSum (Finset.range N)66 (fun n _ => tendsto_zero_iff_norm_tendsto_zero.mp (hx n))67 simpa only [headNorm, Finset.sum_const_zero] using h6869/-- Coordinate norm convergence and uniform norm tails force `ℓ₁` convergence. -/70theorem tendsto_zero_of_coordinates_and_uniformTails {x : ℕ → L1Sum Y}71 (hx : ∀ n : ℕ, Tendsto (fun k => x k n) atTop (𝓝 0))72 (htail : HasUniformNormTails x) : Tendsto x atTop (𝓝 0) := by73 apply Metric.tendsto_atTop.mpr74 intro ε hε75 obtain ⟨N, hN⟩ := htail (ε / 2) (half_pos hε)76 have hhead := (headNorm_tendsto_zero hx N).eventually_lt_const (half_pos hε)77 obtain ⟨K, hK⟩ := eventually_atTop.mp hhead78 refine ⟨K, fun k hk => ?_⟩79 rw [dist_zero_right, norm_eq_headNorm_add_tailNorm N]80 have h₁ := hN k81 have h₂ := hK k hk82 linarith8384/-- Restriction of an `ℓ₁` vector to a finite interval of coordinates. -/85def block (N M : ℕ) (x : L1Sum Y) : L1Sum Y :=86 ∑ i ∈ Finset.Ico N M, lp.single 1 i (x i)8788theorem block_apply (N M : ℕ) (x : L1Sum Y) (i : ℕ) :89 block N M x i = if i ∈ Finset.Ico N M then x i else 0 := by90 simp only [block, lp.coeFn_sum, Finset.sum_apply, lp.coeFn_single,91 Finset.sum_pi_single]9293theorem norm_sub_block {N M : ℕ} (hNM : N ≤ M) (x : L1Sum Y) :94 ‖x - block N M x‖ = headNorm N x + tailNorm M x := by95 have h := lp.norm_compl_sum_single (by norm_num : 0 < (1 : ENNReal).toReal)96 x (Finset.Ico N M)97 simp only [ENNReal.toReal_one, Real.rpow_one] at h98 rw [Finset.sum_Ico_eq_sub (fun i : ℕ => ‖x i‖) hNM] at h99 have hM := norm_eq_headNorm_add_tailNorm M x100 dsimp [block, headNorm] at hM ⊢101 linarith102103/-- The finite-block extraction underlying the gliding-hump argument. A104coordinatewise null sequence which is not norm null has a subsequence uniformly105close to disjoint blocks, while keeping its norm bounded away from zero. -/106theorem exists_disjoint_blocks_of_not_tendsto {x : ℕ → L1Sum Y}107 (hx : ∀ i : ℕ, Tendsto (fun k => x k i) atTop (𝓝 0))108 (hn : ¬ Tendsto x atTop (𝓝 0)) :109 ∃ ε : ℝ, 0 < ε ∧ ∃ n : ℕ → ℕ, (∀ k, k ≤ n k) ∧110 ∃ s : ℕ → Finset ℕ, Pairwise (fun k l => Disjoint (s k) (s l)) ∧111 ∃ v : ℕ → L1Sum Y,112 (∀ k i : ℕ, i ∉ s k → v k i = 0) ∧113 ∀ k : ℕ, ε ≤ ‖x (n k)‖ ∧ ‖x (n k) - v k‖ < ε / 4 := by114 classical115 rw [Metric.tendsto_atTop] at hn116 push Not at hn117 obtain ⟨ε, hε, hbad⟩ := hn118 simp only [dist_zero_right] at hbad119 have hstep : ∀ N k : ℕ, ∃ n M : ℕ,120 k ≤ n ∧ N < M ∧ ε ≤ ‖x n‖ ∧121 headNorm N (x n) < ε / 8 ∧ tailNorm M (x n) < ε / 8 := by122 intro N k123 have hε8 : 0 < ε / 8 := by positivity124 obtain ⟨K, hK⟩ := eventually_atTop.mp125 ((headNorm_tendsto_zero hx N).eventually_lt_const hε8)126 obtain ⟨n, hn, hnorm⟩ := hbad (max k K)127 obtain ⟨M, hM⟩ := eventually_atTop.mp128 ((tailNorm_tendsto_zero (x n)).eventually_lt_const hε8)129 refine ⟨n, max (N + 1) M, (le_max_left k K).trans hn, ?_, hnorm, ?_, ?_⟩130 · exact (Nat.lt_succ_self N).trans_le (le_max_left _ _)131 · exact hK n ((le_max_right k K).trans hn)132 · exact hM _ (le_max_right _ _)133 choose a b ha hb hnorm hhead htail using hstep134 let cut : ℕ → ℕ := Nat.rec 0 (fun k N => b N k)135 have hcutstep : ∀ k : ℕ, cut k < cut (k + 1) := by136 intro k137 change cut k < b (cut k) k138 exact hb _ _139 have hcut : StrictMono cut := strictMono_nat_of_lt_succ hcutstep140 let n : ℕ → ℕ := fun k => a (cut k) k141 let s : ℕ → Finset ℕ := fun k => Finset.Ico (cut k) (cut (k + 1))142 let v : ℕ → L1Sum Y := fun k => block (cut k) (cut (k + 1)) (x (n k))143 refine ⟨ε, hε, n, (fun k => ha _ _), s, ?_, v, ?_, ?_⟩144 · intro k l hkl145 apply Finset.disjoint_left.mpr146 intro i hik hil147 have hik' := Finset.mem_Ico.mp hik148 have hil' := Finset.mem_Ico.mp hil149 rcases lt_or_gt_of_ne hkl with hlt | hgt150 · have hbound := hcut.monotone (Nat.succ_le_of_lt hlt)151 change cut (k + 1) ≤ cut l at hbound152 omega153 · have hbound := hcut.monotone (Nat.succ_le_of_lt hgt)154 change cut (l + 1) ≤ cut k at hbound155 omega156 · intro k i hi157 exact (block_apply (cut k) (cut (k + 1)) (x (n k)) i).trans (ite_eq_right hi)158 · intro k159 refine ⟨hnorm _ _, ?_⟩160 change ‖x (n k) - block (cut k) (cut (k + 1)) (x (n k))‖ < ε / 4161 rw [norm_sub_block (hcutstep k).le]162 have hh : headNorm (cut k) (x (n k)) < ε / 8 := hhead _ _163 have ht : tailNorm (cut (k + 1)) (x (n k)) < ε / 8 := htail _ _164 linarith165166section DualBlocks167168variable (𝕜 : Type*) [RCLike 𝕜] [NormedSpace 𝕜 Y]169170/-- A single bounded functional norms every member of a sequence supported on171pairwise disjoint finite coordinate sets. This is the duality step in the172gliding-hump argument for countable `ℓ₁` sums. -/173theorem exists_dual_norming_disjoint_blocks (v : ℕ → L1Sum Y)174 (s : ℕ → Finset ℕ) (hs : Pairwise (fun k l => Disjoint (s k) (s l)))175 (hv : ∀ k i : ℕ, i ∉ s k → v k i = 0) :176 ∃ φ : L1Sum Y →L[𝕜] 𝕜, ‖φ‖ ≤ 1 ∧ ∀ k : ℕ, φ (v k) = (‖v k‖ : 𝕜) := by177 classical178 choose ψ hψnorm hψvalue using fun k i : ℕ => exists_dual_vector'' 𝕜 (v k i)179 let α : ℕ → Y →L[𝕜] 𝕜 := fun i =>180 if h : ∃ k : ℕ, i ∈ s k then ψ h.choose i else 0181 have hαnorm : ∀ i : ℕ, ‖α i‖ ≤ 1 := by182 intro i183 dsimp [α]184 split_ifs with h185 · exact hψnorm _ _186 · simp187 have hαvalue : ∀ k i : ℕ, α i (v k i) = (‖v k i‖ : 𝕜) := by188 intro k i189 by_cases hi : i ∈ s k190 · have hex : ∃ l : ℕ, i ∈ s l := ⟨k, hi⟩191 have hk : hex.choose = k := by192 by_contra hne193 exact Finset.disjoint_left.mp (hs hne) hex.choose_spec hi194 dsimp [α]195 rw [dite_eq_left hex]196 simpa only [hk] using hψvalue hex.choose i197 · rw [hv k i hi, map_zero, norm_zero, RCLike.ofReal_zero]198 refine ⟨synthesis α 1 hαnorm, norm_synthesis_le α 1 hαnorm zero_le_one, ?_⟩199 intro k200 rw [synthesis_apply]201 simp_rw [hαvalue]202 change (∑' i : ℕ, (RCLike.ofRealCLM : ℝ →L[ℝ] 𝕜) ‖v k i‖) =203 (RCLike.ofRealCLM : ℝ →L[ℝ] 𝕜) ‖v k‖204 rw [← (RCLike.ofRealCLM : ℝ →L[ℝ] 𝕜).map_tsum (summable_norm (v k))]205 rw [← norm_eq_tsum]206207/-- The relative Schur theorem for an actual countable `ℓ₁` sum: a weakly null208sequence is norm null as soon as every coordinate is norm null. No uniform-tail209hypothesis is required; it is replaced by a proved gliding-hump contradiction. -/210theorem tendsto_zero_of_weaklyConverges_and_coordinates {x : ℕ → L1Sum Y}211 (hweak : WeaklyConverges 𝕜 (L1Sum Y) x 0)212 (hcoord : ∀ i : ℕ, Tendsto (fun k => x k i) atTop (𝓝 0)) :213 Tendsto x atTop (𝓝 0) := by214 by_contra hn215 obtain ⟨ε, hε, n, hn, s, hs, v, hv, hnorm⟩ :=216 exists_disjoint_blocks_of_not_tendsto hcoord hn217 obtain ⟨φ, hφ, hvalue⟩ := exists_dual_norming_disjoint_blocks 𝕜 v s hs hv218 have hn_top : Tendsto n atTop atTop := tendsto_atTop_mono hn tendsto_id219 have hlim : Tendsto (fun k => φ (x (n k))) atTop (𝓝 0) := by220 simpa only [Function.comp_def, map_zero] using (hweak φ).comp hn_top221 have hlimnorm := tendsto_zero_iff_norm_tendsto_zero.mp hlim222 obtain ⟨k, hk⟩ := (hlimnorm.eventually_lt_const (half_pos hε)).exists223 have herror : ‖φ (x (n k) - v k)‖ ≤ ‖x (n k) - v k‖ := by224 calc225 ‖φ (x (n k) - v k)‖ ≤ ‖φ‖ * ‖x (n k) - v k‖ := φ.le_opNorm _226 _ ≤ 1 * ‖x (n k) - v k‖ :=227 mul_le_mul_of_nonneg_right hφ (norm_nonneg _)228 _ = ‖x (n k) - v k‖ := one_mul _229 have hvalueNorm : ‖φ (v k)‖ = ‖v k‖ := by230 rw [hvalue]231 simp232 have hφtriangle : ‖v k‖ ≤ ‖φ (x (n k))‖ + ‖φ (x (n k) - v k)‖ := by233 calc234 ‖v k‖ = ‖φ (v k)‖ := hvalueNorm.symm235 _ = ‖φ (x (n k)) - φ (x (n k) - v k)‖ := by236 rw [map_sub, sub_sub_cancel]237 _ ≤ ‖φ (x (n k))‖ + ‖φ (x (n k) - v k)‖ := norm_sub_le _ _238 have hxtriangle : ‖x (n k)‖ ≤ ‖x (n k) - v k‖ + ‖v k‖ := by239 simpa only [sub_add_cancel] using norm_add_le (x (n k) - v k) (v k)240 obtain ⟨hlarge, hclose⟩ := hnorm k241 linarith242243/-- Countable `ℓ₁` sums of a Schur space are Schur. -/244theorem hasSchurProperty (hY : HasSchurProperty 𝕜 Y) :245 HasSchurProperty 𝕜 (L1Sum Y) := by246 intro x a hx247 have hweak := weaklyConverges_iff_sub_const.mp hx248 have hzero : Tendsto (fun k => x k - a) atTop (𝓝 0) := by249 apply tendsto_zero_of_weaklyConverges_and_coordinates 𝕜 hweak250 intro i251 have hc := hY _ _ (hweak.map (lp.evalCLM 𝕜 (fun _ : ℕ => Y) 1 i))252 change Tendsto (fun k => (x k - a) i) atTop (𝓝 ((0 : L1Sum Y) i)) at hc253 simpa using hc254 simpa only [sub_add_cancel, zero_add] using255 hzero.add (tendsto_const_nhds (x := a))256257end DualBlocks258259/-- Schur's theorem for the genuine scalar absolutely summable sequence space,260over either the real or complex field. -/261theorem _root_.PL1.ell1_hasSchurProperty (𝕜 : Type*) [RCLike 𝕜] :262 HasSchurProperty 𝕜 (Ell1 𝕜) := by263 apply L1Sum.hasSchurProperty 𝕜264 intro x a hx265 simpa only [ContinuousLinearMap.id_apply] using hx (ContinuousLinearMap.id 𝕜 𝕜)266267end PL1.L1Sum268269namespace PL1.IntrinsicGraph270271variable {𝕜 Y : Type*} [RCLike 𝕜]272variable [NormedAddCommGroup Y] [NormedSpace 𝕜 Y]273variable (D : ℕ → Y →L[𝕜] Y)274275/-- Coordinate Dunford–Pettis operators alone suffice for the Schur property276of the intrinsic graph. The countable `ℓ₁` argument is fully proved above. -/277theorem hasSchurProperty_of_coordinateDP278 (hcoord : ∀ n : ℕ, IsDunfordPettis (coord D n)) :279 HasSchurProperty 𝕜 (Space D) := by280 intro x a hx281 have hweak := weaklyConverges_iff_sub_const.mp hx282 have hzero : Tendsto (fun k => x k - a) atTop (𝓝 0) := by283 apply tendsto_subtype_rng.mpr284 apply L1Sum.tendsto_zero_of_weaklyConverges_and_coordinates 𝕜285 · change WeaklyConverges 𝕜 (L1Sum Y) (fun k => inclusion D (x k - a)) 0286 have hi := hweak.map (inclusion D).toContinuousLinearMap287 change WeaklyConverges 𝕜 (L1Sum Y) (fun k => inclusion D (x k - a))288 (inclusion D 0) at hi289 simpa only [map_zero] using hi290 · intro n291 simpa only [coord_apply, map_zero] using hcoord n (fun k => x k - a) 0 hweak292 simpa only [sub_add_cancel, zero_add] using293 hzero.add (tendsto_const_nhds (x := a))294295/-- Since every graph coordinate factors through coordinate zero, it suffices296to check the Dunford–Pettis property of the underlying-vector recovery map. -/297theorem hasSchurProperty_iff_evalZero_isDunfordPettis :298 HasSchurProperty 𝕜 (Space D) ↔ IsDunfordPettis (evalZero D) := by299 constructor300 · intro h x a hx301 exact ((evalZero D).continuous.tendsto a).comp (h x a hx)302 · intro h303 apply hasSchurProperty_of_coordinateDP D304 intro n305 have hfactor : coord D n = (D n).comp (evalZero D) := by306 ext x307 exact coord_eq D n x308 rw [hfactor]309 exact h.comp_left (D n)310311/-- A precise approximation criterion for the intrinsic graph's Schur property.312The uniform-tail conclusion for weakly null graph sequences is a separate,313explicit hypothesis, to be established in applications. -/314theorem hasSchurProperty_of_coordinateDP_and_uniformTails315 (hcoord : ∀ n : ℕ, IsDunfordPettis (coord D n))316 (htail : ∀ x : ℕ → Space D, WeaklyConverges 𝕜 (Space D) x 0 →317 L1Sum.HasUniformNormTails (fun k => inclusion D (x k))) :318 HasSchurProperty 𝕜 (Space D) := by319 intro x a hx320 have hweak := weaklyConverges_iff_sub_const.mp hx321 have hzero : Tendsto (fun k => x k - a) atTop (𝓝 0) := by322 apply tendsto_subtype_rng.mpr323 apply L1Sum.tendsto_zero_of_coordinates_and_uniformTails324 · intro n325 simpa only [coord_apply, map_zero] using hcoord n (fun k => x k - a) 0 hweak326 · exact htail (fun k => x k - a) hweak327 simpa only [sub_add_cancel, zero_add] using328 hzero.add (tendsto_const_nhds (x := a))329330end PL1.IntrinsicGraph331