feat(analysis/normed_space/dual): generalize to seminormed space (#7262)

We generalize here the Hahn-Banach theorem and the notion of dual space to `semi_normed_space`.

src/analysis/normed_space/dual.lean

@@ -27,6 +27,9 @@ of a Hilbert space `E` has the form `λ u, ⟪x, u⟫` for some `x : E`.  This p
 `to_dual_map` to be upgraded to an (isometric) continuous linear equivalence, `to_dual`, between a
 Hilbert space and its dual.
 
+Since a lot of elementary properties don't require `eq_of_dist_eq_zero` we start setting up the
+theory for `semi_normed_space` and we specialize to `normed_space` when needed.
+
 ## References
 
 * [M. Einsiedler and T. Ward, *Functional Analysis, Spectral Theory, and Applications*]
@@ -45,13 +48,18 @@ namespace normed_space
 
 section general
 variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
-variables (E : Type*) [normed_group E] [normed_space 𝕜 E]
+variables (E : Type*) [semi_normed_group E] [semi_normed_space 𝕜 E]
+variables (F : Type*) [normed_group F] [normed_space 𝕜 F]
 
-/-- The topological dual of a normed space `E`. -/
-@[derive [has_coe_to_fun, normed_group, normed_space 𝕜]] def dual := E →L[𝕜] 𝕜
+/-- The topological dual of a seminormed space `E`. -/
+@[derive [has_coe_to_fun, semi_normed_group, semi_normed_space 𝕜]] def dual := E →L[𝕜] 𝕜
 
 instance : inhabited (dual 𝕜 E) := ⟨0⟩
 
+instance : normed_group (dual 𝕜 F) := continuous_linear_map.to_normed_group
+
+instance : normed_space 𝕜 (dual 𝕜 F) := continuous_linear_map.to_normed_space
+
 /-- The inclusion of a normed space in its double (topological) dual. -/
 def inclusion_in_double_dual' (x : E) : (dual 𝕜 (dual 𝕜 E)) :=
 linear_map.mk_continuous

src/analysis/normed_space/hahn_banach.lean

@@ -31,22 +31,22 @@ state equalities of the form `g x = norm' 𝕜 x` when `g` is a linear function.
 
 For the concrete cases of `ℝ` and `ℂ`, this is just `∥x∥` and `↑∥x∥`, respectively.
 -/
-noncomputable def norm' (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
-  {E : Type*} [normed_group E] (x : E) : 𝕜 :=
+noncomputable def norm' (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜]
+  {E : Type*} [semi_normed_group E] (x : E) : 𝕜 :=
 algebra_map ℝ 𝕜 ∥x∥
 
-lemma norm'_def (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
-  {E : Type*} [normed_group E] (x : E) :
+lemma norm'_def (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜]
+  {E : Type*} [semi_normed_group E] (x : E) :
   norm' 𝕜 x = (algebra_map ℝ 𝕜 ∥x∥) := rfl
 
 lemma norm_norm'
-  (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
-  (A : Type*) [normed_group A]
+  (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [semi_normed_algebra ℝ 𝕜]
+  (A : Type*) [semi_normed_group A]
   (x : A) : ∥norm' 𝕜 x∥ = ∥x∥ :=
 by rw [norm'_def, norm_algebra_map_eq, norm_norm]
 
 namespace real
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
+variables {E : Type*} [semi_normed_group E] [semi_normed_space ℝ E]
 
 /-- Hahn-Banach theorem for continuous linear functions over `ℝ`. -/
 theorem exists_extension_norm_eq (p : subspace ℝ E) (f : p →L[ℝ] ℝ) :
@@ -73,15 +73,15 @@ end real
 section is_R_or_C
 open is_R_or_C
 
-variables {𝕜 : Type*} [is_R_or_C 𝕜] {F : Type*} [normed_group F] [normed_space 𝕜 F]
+variables {𝕜 : Type*} [is_R_or_C 𝕜] {F : Type*} [semi_normed_group F] [semi_normed_space 𝕜 F]
 
 /-- Hahn-Banach theorem for continuous linear functions over `𝕜` satisyfing `is_R_or_C 𝕜`. -/
 theorem exists_extension_norm_eq (p : subspace 𝕜 F) (f : p →L[𝕜] 𝕜) :
   ∃ g : F →L[𝕜] 𝕜, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥ :=
 begin
   letI : module ℝ F := restrict_scalars.semimodule ℝ 𝕜 F,
   letI : is_scalar_tower ℝ 𝕜 F := restrict_scalars.is_scalar_tower _ _ _,
-  letI : normed_space ℝ F := normed_space.restrict_scalars _ 𝕜 _,
+  letI : semi_normed_space ℝ F := semi_normed_space.restrict_scalars _ 𝕜 _,
   -- Let `fr: p →L[ℝ] ℝ` be the real part of `f`.
   let fr := re_clm.comp (f.restrict_scalars ℝ),
   have fr_apply : ∀ x, fr x = re (f x), by { assume x, refl },