22.2. Locally convex spaces🔗

Locally convex topological vector spaces (LCTVS) come in different forms. Mathlib distinguishes between the topological notion and spaces whose topology is induced by a family of seminorms, and the later one comes in two different forms. Hence, we have the options

LocallyConvexSpace
WithSeminorms
PolynormableSpace

Mathlib contains an extensive theory of all of these different notions. We will now describe how and when to use which notion.

The first option, LocallyConvexSpace, is the topological characterization that the convex neighborhoods of a point form a neighborhood basis of that point and this can be combined with the above characterization of TVS to spell a CLTVS over ℝ or ℂ as follows:

variable (E 𝕜 : Type*) [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E]
  [LocallyConvexSpace ℝ E]

This spelling is useful for proving topological properties about LCTVS.

The more analytical characterization of LCTVS is that the topology is induced by a family of seminorms and there is the predicate WithSeminorms that states that a given topology is induced by a family of seminorms:

variable {ι : Type*} (E 𝕜 : Type*) [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E]
  [ContinuousAdd E] [ContinuousSMul 𝕜 E]
  {p : SeminormFamily 𝕜 E ι} (hp : WithSeminorms p)

and Mathlib knows that in this case the space is locally convex:

example
    [NormedSpace ℝ 𝕜] [Module ℝ E] [IsScalarTower ℝ 𝕜 E] :
    LocallyConvexSpace ℝ E := hp.toLocallyConvexSpace

and conversely the gaugeSeminormFamily induces the topology on a locally convex space:

open scoped ComplexOrder
variable {E 𝕜 : Type*} [RCLike 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E]
  [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [Module ℝ E] [IsScalarTower ℝ 𝕜 E] [ContinuousSMul ℝ E]
  [LocallyConvexSpace 𝕜 E]
example : WithSeminorms (gaugeSeminormFamily 𝕜 E) :=
  with_gaugeSeminormFamily

The spelling WithSeminorms is used in the case where the family of seminorms explicitly appears in the statement or the hypothesis, for example WithSeminorms.tendsto_nhds_atTop.

Finally, there is PolynormableSpace, which states that the family of continuous seminorms induce the topology.

variable {E 𝕜 : Type*} [NormedField 𝕜]
  [AddCommGroup E] [Module 𝕜 E]
  [TopologicalSpace E] [PolynormableSpace 𝕜 E]

This characterization of LCTVS is valid for coefficients more general than ℝ or ℂ and coincides with LocallyConvexSpace if the base field is ℝ or ℂ.

open scoped ComplexOrder

variable (E 𝕜 : Type*) [RCLike 𝕜]
  [AddCommGroup E] [TopologicalSpace E]
  [IsTopologicalAddGroup E]
  [Module 𝕜 E] [ContinuousSMul 𝕜 E]
  [Module ℝ E] [ContinuousSMul ℝ E]
  [IsScalarTower ℝ 𝕜 E]

example [LocallyConvexSpace 𝕜 E] :
    PolynormableSpace 𝕜 E := byE✝:Type u_1𝕜✝:Type u_2inst✝¹⁴:NormedField 𝕜✝inst✝¹³:AddCommGroup E✝inst✝¹²:Module 𝕜✝ E✝inst✝¹¹:TopologicalSpace E✝inst✝¹⁰:PolynormableSpace 𝕜✝ E✝E:Type u_3𝕜:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:AddCommGroup Einst✝⁷:TopologicalSpace Einst✝⁶:IsTopologicalAddGroup Einst✝⁵:Module 𝕜 Einst✝⁴:ContinuousSMul 𝕜 Einst✝³:Module ℝ Einst✝²:ContinuousSMul ℝ Einst✝¹:IsScalarTower ℝ 𝕜 Einst✝:LocallyConvexSpace 𝕜 E⊢ PolynormableSpace 𝕜 E
  infer_instanceAll goals completed! 🐙

example [PolynormableSpace ℝ E] :
    LocallyConvexSpace ℝ E := byE✝:Type u_1𝕜✝:Type u_2inst✝¹⁴:NormedField 𝕜✝inst✝¹³:AddCommGroup E✝inst✝¹²:Module 𝕜✝ E✝inst✝¹¹:TopologicalSpace E✝inst✝¹⁰:PolynormableSpace 𝕜✝ E✝E:Type u_3𝕜:Type u_4inst✝⁹:RCLike 𝕜inst✝⁸:AddCommGroup Einst✝⁷:TopologicalSpace Einst✝⁶:IsTopologicalAddGroup Einst✝⁵:Module 𝕜 Einst✝⁴:ContinuousSMul 𝕜 Einst✝³:Module ℝ Einst✝²:ContinuousSMul ℝ Einst✝¹:IsScalarTower ℝ 𝕜 Einst✝:PolynormableSpace ℝ E⊢ LocallyConvexSpace ℝ E
  infer_instanceAll goals completed! 🐙

Using PolynormableSpace is preferred over WithSeminorms when the family of seminorms does not explicitly appear in either the hypothesis or the conclusion, for instance for statements about derivatives of Fréchet-valued functions.

22.2.1. Notable results🔗

The Hahn-Banach theorem: StrongDual.exists_extension
The Banach-Steinhaus theorem: WithSeminorms.banach_steinhaus and PolynormableSpace.banach_steinhaus