feat(normed_space/dual): (topological) dual of a normed space (#3021)

Define the topological dual of a normed space, and prove that over the reals, the inclusion into the double dual is an isometry.

Supporting material:  a corollary of Hahn-Banach; material about spans of singletons added to `linear_algebra.basic` and `normed_space.operator_norm`; material about homotheties added to `normed_space.operator_norm`.

src/analysis/normed_space/basic.lean

@@ -610,14 +610,15 @@ begin
   exact (tendsto_inv hx)
 end
 
+end normed_field
+
 instance : normed_field ℝ :=
 { norm := λ x, abs x,
   dist_eq := assume x y, rfl,
   norm_mul' := abs_mul }
 
 instance : nondiscrete_normed_field ℝ :=
 { non_trivial := ⟨2, by { unfold norm, rw abs_of_nonneg; norm_num }⟩ }
-end normed_field
 
 /-- If a function converges to a nonzero value, its inverse converges to the inverse of this value.
 We use the name `tendsto.inv'` as `tendsto.inv` is already used in multiplicative topological
@@ -901,14 +902,18 @@ end prio
 normed_algebra.norm_algebra_map_eq _
 
 @[priority 100]
-instance to_normed_space (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
+instance normed_algebra.to_normed_space (𝕜 : Type*) (𝕜' : Type*) [normed_field 𝕜] [normed_ring 𝕜']
   [h : normed_algebra 𝕜 𝕜'] : normed_space 𝕜 𝕜' :=
 { norm_smul_le := λ s x, calc
     ∥s • x∥ = ∥((algebra_map 𝕜 𝕜') s) * x∥ : by { rw h.smul_def', refl }
     ... ≤ ∥algebra_map 𝕜 𝕜' s∥ * ∥x∥ : normed_ring.norm_mul _ _
     ... = ∥s∥ * ∥x∥ : by rw norm_algebra_map_eq,
   ..h }
 
+instance normed_algebra.id (𝕜 : Type*) [normed_field 𝕜] : normed_algebra 𝕜 𝕜 :=
+{ norm_algebra_map_eq := by simp,
+.. algebra.id 𝕜}
+
 end normed_algebra
 
 section restrict_scalars

src/analysis/normed_space/dual.lean

@@ -0,0 +1,86 @@
+/-
+Copyright (c) 2020 Heather Macbeth. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Heather Macbeth
+-/
+import analysis.normed_space.hahn_banach
+
+/-!
+# The topological dual of a normed space
+
+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.)
+-/
+
+noncomputable theory
+
+namespace normed_space
+
+section general
+variables (𝕜 : Type*) [nondiscrete_normed_field 𝕜]
+variables (E : Type*) [normed_group E] [normed_space 𝕜 E]
+
+/-- The topological dual of a normed space `E`. -/
+@[derive [has_coe_to_fun, normed_group, normed_space 𝕜]] def dual := E →L[𝕜] 𝕜
+
+instance : inhabited (dual 𝕜 E) := ⟨0⟩
+
+/-- 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
+  { to_fun := λ f, f x,
+    map_add'    := by simp,
+    map_smul'   := by simp }
+  ∥x∥
+  (λ f, by { rw mul_comm, exact f.le_op_norm x } )
+
+@[simp] lemma dual_def (x : E) (f : dual 𝕜 E) :
+  ((inclusion_in_double_dual' 𝕜 E) x) f = f x := rfl
+
+lemma double_dual_bound (x : E) : ∥(inclusion_in_double_dual' 𝕜 E) x∥ ≤ ∥x∥ :=
+begin
+  apply continuous_linear_map.op_norm_le_bound,
+  { simp },
+  { intros f, rw mul_comm, exact f.le_op_norm x, }
+end
+
+/-- The inclusion of a normed space in its double (topological) dual, considered
+   as a bounded linear map. -/
+def inclusion_in_double_dual : E →L[𝕜] (dual 𝕜 (dual 𝕜 E)) :=
+linear_map.mk_continuous
+  { to_fun := λ (x : E), (inclusion_in_double_dual' 𝕜 E) x,
+    map_add'    := λ x y, by { ext, simp },
+    map_smul'   := λ (c : 𝕜) x, by { ext, simp } }
+  1
+  (λ x, by { convert double_dual_bound _ _ _, simp } )
+
+end general
+
+section real
+variables (E : Type*) [normed_group E] [normed_space ℝ E]
+
+/-- 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∥ :=
+begin
+  by_cases h : vector_space.dim ℝ E = 0,
+  { rw dim_zero_iff_forall_zero.mp h x, simp },
+  { have h' : 0 < vector_space.dim ℝ E := zero_lt_iff_ne_zero.mpr h,
+    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, simp only [and_imp, set.mem_set_of_eq], intros h₁ h₂,
+    cases exists_dual_vector' h' x with f hf,
+    calc ∥x∥ = f x : hf.2.symm
+    ... ≤ ∥f x∥ : le_max_left (f x) (-f x)
+    ... ≤ c * ∥f∥ : h₂ f
+    ... = c : by rw [ hf.1, mul_one ] }
+end
+
+-- TODO: This is also true over ℂ.
+
+end real
+
+end normed_space

src/analysis/normed_space/hahn_banach.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2020 Yury Kudryashov All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Yury Kudryashov
+Authors: Yury Kudryashov, Heather Macbeth
 -/
 import analysis.normed_space.operator_norm
 import analysis.convex.cone
@@ -12,12 +12,15 @@ import analysis.convex.cone
 In this file we prove a version of Hahn-Banach theorem for continuous linear
 functions on normed spaces.
 
+We also prove a standard corollary, needed for the isometric inclusion in the double dual.
+
 ## TODO
 
-Prove some corollaries
+Prove more corollaries
 
 -/
 
+section basic
 variables {E : Type*} [normed_group E] [normed_space ℝ E]
 
 /-- Hahn-Banach theorem for continuous linear functions. -/
@@ -39,3 +42,49 @@ begin
   { simp only [← mul_add],
     exact mul_le_mul_of_nonneg_left (norm_add_le x y) (norm_nonneg f) }
 end
+
+end basic
+
+section dual_vector
+variables {E : Type*} [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) : ∥∥x∥ • coord ℝ x h∥ = 1 :=
+by rw [norm_smul, norm_norm, coord_norm, mul_inv_cancel (mt norm_eq_zero.mp h)]
+
+/-- 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∥ :=
+begin
+  cases exists_extension_norm_eq (submodule.span ℝ {x}) (∥x∥ • coord ℝ x h) with g hg,
+  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' }
+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' (h : 0 < vector_space.dim ℝ E) (x : E) : ∃ g : E →L[ℝ] ℝ,
+  ∥g∥ = 1 ∧ g x = ∥x∥ :=
+begin
+  by_cases hx : x = 0,
+  { cases dim_pos_iff_exists_ne_zero.mp h with y hy,
+    cases exists_dual_vector y hy with g hg,
+    use g, refine ⟨hg.left, _⟩, simp [hx] },
+  { exact exists_dual_vector x hx }
+end
+
+-- TODO: These corollaries are also true over ℂ.
+
+end dual_vector

src/analysis/normed_space/operator_norm.lean

@@ -8,6 +8,7 @@ Operator norm on the space of continuous linear maps
 Define the operator norm on the space of continuous linear maps between normed spaces, and prove
 its basic properties. In particular, show that this space is itself a normed space.
 -/
+import linear_algebra.finite_dimensional
 import analysis.normed_space.riesz_lemma
 import analysis.asymptotics
 noncomputable theory
@@ -200,6 +201,24 @@ theorem is_O_sub (f : E →L[𝕜] F) (l : filter E) (x : E) :
   is_O (λ x', f (x' - x)) (λ x', x' - x) l :=
 f.is_O_comp _ l
 
+/-- A linear map which is a homothety is a continuous linear map.
+    Since the field `𝕜` need not have `ℝ` as a subfield, this theorem is not directly deducible from
+    the corresponding theorem about isometries plus a theorem about scalar multiplication.  Likewise
+    for the other theorems about homotheties in this file.
+ -/
+def of_homothety (f : E →ₗ[𝕜] F) (a : ℝ) (hf : ∀x, ∥f x∥ = a * ∥x∥) : E →L[𝕜] F :=
+f.mk_continuous a (λ x, le_of_eq (hf x))
+
+variable (𝕜)
+
+lemma to_span_singleton_homothety (x : E) (c : 𝕜) : ∥linear_map.to_span_singleton 𝕜 E x c∥ = ∥x∥ * ∥c∥ :=
+by {rw mul_comm, exact norm_smul _ _}
+
+/-- Given an element `x` of a normed space `E` over a field `𝕜`, the natural continuous
+    linear map from `E` to the span of `x`.-/
+def to_span_singleton (x : E) : 𝕜 →L[𝕜] E :=
+of_homothety (linear_map.to_span_singleton 𝕜 E x) ∥x∥ (to_span_singleton_homothety 𝕜 x)
+
 end
 
 section op_norm
@@ -336,6 +355,25 @@ begin
     rw [dist_eq_norm, dist_eq_norm, ← f.map_sub, H] }
 end
 
+lemma homothety_norm (hE : 0 < vector_space.dim 𝕜 E) (f : E →L[𝕜] F) {a : ℝ} (ha : 0 ≤ a) (hf : ∀x, ∥f x∥ = a * ∥x∥) :
+  ∥f∥ = a :=
+begin
+  refine le_antisymm_iff.mpr ⟨_, _⟩,
+  { exact continuous_linear_map.op_norm_le_bound f ha (λ y, le_of_eq (hf y)) },
+  { rw continuous_linear_map.norm_def,
+    apply real.lb_le_Inf _ continuous_linear_map.bounds_nonempty,
+    cases dim_pos_iff_exists_ne_zero.mp hE with x hx,
+    intros c h, rw mem_set_of_eq at h,
+    apply (mul_le_mul_right (norm_pos_iff.mpr hx)).mp,
+    rw ← hf x, exact h.2 x }
+end
+
+lemma to_span_singleton_norm (x : E) : ∥to_span_singleton 𝕜 x∥ = ∥x∥ :=
+begin
+  refine homothety_norm _ _ (norm_nonneg x) (to_span_singleton_homothety 𝕜 x),
+  rw dim_of_field, exact cardinal.zero_lt_one,
+end
+
 variable (f)
 
 theorem uniform_embedding_of_bound {K : nnreal} (hf : ∀ x, ∥x∥ ≤ K * ∥f x∥) :
@@ -631,6 +669,57 @@ lemma subsingleton_or_norm_symm_pos : subsingleton E ∨ 0 < ∥(e.symm : F →L
 lemma subsingleton_or_nnnorm_symm_pos : subsingleton E ∨ 0 < (nnnorm $ (e.symm : F →L[𝕜] E)) :=
 subsingleton_or_norm_symm_pos e
 
+lemma homothety_inverse (a : ℝ) (ha : 0 < a) (f : E ≃ₗ[𝕜] F) :
+  (∀ (x : E), ∥f x∥ = a * ∥x∥) → (∀ (y : F), ∥f.symm y∥ = a⁻¹ * ∥y∥) :=
+begin
+  intros hf y,
+  calc ∥(f.symm) y∥ = a⁻¹ * (a * ∥ (f.symm) y∥) : _
+  ... =  a⁻¹ * ∥f ((f.symm) y)∥ : by rw hf
+  ... = a⁻¹ * ∥y∥ : by simp,
+  rw [← mul_assoc, inv_mul_cancel (ne_of_lt ha).symm, one_mul],
+end
+
+variable (𝕜)
+
+/-- A linear equivalence which is a homothety is a continuous linear equivalence. -/
+def of_homothety (f : E ≃ₗ[𝕜] F) (a : ℝ) (ha : 0 < a) (hf : ∀x, ∥f x∥ = a * ∥x∥) : E ≃L[𝕜] F :=
+{ to_linear_equiv := f,
+  continuous_to_fun := f.to_linear_map.continuous_of_bound a (λ x, le_of_eq (hf x)),
+  continuous_inv_fun := f.symm.to_linear_map.continuous_of_bound a⁻¹
+    (λ x, le_of_eq (homothety_inverse a ha f hf x)) }
+
+lemma to_span_nonzero_singleton_homothety (x : E) (h : x ≠ 0) (c : 𝕜) :
+  ∥linear_equiv.to_span_nonzero_singleton 𝕜 E x h c∥ = ∥x∥ * ∥c∥ :=
+continuous_linear_map.to_span_singleton_homothety _ _ _
+
+/-- Given a nonzero element `x` of a normed space `E` over a field `𝕜`, the natural
+    continuous linear equivalence from `E` to the span of `x`.-/
+def to_span_nonzero_singleton (x : E) (h : x ≠ 0) : 𝕜 ≃L[𝕜] (submodule.span 𝕜 ({x} : set E)) :=
+of_homothety 𝕜
+  (linear_equiv.to_span_nonzero_singleton 𝕜 E x h)
+  ∥x∥
+  (norm_pos_iff.mpr h)
+  (to_span_nonzero_singleton_homothety 𝕜 x h)
+
+/-- Given a nonzero element `x` of a normed space `E` over a field `𝕜`, the natural continuous
+    linear map from the span of `x` to `𝕜`.-/
+abbreviation coord (x : E) (h : x ≠ 0) : (submodule.span 𝕜 ({x} : set E)) →L[𝕜] 𝕜 :=
+  (to_span_nonzero_singleton 𝕜 x h).symm
+
+lemma coord_norm (x : E) (h : x ≠ 0) : ∥coord 𝕜 x h∥ = ∥x∥⁻¹ :=
+begin
+  have hx : 0 < ∥x∥ := (norm_pos_iff.mpr h),
+  refine continuous_linear_map.homothety_norm _ _ (le_of_lt (inv_pos.mpr hx)) _,
+  { rw ← finite_dimensional.findim_eq_dim,
+    rw ← linear_equiv.findim_eq (linear_equiv.to_span_nonzero_singleton 𝕜 E x h),
+    rw finite_dimensional.findim_of_field,
+    have : 0 = ((0:nat) : cardinal) := rfl,
+    rw this, apply cardinal.nat_cast_lt.mpr, norm_num },
+  { intros y,
+    have : (coord 𝕜 x h) y = (to_span_nonzero_singleton 𝕜 x h).symm y := rfl,
+    rw this, apply homothety_inverse, exact hx, exact to_span_nonzero_singleton_homothety 𝕜 x h, }
+end
+
 end continuous_linear_equiv
 
 lemma linear_equiv.uniform_embedding (e : E ≃ₗ[𝕜] F) (h₁ : continuous e) (h₂ : continuous e.symm) :