PL1/Ell2Schur.lean

All source files · Download exact source

SHA-256: 4bd6f1064e0b85f8d5f6387d4bfee60f9fa99daee33ed5e926eca464b06af4e7

1import PL1.WeakSchur2import Mathlib.Analysis.InnerProductSpace.l2Space3import Mathlib.Analysis.InnerProductSpace.Dual45/-!6# The canonical weakly null sequence in `Ell2`78The Schur obstruction below tests the full continuous dual. Fréchet–Riesz9representation reduces this to convergence of the coordinates of a square10summable vector; the canonical unit vectors keep norm one.11-/1213noncomputable section1415open Filter16open scoped Topology1718namespace PL11920variable (𝕜 : Type*) [RCLike 𝕜]2122/-- The `n`th canonical unit vector in the genuine scalar square-summable space. -/23def ell2UnitVector (n : ℕ) : Ell2 𝕜 :=24  lp.single 2 n (1 : 𝕜)2526@[simp]27theorem norm_ell2UnitVector (n : ℕ) : ‖ell2UnitVector 𝕜 n‖ = 1 := by28  rw [ell2UnitVector, lp.norm_single (by norm_num)]29  exact norm_one3031/-- Every square-summable scalar sequence converges to zero. -/32theorem ell2_coordinates_tendsto_zero (x : Ell2 𝕜) :33    Tendsto (fun n : ℕ => x n) atTop (𝓝 0) := by34  have hsq : Summable (fun n : ℕ => ‖x n‖ ^ (2 : ℕ)) := by35    simpa using (lp.memℓp x).summable (by norm_num)36  have hsqrt := Real.continuous_sqrt.continuousAt.tendsto.comp hsq.tendsto_atTop_zero37  apply tendsto_zero_iff_norm_tendsto_zero.mpr38  simpa only [Function.comp_def, Real.sqrt_sq (norm_nonneg _), Real.sqrt_zero] using hsqrt3940/-- The canonical unit vectors are weakly null against every continuous linear41functional, over either real or complex scalars. -/42theorem ell2UnitVector_weaklyConverges_zero :43    WeaklyConverges 𝕜 (Ell2 𝕜) (ell2UnitVector 𝕜) 0 := by44  intro φ45  let x := (InnerProductSpace.toDual 𝕜 (Ell2 𝕜)).symm φ46  have hx := ell2_coordinates_tendsto_zero 𝕜 x47  have hconj := hx.star48  simp only [star_zero] at hconj49  simp only [map_zero]50  convert hconj using 151  ext n52  rw [← InnerProductSpace.toDual_symm_apply]53  change inner 𝕜 x (lp.single 2 n (1 : 𝕜)) = star (x n)54  rw [lp.inner_single_right]55  simp5657/-- The standard scalar `ℓ₂` space fails the Schur property. -/58theorem ell2_not_hasSchurProperty : ¬ HasSchurProperty 𝕜 (Ell2 𝕜) := by59  intro h60  have hv := h (ell2UnitVector 𝕜) 0 (ell2UnitVector_weaklyConverges_zero 𝕜)61  have hn := (tendsto_zero_iff_norm_tendsto_zero.mp hv)62  have hconstant : Tendsto (fun _ : ℕ => (1 : ℝ)) atTop (𝓝 0) := by63    simpa only [norm_ell2UnitVector] using hn64  exact one_ne_zero (tendsto_nhds_unique tendsto_const_nhds hconstant)6566/-- The Hilbert-space copy required in Theorem B already forces its ambient67range to fail the Schur property. -/68theorem not_hasSchurProperty_of_contains_ell269    {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]70    (hcopy : ContainsIsomorphicCopy 𝕜 (Ell2 𝕜) E) :71    ¬ HasSchurProperty 𝕜 E := by72  intro h73  exact ell2_not_hasSchurProperty 𝕜 (h.of_containsIsomorphicCopy hcopy)7475end PL176