feat(analysis/normed_space): generalize corollaries of Hahn-Banach (#3658)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

Author: Ruben-VandeVelde

src/analysis/normed_space/dual.lean

@@ -11,11 +11,13 @@ import analysis.normed_space.hahn_banach
 In this file we define the topological dual of a normed space, and the bounded linear map from
 a normed space into its double dual.
 
-We also prove that, for base field the real numbers, this map is an isometry.  (TODO:  the same for
-the complex numbers.)
+We also prove that, for base field such as the real or the complex numbers, this map is an isometry.
+More generically, this is proved for any field in the class `has_exists_extension_norm_eq`, i.e.,
+satisfying the Hahn-Banach theorem.
 -/
 
 noncomputable theory
+universes u v
 
 namespace normed_space
 
@@ -59,36 +61,38 @@ linear_map.mk_continuous
 
 end general
 
-section real
-variables (E : Type*) [normed_group E] [normed_space ℝ E]
+section bidual_isometry
+
+variables {𝕜 : Type v} [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
+[has_exists_extension_norm_eq.{u} 𝕜]
+{E : Type u} [normed_group E] [normed_space 𝕜 E]
 
 /-- If one controls the norm of every `f x`, then one controls the norm of `x`.
     Compare `continuous_linear_map.op_norm_le_bound`. -/
-lemma norm_le_dual_bound (x : E) {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ (f: dual ℝ E), ∥f x∥ ≤ M * ∥f∥) :
+lemma norm_le_dual_bound (x : E) {M : ℝ} (hMp: 0 ≤ M) (hM : ∀ (f : dual 𝕜 E), ∥f x∥ ≤ M * ∥f∥) :
   ∥x∥ ≤ M :=
 begin
   classical,
   by_cases h : x = 0,
   { simp only [h, hMp, norm_zero] },
-  { cases exists_dual_vector x h with f hf,
-    calc ∥x∥ = f x : hf.2.symm
-    ... ≤ ∥f x∥ : le_max_left (f x) (-f x)
+  { obtain ⟨f, hf⟩ : ∃ g : E →L[𝕜] 𝕜, _ := exists_dual_vector x h,
+    calc ∥x∥ = ∥norm' 𝕜 x∥ : (norm_norm' _ _ _).symm
+    ... = ∥f x∥ : by rw hf.2
     ... ≤ M * ∥f∥ : hM f
-    ... = M : by rw [ hf.1, mul_one ] }
+    ... = M : by rw [hf.1, mul_one] }
 end
 
 /-- The inclusion of a real normed space in its double dual is an isometry onto its image.-/
-lemma inclusion_in_double_dual_isometry (x : E) : ∥inclusion_in_double_dual ℝ E x∥ = ∥x∥ :=
+lemma inclusion_in_double_dual_isometry (x : E) : ∥inclusion_in_double_dual 𝕜 E x∥ = ∥x∥ :=
 begin
-  refine le_antisymm_iff.mpr ⟨double_dual_bound ℝ E x, _⟩,
-  rw continuous_linear_map.norm_def,
-  apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
-  intros c,
-  simpa using norm_le_dual_bound E x,
+  apply le_antisymm,
+  { exact double_dual_bound 𝕜 E x },
+  { rw continuous_linear_map.norm_def,
+    apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
+    rintros c ⟨hc1, hc2⟩,
+    exact norm_le_dual_bound x hc1 hc2 },
 end
 
--- TODO: This is also true over ℂ.
-
-end real
+end bidual_isometry
 
 end normed_space

src/analysis/normed_space/hahn_banach.lean

@@ -11,20 +11,58 @@ import analysis.convex.cone
 # Hahn-Banach theorem
 
 In this file we prove a version of Hahn-Banach theorem for continuous linear
-functions on normed spaces over ℝ and ℂ.
+functions on normed spaces over `ℝ` and `ℂ`.
 
-We also prove a standard corollary, needed for the isometric inclusion in the double dual.
+In order to state and prove its corollaries uniformly, we introduce a typeclass
+`has_exists_extension_norm_eq` for a field, requiring that a strong version of the
+Hahn-Banach theorem holds over this field, and provide instances for `ℝ` and `ℂ`.
 
-## TODO
+In this setting, `exists_dual_vector` states that, for any nonzero `x`, there exists a continuous
+linear form `g` of norm `1` with `g x = ∥x∥` (where the norm has to be interpreted as an element
+of `𝕜`).
 
-Prove more corollaries
+-/
+
+universes u v
+
+/--
+A field where the Hahn-Banach theorem for continuous linear functions holds. This allows stating
+theorems that depend on it uniformly over such fields.
 
+In particular, this is satisfied by `ℝ` and `ℂ`.
 -/
+class has_exists_extension_norm_eq (𝕜 : Type v) [nondiscrete_normed_field 𝕜] : Prop :=
+(exists_extension_norm_eq :
+  ∀ (E : Type u)
+  [normed_group E] [normed_space 𝕜 E]
+  (p : subspace 𝕜 E)
+  (f : p →L[𝕜] 𝕜),
+  ∃ g : E →L[𝕜] 𝕜, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥)
+
+/--
+The norm of `x` as an element of `𝕜` (a normed algebra over `ℝ`). This is needed in particular to
+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) : 𝕜 :=
+algebra_map ℝ 𝕜 ∥x∥
+
+lemma norm'_def (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
+  {E : Type*} [normed_group E] (x : E) :
+  norm' 𝕜 x = (algebra_map ℝ 𝕜 ∥x∥) := rfl
 
-section basic
+lemma norm_norm'
+  (𝕜 : Type*) [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
+  (A : Type*) [normed_group A]
+  (x : A) : ∥norm' 𝕜 x∥ = ∥x∥ :=
+by rw [norm'_def, norm_algebra_map_eq, norm_norm]
+
+section real
 variables {E : Type*} [normed_group E] [normed_space ℝ E]
 
-/-- Hahn-Banach theorem for continuous linear functions over ℝ. -/
+/-- Hahn-Banach theorem for continuous linear functions over `ℝ`. -/
 theorem exists_extension_norm_eq (p : subspace ℝ E) (f : p →L[ℝ] ℝ) :
   ∃ g : E →L[ℝ] ℝ, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥ :=
 begin
@@ -44,14 +82,17 @@ begin
     exact mul_le_mul_of_nonneg_left (norm_add_le x y) (norm_nonneg f) }
 end
 
-end basic
+instance real_has_exists_extension_norm_eq : has_exists_extension_norm_eq ℝ :=
+⟨by { intros, apply exists_extension_norm_eq }⟩
+
+end real
 
 section complex
 variables {F : Type*} [normed_group F] [normed_space ℂ F]
 
 -- Inlining the following two definitions causes a type mismatch between
 -- subspace ℝ (semimodule.restrict_scalars ℝ ℂ F) and subspace ℂ F.
-/-- Restrict a ℂ-subspace to an ℝ-subspace. -/
+/-- Restrict a `ℂ`-subspace to an `ℝ`-subspace. -/
 noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ ℂ F
 
 private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) :
@@ -60,7 +101,7 @@ private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) :
 
 open complex
 
-/-- Hahn-Banach theorem for continuous linear functions over ℂ. -/
+/-- Hahn-Banach theorem for continuous linear functions over `ℂ`. -/
 theorem complex.exists_extension_norm_eq (p : subspace ℂ F) (f : p →L[ℂ] ℂ) :
   ∃ g : F →L[ℂ] ℂ, (∀ x : p, g x = f x) ∧ ∥g∥ = ∥f∥ :=
 begin
@@ -95,48 +136,49 @@ begin
   { exact f.op_norm_le_bound g.extend_to_ℂ.op_norm_nonneg (λ x, h x ▸ g.extend_to_ℂ.le_op_norm x) },
 end
 
+instance complex_has_exists_extension_norm_eq : has_exists_extension_norm_eq ℂ :=
+⟨by { intros, apply complex.exists_extension_norm_eq }⟩
+
 end complex
 
 section dual_vector
-variables {E : Type*} [normed_group E] [normed_space ℝ E]
+variables {𝕜 : Type v} [nondiscrete_normed_field 𝕜] [normed_algebra ℝ 𝕜]
+variables {E : Type u} [normed_group E] [normed_space 𝕜 E]
 
 open continuous_linear_equiv
 open_locale classical
 
-lemma coord_self' (x : E) (h : x ≠ 0) : (∥x∥ • (coord ℝ x h))
-  ⟨x, submodule.mem_span_singleton_self x⟩ = ∥x∥ :=
-calc (∥x∥ • (coord ℝ x h)) ⟨x, submodule.mem_span_singleton_self x⟩
-    = ∥x∥ • (linear_equiv.coord ℝ E x h) ⟨x, submodule.mem_span_singleton_self x⟩ : rfl
-... = ∥x∥ • 1 : by rw linear_equiv.coord_self ℝ E x h
-... = ∥x∥ : mul_one _
+lemma coord_norm' (x : E) (h : x ≠ 0) : ∥norm' 𝕜 x • coord 𝕜 x h∥ = 1 :=
+by rw [norm_smul, norm_norm', coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
 
-lemma coord_norm' (x : E) (h : x ≠ 0) : ∥∥x∥ • coord ℝ x h∥ = 1 :=
-by rw [norm_smul, norm_norm, coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
+variables [has_exists_extension_norm_eq.{u} 𝕜]
+open submodule
 
 /-- Corollary of Hahn-Banach.  Given a nonzero element `x` of a normed space, there exists an
-    element of the dual space, of norm 1, whose value on `x` is `∥x∥`. -/
-theorem exists_dual_vector (x : E) (h : x ≠ 0) : ∃ g : E →L[ℝ] ℝ, ∥g∥ = 1 ∧ g x = ∥x∥ :=
+    element of the dual space, of norm `1`, whose value on `x` is `∥x∥`. -/
+theorem exists_dual_vector (x : E) (h : x ≠ 0) : ∃ g : E →L[𝕜] 𝕜, ∥g∥ = 1 ∧ g x = norm' 𝕜 x :=
 begin
-  cases exists_extension_norm_eq (submodule.span ℝ {x}) (∥x∥ • coord ℝ x h) with g hg,
+  let p : submodule 𝕜 E := span 𝕜 {x},
+  let f := norm' 𝕜 x • coord 𝕜 x h,
+  obtain ⟨g, hg⟩ := has_exists_extension_norm_eq.exists_extension_norm_eq E p f,
   use g, split,
   { rw [hg.2, coord_norm'] },
-  { calc g x = g (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span ℝ {x}) : by simp
-  ... = (∥x∥ • coord ℝ x h) (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span ℝ {x}) : by rw ← hg.1
-  ... = ∥x∥ : by rw coord_self' }
+  { calc g x = g (⟨x, mem_span_singleton_self x⟩ : span 𝕜 {x}) : by rw coe_mk
+    ... = (norm' 𝕜 x • coord 𝕜 x h) (⟨x, mem_span_singleton_self x⟩ : span 𝕜 {x}) : by rw ← hg.1
+    ... = norm' 𝕜 x : by simp [coord_self] }
 end
 
 /-- Variant of the above theorem, eliminating the hypothesis that `x` be nonzero, and choosing
     the dual element arbitrarily when `x = 0`. -/
-theorem exists_dual_vector' [nontrivial E] (x : E) : ∃ g : E →L[ℝ] ℝ,
-  ∥g∥ = 1 ∧ g x = ∥x∥ :=
+theorem exists_dual_vector' [nontrivial E] (x : E) :
+  ∃ g : E →L[𝕜] 𝕜, ∥g∥ = 1 ∧ g x = norm' 𝕜 x :=
 begin
   by_cases hx : x = 0,
-  { rcases exists_ne (0 : E) with ⟨y, hy⟩,
-    cases exists_dual_vector y hy with g hg,
-    use g, refine ⟨hg.left, _⟩, simp [hx] },
+  { obtain ⟨y, hy⟩ := exists_ne (0 : E),
+    obtain ⟨g, hg⟩ : ∃ g : E →L[𝕜] 𝕜, ∥g∥ = 1 ∧ g y = norm' 𝕜 y := exists_dual_vector y hy,
+    refine ⟨g, hg.left, _⟩,
+    rw [norm'_def, hx, norm_zero, ring_hom.map_zero, continuous_linear_map.map_zero] },
   { exact exists_dual_vector x hx }
 end
 
--- TODO: These corollaries are also true over ℂ.
-
 end dual_vector

src/analysis/normed_space/operator_norm.lean

@@ -826,6 +826,10 @@ begin
     rw this, apply homothety_inverse, exact hx, exact to_span_nonzero_singleton_homothety 𝕜 x h, }
 end
 
+lemma coord_self (x : E) (h : x ≠ 0) :
+  (coord 𝕜 x h) (⟨x, submodule.mem_span_singleton_self x⟩ : submodule.span 𝕜 ({x} : set E)) = 1 :=
+linear_equiv.coord_self 𝕜 E x h
+
 variable (E)
 
 /-- The continuous linear equivalences from `E` to itself form a group under composition. -/