PL1/StrongConvergence.lean

All source files · Download exact source

SHA-256: 8ab7962a59a43b82e81fbb53da0b264434818d5dfb85240c810afd807f11a64e

1import PL1.Definitions2import Mathlib.Topology.MetricSpace.UniformConvergence34/-!5# Strong convergence from a dense family67Uniformly bounded continuous linear operators converge everywhere if they8converge on a family with dense linear span. This supplies the density step9from Walsh multiplier convergence to strong convergence on actual L1.10-/1112noncomputable section13open Filter14open scoped Topology NNReal1516namespace PL11718variable {𝕜 E F ι β : Type*} [RCLike 𝕜]19  [NormedAddCommGroup E] [NormedSpace 𝕜 E]20  [NormedAddCommGroup F] [NormedSpace 𝕜 F]2122def convergenceSubmodule (T : β → E →L[𝕜] F) (T₀ : E →L[𝕜] F) (l : Filter β) :23    Submodule 𝕜 E where24  carrier := {x | Tendsto (fun b => T b x) l (𝓝 (T₀ x))}25  zero_mem' := by simpa using (tendsto_const_nhds (x := (0 : F)) (f := l))26  add_mem' := by27    intro x y hx hy28    simpa only [Set.mem_ofPred_eq, map_add] using hx.add hy29  smul_mem' := by30    intro c x hx31    simpa only [Set.mem_ofPred_eq, map_smul] using hx.const_smul c3233theorem isClosed_convergenceSubmodule (T : β → E →L[𝕜] F) (T₀ : E →L[𝕜] F)34    (l : Filter β) (C : ℝ≥0) (hT : ∀ b, ‖T b‖ ≤ C) :35    IsClosed (convergenceSubmodule T T₀ l : Set E) := by36  have hLip (b : β) : LipschitzWith C (T b) :=37    (T b).lipschitzWith.weaken (show ‖T b‖₊ ≤ C from hT b)38  exact (LipschitzWith.uniformEquicontinuous (fun b => T b) C hLip).equicontinuous39    |>.isClosed_setOfPred_tendsto T₀.continuous4041/-- The complete density argument for a uniformly bounded operator family. -/42theorem tendsto_apply_of_dense_span (v : ι → E)43    (hv : Dense (Submodule.span 𝕜 (Set.range v) : Set E))44    (T : β → E →L[𝕜] F) (T₀ : E →L[𝕜] F) (l : Filter β)45    (C : ℝ≥0) (hT : ∀ b, ‖T b‖ ≤ C)46    (h : ∀ i, Tendsto (fun b => T b (v i)) l (𝓝 (T₀ (v i)))) (x : E) :47    Tendsto (fun b => T b x) l (𝓝 (T₀ x)) := by48  have hs : Submodule.span 𝕜 (Set.range v) ≤ convergenceSubmodule T T₀ l := by49    apply Submodule.span_le.mpr50    rintro y ⟨i, rfl⟩51    exact h i52  have hcl := isClosed_convergenceSubmodule T T₀ l C hT53  exact hcl.closure_subset_iff.mpr hs (hv x)5455end PL156