PL1/DunfordPettis.lean
All source files · Download exact source
SHA-256: b5b3560c2f9682781b5a46d3fcabdad890f8aa0d0bb33c1b2b1fcca08755fd81
1import PL1.WeakSchur2import Mathlib.Analysis.Normed.Module.DoubleDual3import Mathlib.Analysis.Normed.Operator.BanachSteinhaus4import Mathlib.Analysis.Normed.Operator.Compact.Basic5import Mathlib.Topology.Algebra.Module.FiniteDimension67/-!8# Finite-rank approximation and Dunford–Pettis operators910The boundedness of weakly convergent sequences is proved using Banach–Steinhaus11and the canonical isometric embedding into the double dual. It is not an extra12hypothesis in the approximation results.13-/1415noncomputable section1617open Filter18open scoped Topology1920namespace PL12122variable {𝕜 : Type*} [RCLike 𝕜]23variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]24variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]2526theorem isDunfordPettis_zero : IsDunfordPettis (0 : E →L[𝕜] F) := by27 intro x a hx28 exact tendsto_const_nhds2930theorem IsDunfordPettis.add {S T : E →L[𝕜] F}31 (hS : IsDunfordPettis S) (hT : IsDunfordPettis T) : IsDunfordPettis (S + T) := by32 intro x a hx33 exact (hS x a hx).add (hT x a hx)3435theorem IsDunfordPettis.smul {T : E →L[𝕜] F} (hT : IsDunfordPettis T) (c : 𝕜) :36 IsDunfordPettis (c • T) := by37 intro x a hx38 exact (hT x a hx).const_smul c3940/-- The Dunford–Pettis operators are a linear subspace of bounded operators. -/41def dunfordPettisSubmodule : Submodule 𝕜 (E →L[𝕜] F) where42 carrier := {T | IsDunfordPettis T}43 zero_mem' := isDunfordPettis_zero44 add_mem' := fun hS hT => hS.add hT45 smul_mem' := fun c _T hT => hT.smul c4647/-- Weakly convergent sequences are norm bounded; completeness of E is unnecessary. -/48theorem WeaklyConverges.exists_norm_bound {x : ℕ → E} {a : E}49 (hx : WeaklyConverges 𝕜 E x a) : ∃ C : ℝ, ∀ n, ‖x n‖ ≤ C := by50 obtain ⟨C, hC⟩ := banach_steinhaus51 (g := fun n => NormedSpace.inclusionInDoubleDual 𝕜 E (x n)) (by52 intro φ53 obtain ⟨C, hC⟩ := (Metric.isBounded_range_of_tendsto _ (hx φ)).exists_norm_le54 exact ⟨C, fun n => hC _ ⟨n, rfl⟩⟩)55 refine ⟨C, fun n => ?_⟩56 have hn := hC n57 change ‖NormedSpace.inclusionInDoubleDualLi 𝕜 (x n)‖ ≤ C at hn58 rw [(NormedSpace.inclusionInDoubleDualLi 𝕜).norm_map] at hn59 exact hn6061/-- A strictly positive uniform bound is convenient for quantitative approximation. -/62theorem WeaklyConverges.exists_pos_norm_bound {x : ℕ → E} {a : E}63 (hx : WeaklyConverges 𝕜 E x a) : ∃ C : ℝ, 0 < C ∧ ∀ n, ‖x n‖ ≤ C := by64 obtain ⟨C, hC⟩ := hx.exists_norm_bound65 exact ⟨max C 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _),66 fun n => (hC n).trans (le_max_left _ _)⟩6768theorem WeaklyConverges.isBounded_range {x : ℕ → E} {a : E}69 (hx : WeaklyConverges 𝕜 E x a) : Bornology.IsBounded (Set.range x) := by70 obtain ⟨C, hC⟩ := hx.exists_norm_bound71 exact isBounded_iff_forall_norm_le.mpr ⟨C, by simpa using hC⟩7273/-- The full dual separates points, so a weak limit in a normed space is unique. -/74theorem WeaklyConverges.unique {x : ℕ → E} {a b : E}75 (ha : WeaklyConverges 𝕜 E x a) (hb : WeaklyConverges 𝕜 E x b) : a = b := by76 apply (SeparatingDual.eq_iff_forall_dual_eq (R := 𝕜)).mpr77 intro φ78 exact tendsto_nhds_unique (ha φ) (hb φ)7980theorem WeaklyConverges.subseq {x : ℕ → E} {a : E}81 (hx : WeaklyConverges 𝕜 E x a) {r : ℕ → ℕ} (hr : StrictMono r) :82 WeaklyConverges 𝕜 E (x ∘ r) a := by83 intro φ84 exact (hx φ).comp hr.tendsto_atTop8586/-- A weakly convergent sequence contained in a norm-compact set converges in norm. -/87theorem WeaklyConverges.tendsto_of_isCompact {x : ℕ → E} {a : E}88 (hx : WeaklyConverges 𝕜 E x a) {K : Set E} (hK : IsCompact K)89 (hxK : ∀ n, x n ∈ K) : Tendsto x atTop (𝓝 a) := by90 by_contra hconv91 rw [Metric.tendsto_atTop] at hconv92 push Not at hconv93 obtain ⟨ε, hε, hbad⟩ := hconv94 have hcompact : IsCompact (K ∩ {y : E | ε ≤ dist y a}) :=95 hK.inter_right (isClosed_le continuous_const (continuous_id.dist continuous_const))96 have hfreq : ∃ᶠ n in atTop, x n ∈ K ∩ {y : E | ε ≤ dist y a} := by97 apply frequently_atTop.mpr98 intro N99 obtain ⟨n, hn, hdist⟩ := hbad N100 exact ⟨n, hn, hxK n, hdist⟩101 obtain ⟨b, hb, r, hr, hsub⟩ := hcompact.tendsto_subseq' hfreq102 have hba : b = a := (weaklyConverges_of_tendsto hsub).unique (hx.subseq hr)103 have hbε : ε ≤ 0 := by104 simpa only [Set.mem_ofPred_eq, hba, dist_self] using hb.2105 exact (not_le_of_gt hε) hbε106107/-- Relative norm compactness is enough in the previous result. -/108theorem WeaklyConverges.tendsto_of_isCompact_closure {x : ℕ → E} {a : E}109 (hx : WeaklyConverges 𝕜 E x a) (hc : IsCompact (closure (Set.range x))) :110 Tendsto x atTop (𝓝 a) :=111 hx.tendsto_of_isCompact hc (fun n => subset_closure ⟨n, rfl⟩)112113/-- In a Banach space, a weakly convergent sequence with totally bounded range114converges in norm. This is the compactness step in the paper's restriction criterion. -/115theorem WeaklyConverges.tendsto_of_totallyBounded [CompleteSpace E]116 {x : ℕ → E} {a : E} (hx : WeaklyConverges 𝕜 E x a)117 (htb : TotallyBounded (Set.range x)) : Tendsto x atTop (𝓝 a) :=118 hx.tendsto_of_isCompact_closure (htb.closure.isCompact_of_isClosed isClosed_closure)119120/-- Finite-dimensional normed spaces have the Schur property. -/121theorem hasSchurProperty_of_finiteDimensional [FiniteDimensional 𝕜 E] :122 HasSchurProperty 𝕜 E := by123 let e := (Module.finBasis 𝕜 E).equivFunL124 intro x a hx125 have hcoord : Tendsto (fun n => e (x n)) atTop (𝓝 (e a)) := by126 apply tendsto_pi_nhds.mpr127 intro i128 exact hx ((ContinuousLinearMap.proj i).comp e.toContinuousLinearMap)129 simpa [Function.comp_def] using (e.symm.continuous.tendsto (e a)).comp hcoord130131/-- Every bounded linear operator of finite rank is Dunford–Pettis. -/132theorem isDunfordPettis_of_finiteDimensional_range (T : E →L[𝕜] F)133 [FiniteDimensional 𝕜 T.range] : IsDunfordPettis T :=134 isDunfordPettis_of_hasSchurProperty_range T hasSchurProperty_of_finiteDimensional135136/-- Limits in operator norm of Dunford–Pettis operators are Dunford–Pettis. -/137theorem isDunfordPettis_of_tendsto {T : ℕ → E →L[𝕜] F} {S : E →L[𝕜] F}138 (hT : ∀ m, IsDunfordPettis (T m)) (hlim : Tendsto T atTop (𝓝 S)) :139 IsDunfordPettis S := by140 apply (isDunfordPettis_iff_weaklyNull S).mpr141 intro x hx142 obtain ⟨C, hC, hbound⟩ := hx.exists_pos_norm_bound143 apply Metric.tendsto_atTop.mpr144 intro ε hε145 obtain ⟨m, hm⟩ := Metric.tendsto_atTop.mp hlim (ε / (2 * C)) (by positivity)146 have happrox : ‖S - T m‖ < ε / (2 * C) := by147 simpa only [dist_eq_norm, norm_sub_rev] using hm m le_rfl148 have hmnull := (isDunfordPettis_iff_weaklyNull (T m)).mp (hT m) x hx149 obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hmnull (ε / 2) (by positivity)150 refine ⟨N, fun n hn => ?_⟩151 have hsmall : ‖T m (x n)‖ < ε / 2 := by152 simpa only [dist_zero_right] using hN n hn153 have happroxC : ‖S - T m‖ * C < ε / 2 := by154 have h := (lt_div_iff₀ (mul_pos (by norm_num) hC)).mp happrox155 nlinarith156 rw [dist_zero_right]157 calc158 ‖S (x n)‖ ≤ ‖(S - T m) (x n)‖ + ‖T m (x n)‖ := by159 simpa only [sub_apply, sub_add_cancel] using160 norm_add_le ((S - T m) (x n)) (T m (x n))161 _ ≤ ‖S - T m‖ * C + ‖T m (x n)‖ := by162 gcongr163 exact ((S - T m).le_opNorm (x n)).trans164 (mul_le_mul_of_nonneg_left (hbound n) (norm_nonneg _))165 _ < ε := by linarith166167/-- The Dunford–Pettis operators form a closed set in operator norm. -/168theorem isClosed_setOf_isDunfordPettis :169 IsClosed {T : E →L[𝕜] F | IsDunfordPettis T} := by170 apply isSeqClosed_iff_isClosed.mp171 intro T S hT hlim172 exact isDunfordPettis_of_tendsto hT hlim173174theorem isDunfordPettis_sum {ι : Type*} (s : Finset ι) (T : ι → E →L[𝕜] F)175 (hT : ∀ i ∈ s, IsDunfordPettis (T i)) : IsDunfordPettis (∑ i ∈ s, T i) := by176 change (∑ i ∈ s, T i) ∈ (dunfordPettisSubmodule : Submodule 𝕜 (E →L[𝕜] F))177 exact Submodule.sum_mem _ hT178179/-- A summable series of Dunford–Pettis operators has a Dunford–Pettis sum. -/180theorem isDunfordPettis_tsum {ι : Type*} {T : ι → E →L[𝕜] F}181 (hT : ∀ i, IsDunfordPettis (T i)) (hsum : Summable T) :182 IsDunfordPettis (∑' i, T i) := by183 apply isClosed_setOf_isDunfordPettis.mem_of_tendsto hsum.hasSum184 exact Eventually.of_forall (fun s => isDunfordPettis_sum s T (fun i _ => hT i))185186/-- In particular, every operator approximable in norm by finite-rank operators187is Dunford–Pettis. -/188theorem isDunfordPettis_of_finiteRank_approximation189 {T : ℕ → E →L[𝕜] F} {S : E →L[𝕜] F}190 (hfinite : ∀ m, FiniteDimensional 𝕜 (T m).range)191 (hlim : Tendsto T atTop (𝓝 S)) : IsDunfordPettis S := by192 apply isDunfordPettis_of_tendsto (T := T) _ hlim193 intro m194 let := hfinite m195 exact isDunfordPettis_of_finiteDimensional_range (T m)196197/-- Every compact continuous linear operator is Dunford–Pettis. The proof uses198compactness itself, and imposes no approximation property on either space. -/199theorem isDunfordPettis_of_isCompactOperator (T : E →L[𝕜] F)200 (hT : IsCompactOperator T) : IsDunfordPettis T := by201 intro x a hx202 obtain ⟨K, hK, hTxK⟩ := hT.image_subset_compact_of_bounded hx.isBounded_range203 exact (hx.map T).tendsto_of_isCompact hK (fun n => hTxK ⟨x n, ⟨n, rfl⟩, rfl⟩)204205end PL1206