PL1/WeakSchur.lean
All source files · Download exact source
SHA-256: 31066997371ca8e84a4c31d6dd857bbff88a73b23445d668958e0099698b497d
1import PL1.Definitions2import Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict34/-!5# Weak convergence, the Schur property, and Dunford–Pettis projections67These lemmas concern the reviewed predicates in `PL1.Definitions`. In particular,8all weak convergence statements use the full continuous dual. No construction of9the main counterexamples is assumed or asserted in this module.10-/1112noncomputable section1314open Filter15open scoped Topology1617namespace PL11819variable {𝕜 : Type*} [RCLike 𝕜]20variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]21variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]22variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]2324/-- Every continuous linear map preserves weak sequential convergence. -/25theorem WeaklyConverges.map {x : ℕ → E} {a : E}26 (hx : WeaklyConverges 𝕜 E x a) (T : E →L[𝕜] F) :27 WeaklyConverges 𝕜 F (fun n => T (x n)) (T a) := by28 intro φ29 exact hx (φ.comp T)3031/-- Norm convergence implies weak convergence. -/32theorem weaklyConverges_of_tendsto {x : ℕ → E} {a : E}33 (hx : Tendsto x atTop (𝓝 a)) : WeaklyConverges 𝕜 E x a := by34 intro φ35 exact (φ.continuous.tendsto a).comp hx3637theorem weaklyConverges_const (a : E) :38 WeaklyConverges 𝕜 E (fun _ : ℕ => a) a :=39 weaklyConverges_of_tendsto tendsto_const_nhds4041theorem WeaklyConverges.sub {x y : ℕ → E} {a b : E}42 (hx : WeaklyConverges 𝕜 E x a) (hy : WeaklyConverges 𝕜 E y b) :43 WeaklyConverges 𝕜 E (fun n => x n - y n) (a - b) := by44 intro φ45 simpa only [map_sub] using (hx φ).sub (hy φ)4647/-- Subtracting the proposed limit converts weak convergence into weak nullity. -/48theorem weaklyConverges_iff_sub_const {x : ℕ → E} {a : E} :49 WeaklyConverges 𝕜 E x a ↔50 WeaklyConverges 𝕜 E (fun n => x n - a) 0 := by51 constructor52 · intro hx53 simpa using hx.sub (weaklyConverges_const a)54 · intro hx φ55 have h := (hx φ).add (tendsto_const_nhds (x := φ a))56 simpa only [map_sub, map_zero, sub_add_cancel, zero_add] using h5758/-- A continuous linear equivalence preserves and reflects weak convergence. -/59theorem weaklyConverges_equiv_iff (e : E ≃L[𝕜] F) {x : ℕ → E} {a : E} :60 WeaklyConverges 𝕜 F (fun n => e (x n)) (e a) ↔61 WeaklyConverges 𝕜 E x a := by62 constructor63 · intro hx64 simpa using hx.map e.symm.toContinuousLinearMap65 · intro hx66 exact hx.map e.toContinuousLinearMap6768/-- The Schur property is invariant under Banach-space isomorphisms. -/69theorem hasSchurProperty_equiv_iff (e : E ≃L[𝕜] F) :70 HasSchurProperty 𝕜 E ↔ HasSchurProperty 𝕜 F := by71 constructor72 · intro h x a hx73 have h' := h (fun n => e.symm (x n)) (e.symm a)74 (hx.map e.symm.toContinuousLinearMap)75 simpa [Function.comp_def] using (e.continuous.tendsto (e.symm a)).comp h'76 · intro h x a hx77 have h' := h (fun n => e (x n)) (e a) (hx.map e.toContinuousLinearMap)78 simpa [Function.comp_def] using (e.symm.continuous.tendsto (e a)).comp h'7980/-- Every linear subspace of a Schur space is Schur, with its induced norm. -/81theorem HasSchurProperty.submodule (h : HasSchurProperty 𝕜 E)82 (V : Submodule 𝕜 E) : HasSchurProperty 𝕜 V := by83 intro x a hx84 apply tendsto_subtype_rng.mpr85 exact h _ _ (hx.map V.subtypeL)8687/-- A space isomorphic to a closed subspace of a Schur space is Schur. -/88theorem HasSchurProperty.of_containsIsomorphicCopy (h : HasSchurProperty 𝕜 E)89 (hcopy : ContainsIsomorphicCopy 𝕜 F E) : HasSchurProperty 𝕜 F := by90 obtain ⟨V, _, ⟨e⟩⟩ := hcopy91 exact (hasSchurProperty_equiv_iff e).mpr (h.submodule V)9293/-- Consequently a Schur space cannot contain an isomorphic copy of a non-Schur space. -/94theorem HasSchurProperty.not_containsIsomorphicCopy (h : HasSchurProperty 𝕜 E)95 (hF : ¬ HasSchurProperty 𝕜 F) : ¬ ContainsIsomorphicCopy 𝕜 F E := by96 intro hcopy97 exact hF (h.of_containsIsomorphicCopy hcopy)9899/-- Any operator with Schur codomain is Dunford–Pettis. -/100theorem HasSchurProperty.isDunfordPettis (h : HasSchurProperty 𝕜 F)101 (T : E →L[𝕜] F) : IsDunfordPettis T := by102 intro x a hx103 exact h _ _ (hx.map T)104105/-- Precomposition by a bounded operator preserves the Dunford–Pettis property. -/106theorem IsDunfordPettis.comp_right {T : F →L[𝕜] G}107 (hT : IsDunfordPettis T) (S : E →L[𝕜] F) : IsDunfordPettis (T.comp S) := by108 intro x a hx109 exact hT _ _ (hx.map S)110111/-- Postcomposition by a bounded operator preserves the Dunford–Pettis property. -/112theorem IsDunfordPettis.comp_left {T : E →L[𝕜] F}113 (hT : IsDunfordPettis T) (S : F →L[𝕜] G) : IsDunfordPettis (S.comp T) := by114 intro x a hx115 exact (S.continuous.tendsto (T a)).comp (hT x a hx)116117/-- The reviewed all-limits definition agrees with the weak-null definition in the paper. -/118theorem isDunfordPettis_iff_weaklyNull (T : E →L[𝕜] F) :119 IsDunfordPettis T ↔120 ∀ x : ℕ → E, WeaklyConverges 𝕜 E x 0 →121 Tendsto (fun n => T (x n)) atTop (𝓝 0) := by122 constructor123 · intro h x hx124 simpa only [map_zero] using h x 0 hx125 · intro h x a hx126 have h' := h (fun n => x n - a) (weaklyConverges_iff_sub_const.mp hx)127 have h'' := h'.add (tendsto_const_nhds (x := T a))128 simpa only [map_sub, sub_add_cancel, zero_add] using h''129130/-- An idempotent continuous operator is the identity on its range. -/131theorem IsProjection.apply_range {P : E →L[𝕜] E} (hP : IsProjection P)132 (x : P.range) : P x = (x : E) := by133 obtain ⟨y, hy⟩ := x.property134 change P y = (x : E) at hy135 have h := DFunLike.congr_fun hP y136 simpa only [ContinuousLinearMap.comp_apply, hy] using h137138/-- The range of any continuous projection is closed. -/139theorem IsProjection.isClosed_range {P : E →L[𝕜] E} (hP : IsProjection P) :140 IsClosed (P.range : Set E) := by141 apply ContinuousLinearMap.IsIdempotentElem.isClosed_range142 exact hP143144/-- The key abstract implication in Proposition 4.3: a Dunford–Pettis projection145has a Schur range, with the actual inherited range norm. -/146theorem IsProjection.hasSchurProperty_range {P : E →L[𝕜] E}147 (hP : IsProjection P) (hDP : IsDunfordPettis P) :148 HasSchurProperty 𝕜 P.range := by149 intro x a hx150 apply tendsto_subtype_rng.mpr151 have h := hDP (fun n => (x n : E)) (a : E) (hx.map P.range.subtypeL)152 simpa only [hP.apply_range] using h153154/-- An operator whose actual range is Schur is Dunford–Pettis. No idempotence155is needed for this direction. -/156theorem isDunfordPettis_of_hasSchurProperty_range (T : E →L[𝕜] F)157 (h : HasSchurProperty 𝕜 T.range) : IsDunfordPettis T := by158 intro x a hx159 have h' := h (fun n => T.rangeRestrict (x n)) (T.rangeRestrict a)160 (hx.map T.rangeRestrict)161 exact tendsto_subtype_rng.mp h'162163/-- A continuous projection is Dunford–Pettis exactly when its range is Schur. -/164theorem IsProjection.isDunfordPettis_iff_hasSchurProperty_range165 {P : E →L[𝕜] E} (hP : IsProjection P) :166 IsDunfordPettis P ↔ HasSchurProperty 𝕜 P.range :=167 ⟨hP.hasSchurProperty_range, isDunfordPettis_of_hasSchurProperty_range P⟩168169end PL1170