The topology of pointwise convergence is locally convex

We prove that the topology of pointwise convergence is induced by a family of seminorms and that it is locally convex in the topological sense

• PointwiseConvergenceCLM.seminorm: the seminorms on E →SLₚₜ[σ] F given by A ↦ ‖A x‖ for fixed x : E.
• PointwiseConvergenceCLM.withSeminorm: the topology is induced by the seminorms.
• PointwiseConvergenceCLM.instLocallyConvexSpace: E →SLₚₜ[σ] F is locally convex.

def PointwiseConvergenceCLM.seminorm {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] (x : E) : Seminorm 𝕜₂ (E →SLₚₜ[σ] F)

The family of seminorms that induce the topology of pointwise convergence, namely ‖A x‖ for all x : E.

@[reducible, inline]

abbrev PointwiseConvergenceCLM.seminormFamily {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7) (F : Type u_8) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : SeminormFamily 𝕜₂ (E →SLₚₜ[σ] F) E

The family of seminorms that induce the topology of pointwise convergence, namely ‖A x‖ for all x : E.

def PointwiseConvergenceCLM.inducingFn {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7) (F : Type u_8) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : (E →SLₚₜ[σ] F) →ₗ[𝕜₂] E → F

The coercion E →SLₚₜ[σ] F to E → F as a linear map.

The topology on E →SLₚₜ[σ] F is induced by this map.

theorem PointwiseConvergenceCLM.isInducing_inducingFn {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7) (F : Type u_8) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : Topology.IsInducing ⇑(inducingFn σ E F)

theorem PointwiseConvergenceCLM.withSeminorms {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] : WithSeminorms (PointwiseConvergenceCLM.seminormFamily σ E F)

theorem PointwiseConvergenceCLM.tendsto_nhds {α : Type u_1} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] {f : Filter α} (u : α → E →SLₚₜ[σ] F) (y₀ : E →SLₚₜ[σ] F) : Filter.Tendsto u f (nhds y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∀ᶠ (k : α) in f, ‖(u k) x - y₀ x‖ < ε

theorem PointwiseConvergenceCLM.tendsto_nhds_atTop {α : Type u_1} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [SemilatticeSup α] [Nonempty α] (u : α → E →SLₚₜ[σ] F) (y₀ : E →SLₚₜ[σ] F) : Filter.Tendsto u Filter.atTop (nhds y₀) ↔ ∀ (x : E) (ε : ℝ), 0 < ε → ∃ (k₀ : α), ∀ (k : α), k₀ ≤ k → ‖(u k) x - y₀ x‖ < ε

def PointwiseConvergenceCLM.mkCLM {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} {𝕜₃ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] [NormedField 𝕜₃] {σ : 𝕜₁ →+* 𝕜₂} {τ : 𝕜₃ →+* 𝕜₂} {D : Type u_6} {E : Type u_7} (F : Type u_8) (G : Type u_9) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [NormedAddCommGroup F] [NormedSpace 𝕜₂ F] [AddCommGroup D] [TopologicalSpace D] [Module 𝕜₃ D] [NormedAddCommGroup G] [NormedSpace 𝕜₂ G] (A : (E →SL[σ] F) →ₗ[𝕜₂] D →SL[τ] G) (hbound : ∀ (f : D), ∃ (s : Finset E) (C : NNReal), ∀ (B : E →SL[σ] F), ∃ (g : E) (_ : g ∈ s), ‖(A B) f‖ ≤ C • ‖B g‖) : (E →SLₚₜ[σ] F) →L[𝕜₂] D →SLₚₜ[τ] G

Define a continuous linear map between E →SLₚₜ[σ] F and D →SLₚₜ[τ] G.

Use PointwiseConvergenceCLM.precomp for the special case of the adjoint operator.

instance PointwiseConvergenceCLM.instLocallyConvexSpace {R : Type u_2} {𝕜₁ : Type u_3} {𝕜₂ : Type u_4} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_7} {F : Type u_8} [AddCommGroup E] [TopologicalSpace E] [Module 𝕜₁ E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₂ F] [Semiring R] [PartialOrder R] [Module R F] [ContinuousConstSMul R F] [LocallyConvexSpace R F] [SMulCommClass 𝕜₂ R F] : LocallyConvexSpace R (E →SLₚₜ[σ] F)