22.4. Continuous linear maps🔗

If E and F are two topological vector spaces:

variable (𝕜 E F : Type*) [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
  [ContinuousAdd F] [ContinuousSMul 𝕜 F]

we can speak of the continuous linear maps between E and F. The relevant definition is ContinuousLinearMap and it has special notation as follows:

E →L[𝕜] F : Type (max u_2 u_3)#check E →L[𝕜] F

22.4.1. Topologies on continuous linear maps🔗

The space of continuous linear maps is naturally equipped with topology of bounded convergence. This topology coincides with the operator norm topology in case linear maps on Banach spaces.

variable (𝕜 E F : Type*) [NontriviallyNormedField 𝕜]
  [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  [NormedAddCommGroup F] [NormedSpace 𝕜 F]
  (f : E →L[𝕜] F)

example (x : E) : ‖f x‖ ≤ ‖f‖ * ‖x‖ := f.le_opNorm x

example {M : ℝ} (hMp : 0 ≤ M) (hM : ∀ x, ‖f x‖ ≤ M * ‖x‖) :
    ‖f‖ ≤ M := f.opNorm_le_bound hMp hM

Mathlib also knows about the following topologies on type synonyms of continuous linear maps:

Pointwise convergence (or strong operator topology): PointwiseConvergenceCLM
Compact convergence: CompactConvergenceCLM
Weak operator topology: ContinuousLinearMapWOT

22.4.2. Topological dual🔗

In the special case that F is the base field 𝕜, we have the abbreviation StrongDual 𝕜 E for the E →L[𝕜] 𝕜. This space naturally carries the topology of bounded convergence, which is also known as the strong topology. To obtain the weak dual use WeakDual.