Basic facts about bounded operators

This file records a shared uniform-bound lemma for continuous linear maps. It lets an evaluation T i (g i) pass to the limit when the operators T i are eventually uniformly bounded, their values at the limiting argument converge, and the arguments g i converge. In particular, it supplies the common continuity step for StronglyContinuousSemigroup.tendsto_realOperator_apply and StronglyContinuousGroup.tendsto_apply.

theorem ContinuousLinearMap.tendsto_apply_of_eventually_norm_le {𝕜 : 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 ι} {T : ι → X →L[𝕜] Y} {C : ℝ} {g : ι → X} {z : X} {w : Y} (hT : ∀ᶠ (i : ι) in l, ‖T i‖ ≤ C) (hz : Filter.Tendsto (fun (i : ι) => (T i) z) l (nhds w)) (hg : Filter.Tendsto g l (nhds z)) : Filter.Tendsto (fun (i : ι) => (T i) (g i)) l (nhds w)

If T i is eventually uniformly bounded, T i z tends to w, and g i tends to z, then the moving evaluations T i (g i) tend to w.