Extending bounded-operator convergence from dense subsets

This file records two standard density arguments for uniformly bounded families of continuous linear maps. Pointwise convergence on a dense subset extends to pointwise convergence everywhere, and uniform Cauchy convergence on a parameter set does likewise. Both rest on the same estimate ContinuousLinearMap.norm_sub_apply_le_of_norm_le, which moves the point at which a difference of two uniformly bounded operators is evaluated to a nearby point of the dense subset.

theorem ContinuousLinearMap.norm_sub_apply_le_of_norm_le {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {T S : X →L[𝕜] Y} {K : ℝ} (hT : ‖T‖ ≤ K) (hS : ‖S‖ ≤ K) (x y : X) : ‖T x - S x‖ ≤ ‖T y - S y‖ + 2 * K * ‖x - y‖

Comparing two continuous linear maps of norm at most K at x costs at most 2 K ‖x - y‖ more than comparing them at y. This is the shared estimate of the two density arguments below: y is chosen in the dense subset, close to the arbitrary vector x.

theorem ContinuousLinearMap.tendsto_apply_of_dense {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {ι : Type u_4} {l : Filter ι} {D : Set X} (hD : Dense D) {f : ι → X →L[𝕜] Y} {g : X →L[𝕜] Y} {C : ℝ} (hbound : ∀ᶠ (i : ι) in l, ‖f i‖ ≤ C) (htendsto : ∀ x ∈ D, Filter.Tendsto (fun (i : ι) => (f i) x) l (nhds (g x))) (x : X) : Filter.Tendsto (fun (i : ι) => (f i) x) l (nhds (g x))

A uniformly bounded family of continuous linear maps that converges pointwise on a dense subset converges pointwise everywhere.

theorem ContinuousLinearMap.uniformCauchySeqOn_apply_of_dense {𝕜 : Type u_1} {X : Type u_2} {Y : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup X] [NormedSpace 𝕜 X] [NormedAddCommGroup Y] [NormedSpace 𝕜 Y] {ι : Type u_4} {Z : Type u_5} {p : Filter ι} {D : Set X} (hD : Dense D) {f : ι → Z → X →L[𝕜] Y} {s : Set Z} {C : ℝ} (hbound : ∀ᶠ (i : ι) in p, ∀ z ∈ s, ‖f i z‖ ≤ C) (hcauchy : ∀ x ∈ D, UniformCauchySeqOn (fun (i : ι) (z : Z) => (f i z) x) p s) (x : X) : UniformCauchySeqOn (fun (i : ι) (z : Z) => (f i z) x) p s

A uniformly bounded family of continuous linear maps that is uniformly Cauchy on a parameter set at every vector in a dense subset is uniformly Cauchy there at every vector.