PL1/WeakSequentialCompleteness.lean

All source files · Download exact source

SHA-256: 3e85198399e108b93f2d24ee22b1a03ed3023bd4484f9052a24d68dd16133a41

1import PL1.SchurBoundedCompleteness23/-! # Weak sequential completeness with the entire continuous dual45The generic Schur argument is reused from `SchurBoundedCompleteness`.6A weak Cauchy sequence in a complete Schur space has an actual norm limit,7and therefore a weak limit against every continuous linear functional.8-/910noncomputable section11open Filter12open scoped Topology13namespace PL11415variable {K E F : Type*} [RCLike K] [NormedAddCommGroup E] [NormedSpace K E]16  [NormedAddCommGroup F] [NormedSpace K F]1718/-- Every member of the full continuous dual sends the sequence to a Cauchy sequence. -/19abbrev WeaklyCauchy (K E : Type*) [RCLike K] [NormedAddCommGroup E] [NormedSpace K E]20    (x : ℕ → E) : Prop := SchurBoundedCompleteness.WeaklyCauchy (𝕜 := K) x2122/-- Weak sequential completeness uses the original continuous dual and original space. -/23def IsWeaklySequentiallyComplete (K E : Type*) [RCLike K]24    [NormedAddCommGroup E] [NormedSpace K E] : Prop :=25  ∀ x : ℕ → E, WeaklyCauchy K E x → ∃ a : E, WeaklyConverges K E x a2627theorem WeaklyCauchy.map {x : ℕ → E} (hx : WeaklyCauchy K E x) (T : E →L[K] F) :28    WeaklyCauchy K F (fun n => T (x n)) := fun φ => hx (φ.comp T)2930/-- Completeness of the space is unnecessary for the norm Cauchy conclusion. -/31theorem HasSchurProperty.cauchySeq_of_weaklyCauchy (hS : HasSchurProperty K E)32    {x : ℕ → E} (hx : WeaklyCauchy K E x) : CauchySeq x :=33  SchurBoundedCompleteness.cauchySeq_of_weaklyCauchy hS hx3435/-- A weak Cauchy sequence in a complete Schur space converges in its original norm. -/36theorem HasSchurProperty.exists_norm_limit_of_weaklyCauchy [CompleteSpace E]37    (hS : HasSchurProperty K E) {x : ℕ → E} (hx : WeaklyCauchy K E x) :38    ∃ a : E, Tendsto x atTop (𝓝 a) :=39  SchurBoundedCompleteness.exists_tendsto_of_weaklyCauchy hS hx4041/-- Every complete Schur space is weakly sequentially complete. -/42theorem HasSchurProperty.isWeaklySequentiallyComplete [CompleteSpace E]43    (hS : HasSchurProperty K E) : IsWeaklySequentiallyComplete K E := by44  intro x hx45  obtain ⟨a, ha⟩ := hS.exists_norm_limit_of_weaklyCauchy hx46  exact ⟨a, weaklyConverges_of_tendsto ha⟩4748/-- Failure of norm Cauchy convergence in a Schur space is witnessed by a genuine dual functional. -/49theorem HasSchurProperty.exists_dual_not_cauchy (hS : HasSchurProperty K E)50    {x : ℕ → E} (hx : ¬ CauchySeq x) : ∃ φ : E →L[K] K, ¬ CauchySeq (fun n => φ (x n)) := by51  by_contra h52  push Not at h53  exact hx (hS.cauchySeq_of_weaklyCauchy h)5455/-- The same dual witness oscillates by a fixed positive amount arbitrarily far out. -/56theorem HasSchurProperty.exists_dual_oscillation (hS : HasSchurProperty K E)57    {x : ℕ → E} (hx : ¬ CauchySeq x) :58    ∃ (φ : E →L[K] K) (ε : ℝ), 0 < ε ∧59      ∀ N : ℕ, ∃ m ≥ N, ∃ n ≥ N, ε ≤ ‖φ (x m) - φ (x n)‖ := by60  obtain ⟨φ, hφ⟩ := hS.exists_dual_not_cauchy hx61  rw [Metric.cauchySeq_iff] at hφ62  push Not at hφ63  simpa only [dist_eq_norm] using (show ∃ (φ : E →L[K] K) (ε : ℝ), 0 < ε ∧64    ∀ N : ℕ, ∃ m ≥ N, ∃ n ≥ N, ε ≤ dist (φ (x m)) (φ (x n)) from ⟨φ, hφ⟩)6566#print axioms HasSchurProperty.isWeaklySequentiallyComplete67#print axioms HasSchurProperty.exists_dual_oscillation68end PL169