feat: introduce an IsNormableSpace class

Mathlib/Analysis/LocallyConvex/WithSeminorms.lean

@@ -24,6 +24,8 @@ public import Mathlib.Topology.Algebra.Module.LocallyConvex
   bounded by a finite number of seminorms in `E`.
 * `WithSeminorms p`, when `p` is a family of seminorms on `E`, is a proposition expressing that the
   (existing) topology on `E` is induced by the seminorms `p`.
+* `NormableSpace 𝕜 E` is a class asserting that the (existing) topology on `E` is induced
+  by *some* `𝕜`-seminorm
 * `PolynormableSpace 𝕜 E` is a class asserting that the (existing) topology on `E` is induced
   by *some* family of `𝕜`-seminorms. If `𝕜` is `RCLike`, this is equivalent to
   `LocallyConvexSpace 𝕜 E`.
@@ -284,6 +286,18 @@ variable [NormedField 𝕜] [AddCommGroup E] [Module 𝕜 E]
 structure WithSeminorms (p : SeminormFamily 𝕜 E ι) [topology : TopologicalSpace E] : Prop where
   topology_eq_withSeminorms : topology = p.moduleFilterBasis.topology
 
+variable (𝕜 E) in
+/-- A topological vector space `E` is **normable** over `𝕜` if its topology is induced by
+*some* `𝕜`-seminorm.
+To endow such a space with a normed space structure with the same topology, use:
+```
+  let : SeminormedAddCommGroup E := NormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := NormableSpace.toNormedSpace 𝕜 E
+```
+-/
+class NormableSpace [topology : TopologicalSpace E] where
+  withSeminorms' : ∃ (p : Seminorm 𝕜 E), WithSeminorms (fun (_ : Fin 1) ↦ p)
+
 variable (𝕜 E) in
 /-- A topological vector space `E` is **polynormable** over `𝕜` if its topology is induced by
 *some* family of `𝕜`-seminorms. Equivalently, its topology is induced by *all* its continuous
@@ -313,6 +327,9 @@ theorem WithSeminorms.continuousSMul (hp : WithSeminorms p) : ContinuousSMul 
   rw [hp.withSeminorms_eq]
   exact ModuleFilterBasis.continuousSMul _
 
+instance [h : PolynormableSpace 𝕜 E] : ContinuousSMul 𝕜 E :=
+  h.withSeminorms'.continuousSMul
+
 theorem WithSeminorms.hasBasis (hp : WithSeminorms p) :
     (𝓝 (0 : E)).HasBasis (fun s : Set E => s ∈ p.basisSets) id := by
   rw [congr_fun (congr_arg (@nhds E) hp.1) 0]
@@ -474,6 +491,10 @@ theorem WithSeminorms.toPolynormableSpace {p : SeminormFamily 𝕜 E ι} (hp : W
       intro i
       exact iInf_le (ι := {p : Seminorm 𝕜 E // Continuous p}) _ ⟨p i, hp' i⟩
 
+instance [h : NormableSpace 𝕜 E] : PolynormableSpace 𝕜 E := by
+  rcases h.withSeminorms' with ⟨q, hq⟩
+  exact hq.toPolynormableSpace
+
 end TopologicalSpace
 
 /-- The uniform structure induced by a family of seminorms is exactly the infimum of the ones
@@ -498,10 +519,54 @@ theorem norm_withSeminorms (𝕜 E) [NormedField 𝕜] [SeminormedAddCommGroup E
   rw [SeminormFamily.withSeminorms_iff_nhds_eq_iInf, iInf_const, coe_normSeminorm,
     comap_norm_nhds_zero]
 
-/-- A (semi-)normed space is polynormable. -/
-instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] :
-    PolynormableSpace 𝕜 E :=
-  norm_withSeminorms 𝕜 E |>.toPolynormableSpace
+/-- A (semi-)normed space is normable. -/
+instance [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : NormableSpace 𝕜 E :=
+  ⟨⟨normSeminorm 𝕜 E, norm_withSeminorms 𝕜 E⟩⟩
+
+variable [NormedField 𝕜] [ha : AddCommGroup E] [hm : Module 𝕜 E]
+  [t : TopologicalSpace E] [hn : NormableSpace 𝕜 E]
+
+variable (𝕜 E)
+
+/-- A seminorm defining the topology in a normable space. -/
+noncomputable def NormableSpace.seminorm : Seminorm 𝕜 E := hn.withSeminorms'.choose
+
+/-- A normable space can be endowed with a seminorm defining the same topology. -/
+noncomputable abbrev NormableSpace.toSeminormedAddCommGroup : SeminormedAddCommGroup E := by
+  let q := NormableSpace.seminorm 𝕜 E
+  have hq := hn.withSeminorms'.choose_spec
+  have : IsTopologicalAddGroup E := hq.topologicalAddGroup
+  let : Norm E := ⟨NormableSpace.seminorm 𝕜 E⟩
+  let c : SeminormedSpace.Core 𝕜 E :=
+  { norm_nonneg x := apply_nonneg q x
+    norm_smul c x := map_smul_eq_mul q c x
+    norm_triangle x y := map_add_le_add q x y }
+  refine SeminormedAddCommGroup.ofCoreReplaceTopology c ?_
+  rw [(SeminormFamily.withSeminorms_iff_topologicalSpace_eq_iInf _).1 hq, ciInf_unique]
+  rfl
+
+/-- A normable space can be endowed with a normed space structure. -/
+noncomputable abbrev NormableSpace.toNormedSpace :
+    letI : SeminormedAddCommGroup E := NormableSpace.toSeminormedAddCommGroup 𝕜 E
+    NormedSpace 𝕜 E :=
+  letI : SeminormedAddCommGroup E := NormableSpace.toSeminormedAddCommGroup 𝕜 E
+  { norm_smul_le c x := (map_smul_eq_mul (NormableSpace.seminorm 𝕜 E) c x).le }
+
+instance [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F] [NormableSpace 𝕜 F] :
+    NormableSpace 𝕜 (E × F) := by
+  let : SeminormedAddCommGroup E := NormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := NormableSpace.toNormedSpace 𝕜 E
+  let : SeminormedAddCommGroup F := NormableSpace.toSeminormedAddCommGroup 𝕜 F
+  let : NormedSpace 𝕜 F := NormableSpace.toNormedSpace 𝕜 F
+  infer_instance
+
+instance {E : ι → Type*} [Finite ι] [∀ i, AddCommGroup (E i)] [∀ i, Module 𝕜 (E i)]
+    [∀ i, TopologicalSpace (E i)] [∀ i, NormableSpace 𝕜 (E i)] :
+    NormableSpace 𝕜 (Π i, E i) := by
+  let A i : SeminormedAddCommGroup (E i) := NormableSpace.toSeminormedAddCommGroup 𝕜 (E i)
+  let B i : NormedSpace 𝕜 (E i) := NormableSpace.toNormedSpace 𝕜 (E i)
+  let : Fintype ι := Fintype.ofFinite ι
+  infer_instance
 
 end NormedSpace
 

Mathlib/Analysis/Normed/Module/Dual.lean

@@ -59,7 +59,7 @@ theorem polar_closure (s : Set E) : StrongDual.polar 𝕜 (closure s) = StrongDu
     (topDualPairing 𝕜 E).flip.polar_gc.l_le <|
       closure_minimal ((topDualPairing 𝕜 E).flip.polar_gc.le_u_l s) <| by
         simpa [LinearMap.flip_flip] using!
-          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E := E)).continuous
+          (isClosed_polar _ _).preimage (ContinuousLinearMap.apply 𝕜 𝕜 (E' := E)).continuous
 
 variable {𝕜}
 

Mathlib/Analysis/Normed/Operator/Basic.lean

@@ -389,6 +389,16 @@ instance toNormedSpace {𝕜' : Type*} [NormedField 𝕜'] [NormedSpace 𝕜' F]
     NormedSpace 𝕜' (E →SL[σ₁₂] F) :=
   ⟨opNorm_smul_le⟩
 
+instance {E F : Type*} [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [NormableSpace 𝕜 E]
+    [AddCommGroup F] [Module 𝕜₂ F] [TopologicalSpace F] [IsTopologicalAddGroup F]
+    [NormableSpace 𝕜₂ F] :
+    NormableSpace 𝕜₂ (E →SL[σ₁₂] F) := by
+  let : SeminormedAddCommGroup E := NormableSpace.toSeminormedAddCommGroup 𝕜 E
+  let : NormedSpace 𝕜 E := NormableSpace.toNormedSpace 𝕜 E
+  let : SeminormedAddCommGroup F := NormableSpace.toSeminormedAddCommGroup 𝕜₂ F
+  let : NormedSpace 𝕜₂ F := NormableSpace.toNormedSpace 𝕜₂ F
+  infer_instance
+
 /-- The operator norm is submultiplicative. -/
 theorem opNorm_comp_le (f : E →SL[σ₁₂] F) : ‖h.comp f‖ ≤ ‖h‖ * ‖f‖ :=
   csInf_le bounds_bddBelow ⟨by positivity, fun x => by