PL1/SchurBoundedCompleteness.lean
All source files · Download exact source
SHA-256: 4af58f8063b84818b727acca1dd1a4aeb1680d6054fdc94dee2450f2ed7e1d23
1import PL1.WeakSchur2import Mathlib.Topology.Algebra.InfiniteSum.Real3import Mathlib.Analysis.Normed.Group.InfiniteSum45/-!6# Weak Cauchy sequences and bounded signed expansions in Schur spaces78These proofs give the bounded-completeness step in the paper's lattice lemma.9They do not assume or assert that an atomic lattice basis has already been constructed.10-/1112noncomputable section13open Filter14open scoped Topology1516namespace PL1.SchurBoundedCompleteness1718section GeneralScalar1920variable {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E]2122/-- Weak Cauchy convergence is tested against the entire continuous dual. -/23def WeaklyCauchy (x : ℕ → E) : Prop :=24 ∀ φ : E →L[𝕜] 𝕜, CauchySeq (fun n => φ (x n))2526/-- A Schur space sends every weak Cauchy sequence to a norm Cauchy sequence. -/27theorem cauchySeq_of_weaklyCauchy (hS : HasSchurProperty 𝕜 E) {x : ℕ → E}28 (hx : WeaklyCauchy (𝕜 := 𝕜) x) : CauchySeq x := by29 by_contra hbad30 rw [Metric.cauchySeq_iff] at hbad31 push Not at hbad32 obtain ⟨ε, hε, hbad⟩ := hbad33 choose a ha b hb hab using hbad34 have hat : Tendsto a atTop atTop := tendsto_atTop_mono ha tendsto_id35 have hbt : Tendsto b atTop atTop := tendsto_atTop_mono hb tendsto_id36 have hweak : WeaklyConverges 𝕜 E (fun n => x (a n) - x (b n)) 0 := by37 intro φ38 obtain ⟨c, hc⟩ := cauchySeq_tendsto_of_complete (hx φ)39 simpa only [map_sub, map_zero, sub_self, Function.comp_apply] using (hc.comp hat).sub (hc.comp hbt)40 have hn := (hS _ _ hweak).norm41 simp only [norm_zero] at hn42 have he := hn.eventually_lt_const hε43 obtain ⟨n, hn⟩ := he.exists44 exact (not_lt_of_ge (hab n)) (by simpa only [dist_eq_norm] using hn)4546/-- Completeness upgrades weak Cauchy sequences in a Schur space to norm convergence. -/47theorem exists_tendsto_of_weaklyCauchy [CompleteSpace E] (hS : HasSchurProperty 𝕜 E)48 {x : ℕ → E} (hx : WeaklyCauchy (𝕜 := 𝕜) x) : ∃ a : E, Tendsto x atTop (𝓝 a) :=49 cauchySeq_tendsto_of_complete (cauchySeq_of_weaklyCauchy hS hx)5051/-- In a complete Schur space, scalar summability against every continuous52functional forces genuine unordered vector summability. -/53theorem summable_of_dual_summable [CompleteSpace E] (hS : HasSchurProperty 𝕜 E)54 (x : ℕ → E) (hx : ∀ φ : E →L[𝕜] 𝕜, Summable (fun n => φ (x n))) : Summable x := by55 classical56 by_contra hbad57 rw [summable_iff_vanishing_norm] at hbad58 push Not at hbad59 obtain ⟨ε, hε, hbad⟩ := hbad60 choose t ht hnorm using fun n : ℕ => hbad (Finset.range n)61 have hweak : WeaklyConverges 𝕜 E (fun n => ∑ j ∈ t n, x j) 0 := by62 intro φ63 rw [map_zero]64 apply Metric.tendsto_atTop.mpr65 intro δ hδ66 obtain ⟨s, hs⟩ := summable_iff_vanishing_norm.1 (hx φ) δ hδ67 obtain ⟨N, hN⟩ := Finset.exists_nat_subset_range s68 refine ⟨N, fun n hn => ?_⟩69 simpa only [map_sum, dist_zero_right] using70 hs (t n) ((ht n).mono_right (hN.trans (Finset.range_mono hn)))71 have hz := (hS _ _ hweak).norm72 simp only [norm_zero] at hz73 obtain ⟨n, hn⟩ := (hz.eventually_lt_const hε).exists74 exact not_lt_of_ge (hnorm n) hn7576end GeneralScalar7778section RealScalar7980variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]8182/-- One bound for every finite initial signed sum. -/83def SignedSumsBounded (x : ℕ → E) (M : ℝ) : Prop :=84 ∀ (N : ℕ) (ε : ℕ → ℝ), (∀ n, ε n = 1 ∨ ε n = -1) →85 ‖∑ n ∈ Finset.range N, ε n • x n‖ ≤ M8687/-- Scalar signs can recover the entire finite sum of absolute dual values. -/88theorem sum_dual_norm_le_of_signed_sums_bounded (x : ℕ → E) (M : ℝ)89 (hM : SignedSumsBounded x M) (φ : E →L[ℝ] ℝ) (N : ℕ) :90 (∑ n ∈ Finset.range N, ‖φ (x n)‖) ≤ ‖φ‖ * M := by91 classical92 let ε : ℕ → ℝ := fun n => if 0 ≤ φ (x n) then 1 else -193 have hε : ∀ n, ε n = 1 ∨ ε n = -1 := by intro n; dsimp [ε]; split <;> simp94 have heq : φ (∑ n ∈ Finset.range N, ε n • x n) =95 ∑ n ∈ Finset.range N, ‖φ (x n)‖ := by96 rw [map_sum]97 apply Finset.sum_congr rfl98 intro n hn99 rw [map_smul]100 by_cases h : 0 ≤ φ (x n)101 · simp [ε, h, Real.norm_of_nonneg h]102 · simp [ε, h, Real.norm_eq_abs, abs_of_neg (lt_of_not_ge h)]103 rw [← heq]104 calc105 _ ≤ ‖φ (∑ n ∈ Finset.range N, ε n • x n)‖ := le_abs_self _106 _ ≤ ‖φ‖ * ‖∑ n ∈ Finset.range N, ε n • x n‖ := φ.le_opNorm _107 _ ≤ ‖φ‖ * M := mul_le_mul_of_nonneg_left (hM N ε hε) (norm_nonneg _)108109/-- Every continuous functional is absolutely summable on a series with bounded signed sums. -/110theorem dual_summable_norm_of_signed_sums_bounded (x : ℕ → E) (M : ℝ)111 (hM : SignedSumsBounded x M) (φ : E →L[ℝ] ℝ) :112 Summable (fun n => ‖φ (x n)‖) :=113 summable_of_sum_range_le (fun _ => norm_nonneg _)114 (sum_dual_norm_le_of_signed_sums_bounded x M hM φ)115116/-- Bounded signed sums force the terms themselves to be weakly null. -/117theorem weaklyConverges_zero_of_signed_sums_bounded (x : ℕ → E) (M : ℝ)118 (hM : SignedSumsBounded x M) : WeaklyConverges ℝ E x 0 := by119 intro φ120 simpa only [map_zero] using121 (dual_summable_norm_of_signed_sums_bounded x M hM φ).of_norm.tendsto_atTop_zero122123/-- Partial sums are weak Cauchy under the same signed-sum bound. -/124theorem weaklyCauchy_partialSums_of_signed_sums_bounded (x : ℕ → E) (M : ℝ)125 (hM : SignedSumsBounded x M) :126 WeaklyCauchy (𝕜 := ℝ) (fun N => ∑ n ∈ Finset.range N, x n) := by127 intro φ128 have h := (dual_summable_norm_of_signed_sums_bounded x M hM φ).of_norm.hasSum.tendsto_sum_nat129 simpa only [map_sum] using h.cauchySeq130131/-- In a complete Schur space, every series with uniformly bounded signed partial sums converges. -/132theorem exists_tendsto_partialSums_of_signed_sums_bounded [CompleteSpace E]133 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (M : ℝ) (hM : SignedSumsBounded x M) :134 ∃ a : E, Tendsto (fun N => ∑ n ∈ Finset.range N, x n) atTop (𝓝 a) :=135 exists_tendsto_of_weaklyCauchy hS (weaklyCauchy_partialSums_of_signed_sums_bounded x M hM)136137/-- Uniformly bounded signed partial sums in a complete real Schur space138converge unconditionally, in Mathlib's full finite-subset sense. -/139theorem summable_of_signed_sums_bounded [CompleteSpace E]140 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (M : ℝ) (hM : SignedSumsBounded x M) :141 Summable x :=142 summable_of_dual_summable hS x143 (fun φ => (dual_summable_norm_of_signed_sums_bounded x M hM φ).of_norm)144145/-- A uniform bound on finite sign transformations converts bounded ordinary partial sums146into bounded signed partial sums. -/147theorem signedSumsBounded_of_sign_transform_bound (x : ℕ → E) (C M : ℝ) (hC : 0 ≤ C)148 (hpartial : ∀ N, ‖∑ n ∈ Finset.range N, x n‖ ≤ M)149 (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ), (∀ n, ε n = 1 ∨ ε n = -1) →150 ‖∑ n ∈ Finset.range N, ε n • x n‖ ≤ C * ‖∑ n ∈ Finset.range N, x n‖) :151 SignedSumsBounded x (C * M) := by152 intro N ε hε153 exact (htransform N ε hε).trans (mul_le_mul_of_nonneg_left (hpartial N) hC)154155/-- The bounded-completeness argument for an unconditional expansion in a Schur space. -/156theorem bounded_completeness_of_sign_transform_bound [CompleteSpace E]157 (hS : HasSchurProperty ℝ E) (x : ℕ → E) (C M : ℝ) (hC : 0 ≤ C)158 (hpartial : ∀ N, ‖∑ n ∈ Finset.range N, x n‖ ≤ M)159 (htransform : ∀ (N : ℕ) (ε : ℕ → ℝ), (∀ n, ε n = 1 ∨ ε n = -1) →160 ‖∑ n ∈ Finset.range N, ε n • x n‖ ≤ C * ‖∑ n ∈ Finset.range N, x n‖) :161 ∃ a : E, Tendsto (fun N => ∑ n ∈ Finset.range N, x n) atTop (𝓝 a) :=162 exists_tendsto_partialSums_of_signed_sums_bounded hS x (C * M)163 (signedSumsBounded_of_sign_transform_bound x C M hC hpartial htransform)164165end RealScalar166end PL1.SchurBoundedCompleteness167168169