Topology of pointwise convergence on continous linear maps

Main definitions

• PointwiseConvergenceCLM: Type synonym of E →SL[σ] F equipped with the uniform convergence topology on finite sets.
• PointwiseConvergenceCLM.evalCLM: The evaluation map (f : E →SLₚₜ[σ] F) ↦ f a for fixed a : E as a continuous linear map.
• ContinousLinearMap.toPointwiseConvergenceCLM: The canonical map from E →SL[σ] F to E →SLₚₜ[σ] F as a continuous linear map. This is the statement that bounded convergence is stronger than pointwise convergence.
• PointwiseConvergenceCLM.equivWeakDual: The continuous equivalence between E →Lₚₜ[𝕜] 𝕜 and WeakDual 𝕜 E.

Main statements

• PointwiseConvergenceCLM.tendsto_iff_forall_tendsto: In the topology of pointwise convergence, a converges to a₀ iff for every x : E the map a · x converges to a₀ x.
• PointwiseConvergenceCLM.continuous_of_continuous_eval: A map to g : α → E →SLₚₜ[σ] F is continuous if for every x : E the evaluation g · x is continuous.

Notation

• E →SLₚₜ[σ] F is space of continuous linear maps equipped with pointwise convergence topology.

Topology of pointwise convergence

@[reducible, inline]

abbrev PointwiseConvergenceCLM {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [Module 𝕜₁ E] [Module 𝕜₂ F] : Type (max u_6 u_7)

The space of continuous linear maps equipped with the topology of pointwise convergence, sometimes also called the strong operator topology. We avoid this terminology since so many other things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak*-topology in the case that σ = RingHom.id 𝕜 and F = 𝕜

Equations

• (E →SLₚₜ[σ] F) = UniformConvergenceCLM σ F {s : Set E | Finite ↑s}

def «term_→SLₚₜ[_]_» : Lean.TrailingParserDescr

The space of continuous linear maps equipped with the topology of pointwise convergence, sometimes also called the strong operator topology. We avoid this terminology since so many other things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak*-topology in the case that σ = RingHom.id 𝕜 and F = 𝕜

Equations

• One or more equations did not get rendered due to their size.

def «term_→Lₚₜ[_]_» : Lean.TrailingParserDescr

The space of continuous linear maps equipped with the topology of pointwise convergence, sometimes also called the strong operator topology. We avoid this terminology since so many other things share similar names, and using "pointwise convergence" in the name is more informative.

This topology is also known as the weak*-topology in the case that σ = RingHom.id 𝕜 and F = 𝕜

Equations

• One or more equations did not get rendered due to their size.

instance PointwiseConvergenceCLM.instT2Space {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [T2Space F] : T2Space (E →SLₚₜ[σ] F)

instance PointwiseConvergenceCLM.continuousEvalConst {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] : ContinuousEvalConst (E →SLₚₜ[σ] F) E F

theorem PointwiseConvergenceCLM.hasBasis_nhds_zero_of_basis {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] {ι : Type u_9} {p : ι → Prop} {b : ι → Set F} (h : (nhds 0).HasBasis p b) : (nhds 0).HasBasis (fun (Si : Set E × ι) => Finite ↑Si.1 ∧ p Si.2) fun (Si : Set E × ι) => {f : E →SLₚₜ[σ] F | ∀ x ∈ Si.1, f x ∈ b Si.2}

theorem PointwiseConvergenceCLM.hasBasis_nhds_zero {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] : (nhds 0).HasBasis (fun (SV : Set E × Set F) => Finite ↑SV.1 ∧ SV.2 ∈ nhds 0) fun (SV : Set E × Set F) => {f : E →SLₚₜ[σ] F | ∀ x ∈ SV.1, f x ∈ SV.2}

theorem PointwiseConvergenceCLM.isUniformEmbedding_coeFn {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (Fᵤ : Type u_8) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup Fᵤ] [UniformSpace Fᵤ] [IsUniformAddGroup Fᵤ] [Module 𝕜₁ E] [Module 𝕜₂ Fᵤ] : IsUniformEmbedding DFunLike.coe

theorem PointwiseConvergenceCLM.isEmbedding_coeFn {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] : Topology.IsEmbedding DFunLike.coe

theorem PointwiseConvergenceCLM.tendsto_iff_forall_tendsto {ι : Type u_2} {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] {p : Filter ι} {a : ι → E →SLₚₜ[σ] F} {a₀ : E →SLₚₜ[σ] F} : Filter.Tendsto a p (nhds a₀) ↔ ∀ (x : E), Filter.Tendsto (fun (x_1 : ι) => (a x_1) x) p (nhds (a₀ x))

In the topology of pointwise convergence, a converges to a₀ iff for every x : E the map a · x converges to a₀ x.

def PointwiseConvergenceCLM.coeLMₛₗ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] : (E →SLₚₜ[σ] F) →ₗ[𝕜₂] E →ₛₗ[σ] F

Coercion from E →SLₚₜ[σ] F to E →ₛₗ[σ] F as a 𝕜₂-linear map.

Equations

• PointwiseConvergenceCLM.coeLMₛₗ σ E F = ContinuousLinearMap.coeLMₛₗ σ

@[simp]

theorem PointwiseConvergenceCLM.coeLMₛₗ_apply {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] (self : E →SL[σ] F) : (coeLMₛₗ σ E F) self = ↑self

def PointwiseConvergenceCLM.coeLM (𝕜 : Type u_3) [NormedField 𝕜] (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 E] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] : (E →Lₚₜ[𝕜] F) →ₗ[𝕜] E →ₗ[𝕜] F

Coercion from E →Lₚₜ[𝕜] F to E →ₗ[𝕜] F as a 𝕜-linear map.

Equations

• PointwiseConvergenceCLM.coeLM 𝕜 E F = ContinuousLinearMap.coeLM 𝕜

@[simp]

theorem PointwiseConvergenceCLM.coeLM_apply (𝕜 : Type u_3) [NormedField 𝕜] (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜 E] [Module 𝕜 F] [ContinuousConstSMul 𝕜 F] (self : E →L[𝕜] F) : (coeLM 𝕜 E F) self = ↑self

def PointwiseConvergenceCLM.evalCLM {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_6} (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] (a : E) : (E →SLₚₜ[σ] F) →L[𝕜₂] F

The evaluation map (f : E →SLₚₜ[σ] F) ↦ f a for a : E as a continuous linear map.

Equations

• PointwiseConvergenceCLM.evalCLM σ F a = { toLinearMap := (PointwiseConvergenceCLM.coeLMₛₗ σ E F).flip a, cont := ⋯ }

@[simp]

theorem PointwiseConvergenceCLM.evalCLM_apply {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_6} (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousConstSMul 𝕜₂ F] (a : E) (m : E →SLₚₜ[σ] F) : (evalCLM σ F a) m = m a

theorem PointwiseConvergenceCLM.continuous_of_continuous_eval {α : Type u_1} [TopologicalSpace α] {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [NormedField 𝕜₁] [NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_6} {F : Type u_7} [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] {g : α → E →SLₚₜ[σ] F} (h : ∀ (x : E), Continuous fun (x_1 : α) => (g x_1) x) : Continuous g

A map to E →SLₚₜ[σ] F is continuous if for every x : E the evaluation g · x is continuous.

def ContinuousLinearMap.toPointwiseConvergenceCLM {𝕜₁ : Type u_4} (𝕜₂ : Type u_5) [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousSMul 𝕜₁ E] [ContinuousConstSMul 𝕜₂ F] : (E →SL[σ] F) →L[𝕜₂] E →SLₚₜ[σ] F

The topology of bounded convergence is stronger than the topology of pointwise convergence.

Equations

• ContinuousLinearMap.toPointwiseConvergenceCLM 𝕜₂ σ E F = { toLinearMap := LinearMap.id, cont := ⋯ }

@[simp]

theorem ContinuousLinearMap.toPointwiseConvergenceCLM_apply {𝕜₁ : Type u_4} (𝕜₂ : Type u_5) [NormedField 𝕜₁] [NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_6) (F : Type u_7) [AddCommGroup E] [TopologicalSpace E] [AddCommGroup F] [TopologicalSpace F] [IsTopologicalAddGroup F] [Module 𝕜₁ E] [Module 𝕜₂ F] [ContinuousSMul 𝕜₁ E] [ContinuousConstSMul 𝕜₂ F] (a : E →SL[σ] F) : (toPointwiseConvergenceCLM 𝕜₂ σ E F) a = a

def PointwiseConvergenceCLM.equivWeakDual (𝕜 : Type u_3) [NormedField 𝕜] (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] : (E →Lₚₜ[𝕜] 𝕜) ≃L[𝕜] WeakDual 𝕜 E

The topology of pointwise convergence on E →Lₚₜ[𝕜] 𝕜 coincides with the weak-* topology.

Equations

• PointwiseConvergenceCLM.equivWeakDual 𝕜 E = { toLinearEquiv := LinearEquiv.refl 𝕜 (E →L[𝕜] 𝕜), continuous_toFun := ⋯, continuous_invFun := ⋯ }

@[simp]

theorem PointwiseConvergenceCLM.equivWeakDual_apply (𝕜 : Type u_3) [NormedField 𝕜] (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] (a : E →L[𝕜] 𝕜) : (equivWeakDual 𝕜 E) a = a

@[simp]

theorem PointwiseConvergenceCLM.equivWeakDual_symm_apply (𝕜 : Type u_3) [NormedField 𝕜] (E : Type u_6) [AddCommGroup E] [TopologicalSpace E] [Module 𝕜 E] (a✝ : E →L[𝕜] 𝕜) : (equivWeakDual 𝕜 E).symm a✝ = a✝