feat(analysis/normed_space/dual): Fréchet-Riesz representation for th…

…e dual of a Hilbert space (#4379)

This PR defines `to_dual` which maps an element `x` of an inner product space to `λ y, ⟪x, y⟫`. We also give the Fréchet-Riesz representation, which states that every element of the dual of a Hilbert space `E` has the form `λ u, ⟪x, u⟫` for some `x : E`.



Co-authored-by: Frédéric Dupuis <31101893+dupuisf@users.noreply.github.com>

docs/overview.yaml

@@ -230,6 +230,7 @@ Analysis:
     absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
     Hahn-Banach theorem: 'exists_extension_norm_eq'
     dual of a normed space: 'normed_space.dual'
+    Fréchet-Riesz representation of the dual of a Hilbert space: 'inner_product_space.to_dual'
     isometric inclusion in double dual: 'normed_space.inclusion_in_double_dual_isometry'
     completeness of spaces of bounded continuous functions: 'bounded_continuous_function.complete_space'
 

docs/references.bib

@@ -481,6 +481,14 @@ @book{LurieSAG
   year={last updated 2018},
 }
 
+@book{EinsiedlerWard2017,
+  author = {Einsiedler, Manfred and Ward, Thomas},
+  title = {Functional Analysis, Spectral Theory, and Applications},
+  year = 2017,
+  publisher = {Springer},
+  doi = {10.1007/978-3-319-58540-6},
+}
+
 @book{Elephant,
   title={Sketches of an Elephant – A Topos Theory Compendium},
   author={Peter Johnstone},

docs/undergrad.yaml

@@ -433,7 +433,7 @@ Topology:
     Hilbert projection theorem: 'exists_norm_eq_infi_of_complete_convex'
     orthogonal projection onto closed vector subspaces: 'orthogonal_projection_fn'
     dual space: 'normed_space.dual.inst'
-    Riesz representation theorem:
+    Riesz representation theorem: 'inner_product_space.to_dual'
     $l^2$ and $L^2$ cases:
     Hilbert (orthonormal) bases (in the separable case):
     Hilbert basis of trigonometric polynomials:

src/analysis/normed_space/bounded_linear_maps.lean

@@ -438,3 +438,14 @@ begin
 end
 
 end bilinear_map
+
+/-- A linear isometry preserves the norm. -/
+lemma linear_map.norm_apply_of_isometry (f : E →ₗ[𝕜] F) {x : E} (hf : isometry f) : ∥f x∥ = ∥x∥ :=
+by { simp_rw [←dist_zero_right, ←f.map_zero], exact isometry.dist_eq hf _ _ }
+
+/-- Construct a continuous linear equiv from a linear map that is also an isometry with full range. -/
+def continuous_linear_equiv.of_isometry (f : E →ₗ[𝕜] F) (hf : isometry f) (hfr : f.range = ⊤) :
+  E ≃L[𝕜] F :=
+continuous_linear_equiv.of_homothety 𝕜
+(linear_equiv.of_bijective f (linear_map.ker_eq_bot.mpr (isometry.injective hf)) hfr)
+1 zero_lt_one (λ _, by simp [one_mul, f.norm_apply_of_isometry hf])

src/analysis/normed_space/dual.lean

@@ -1,20 +1,44 @@
 /-
 Copyright (c) 2020 Heather Macbeth. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Heather Macbeth
+Authors: Heather Macbeth, Frédéric Dupuis
 -/
 import analysis.normed_space.hahn_banach
+import analysis.normed_space.inner_product
 
 /-!
 # 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 such as the real or the complex numbers, this map is an isometry.
+We also prove that, for base field `𝕜` with `[is_R_or_C 𝕜]`, this map is an isometry.
+
+We then consider inner product spaces, with base field over `ℝ` (the corresponding results for `ℂ`
+will require the definition of conjugate-linear maps). We define `to_dual_map`, a continuous linear
+map from `E` to its dual, which maps an element `x` of the space to `λ y, ⟪x, y⟫`. We check
+(`to_dual_map_isometry`) that this map is an isometry onto its image, and particular is injective.
+We also define `to_dual'` as the function taking taking a vector to its dual for a base field `𝕜`
+with `[is_R_or_C 𝕜]`; this is a function and not a linear map.
+
+Finally, under the hypothesis of completeness (i.e., for Hilbert spaces), we prove the Fréchet-Riesz
+representation (`to_dual_map_eq_top`), which states the surjectivity: every element of the dual
+of a Hilbert space `E` has the form `λ u, ⟪x, u⟫` for some `x : E`.  This permits the map
+`to_dual_map` to be upgraded to an (isometric) continuous linear equivalence, `to_dual`, between a
+Hilbert space and its dual.
+
+## References
+
+* [M. Einsiedler and T. Ward, *Functional Analysis, Spectral Theory, and Applications*]
+  [EinsiedlerWard2017]
+
+## Tags
+
+dual, Fréchet-Riesz
 -/
 
 noncomputable theory
+open_locale classical
 universes u v
 
 namespace normed_space
@@ -79,7 +103,7 @@ begin
     ... = 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.-/
+/-- The inclusion of a 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
   apply le_antisymm,
@@ -93,3 +117,191 @@ end
 end bidual_isometry
 
 end normed_space
+
+namespace inner_product_space
+open is_R_or_C continuous_linear_map
+
+section is_R_or_C
+
+variables (𝕜 : Type*)
+variables {E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E]
+local notation `⟪`x`, `y`⟫` := @inner 𝕜 E _ x y
+local postfix `†`:90 := @is_R_or_C.conj 𝕜 _
+
+/--
+Given some `x` in an inner product space, we can define its dual as the continuous linear map
+`λ y, ⟪x, y⟫`. Consider using `to_dual` or `to_dual_map` instead in the real case.
+-/
+def to_dual' : E →+ normed_space.dual 𝕜 E :=
+{ to_fun := λ x, linear_map.mk_continuous
+  { to_fun := λ y, ⟪x, y⟫,
+    map_add' := λ _ _, inner_add_right,
+    map_smul' := λ _ _, inner_smul_right }
+  ∥x∥
+  (λ y, by { rw [is_R_or_C.norm_eq_abs], exact abs_inner_le_norm _ _ }),
+  map_zero' := by { ext z, simp },
+  map_add' := λ x y, by { ext z, simp [inner_add_left] } }
+
+@[simp] lemma to_dual'_apply {x y : E} : to_dual' 𝕜 x y = ⟪x, y⟫ := rfl
+
+/-- In an inner product space, the norm of the dual of a vector `x` is `∥x∥` -/
+@[simp] lemma norm_to_dual'_apply (x : E) : ∥to_dual' 𝕜 x∥ = ∥x∥ :=
+begin
+  refine le_antisymm _ _,
+  { exact linear_map.mk_continuous_norm_le _ (norm_nonneg _) _ },
+  { cases eq_or_lt_of_le (norm_nonneg x) with h h,
+    { have : x = 0 := norm_eq_zero.mp (eq.symm h),
+      simp [this] },
+    { refine (mul_le_mul_right h).mp _,
+      calc ∥x∥ * ∥x∥ = ∥x∥ ^ 2 : by ring
+      ... = re ⟪x, x⟫ : norm_sq_eq_inner _
+      ... ≤ abs ⟪x, x⟫ : re_le_abs _
+      ... = ∥to_dual' 𝕜 x x∥ : by simp [norm_eq_abs]
+      ... ≤ ∥to_dual' 𝕜 x∥ * ∥x∥ : le_op_norm (to_dual' 𝕜 x) x } }
+end
+
+variables (E)
+
+lemma to_dual'_isometry : isometry (@to_dual' 𝕜 E _ _) :=
+add_monoid_hom.isometry_of_norm _ (norm_to_dual'_apply 𝕜)
+
+/--
+Fréchet-Riesz representation: any `ℓ` in the dual of a Hilbert space `E` is of the form
+`λ u, ⟪y, u⟫` for some `y : E`, i.e. `to_dual'` is surjective.
+-/
+lemma to_dual'_surjective [complete_space E] : function.surjective (@to_dual' 𝕜 E _ _) :=
+begin
+  intros ℓ,
+  set Y := ker ℓ with hY,
+  by_cases htriv : Y = ⊤,
+  { have hℓ : ℓ = 0,
+    { have h' := linear_map.ker_eq_top.mp htriv,
+      rw [←coe_zero] at h',
+      apply coe_injective,
+      exact h' },
+    exact ⟨0, by simp [hℓ]⟩ },
+  { have Ycomplete := is_complete_ker ℓ,
+    rw [submodule.eq_top_iff_orthogonal_eq_bot Ycomplete, ←hY] at htriv,
+    change Y.orthogonal ≠ ⊥ at htriv,
+    rw [submodule.ne_bot_iff] at htriv,
+    obtain ⟨z : E, hz : z ∈ Y.orthogonal, z_ne_0 : z ≠ 0⟩ := htriv,
+    refine ⟨((ℓ z)† / ⟪z, z⟫) • z, _⟩,
+    ext x,
+    have h₁ : (ℓ z) • x - (ℓ x) • z ∈ Y,
+    { rw [mem_ker, map_sub, map_smul, map_smul, algebra.id.smul_eq_mul, algebra.id.smul_eq_mul,
+          mul_comm],
+      exact sub_self (ℓ x * ℓ z) },
+    have h₂ : (ℓ z) * ⟪z, x⟫ = (ℓ x) * ⟪z, z⟫,
+    { have h₃ := calc
+        0    = ⟪z, (ℓ z) • x - (ℓ x) • z⟫       : by { rw [(Y.mem_orthogonal' z).mp hz], exact h₁ }
+         ... = ⟪z, (ℓ z) • x⟫ - ⟪z, (ℓ x) • z⟫  : by rw [inner_sub_right]
+         ... = (ℓ z) * ⟪z, x⟫ - (ℓ x) * ⟪z, z⟫  : by simp [inner_smul_right],
+      exact sub_eq_zero.mp (eq.symm h₃) },
+    have h₄ := calc
+      ⟪((ℓ z)† / ⟪z, z⟫) • z, x⟫ = (ℓ z) / ⟪z, z⟫ * ⟪z, x⟫
+            : by simp [inner_smul_left, conj_div, conj_conj]
+                            ... = (ℓ z) * ⟪z, x⟫ / ⟪z, z⟫
+            : by rw [←div_mul_eq_mul_div]
+                            ... = (ℓ x) * ⟪z, z⟫ / ⟪z, z⟫
+            : by rw [h₂]
+                            ... = ℓ x
+            : begin
+                have : ⟪z, z⟫ ≠ 0,
+                { change z = 0 → false at z_ne_0,
+                  rwa ←inner_self_eq_zero at z_ne_0 },
+                field_simp [this]
+              end,
+    exact h₄ }
+end
+
+end is_R_or_C
+
+section real
+
+variables {F : Type*} [inner_product_space ℝ F]
+
+/-- In a real inner product space `F`, the function that takes a vector `x` in `F` to its dual
+`λ y, ⟪x, y⟫` is a continuous linear map. If the space is complete (i.e. is a Hilbert space),
+consider using `to_dual` instead. -/
+-- TODO extend to `is_R_or_C` (requires a definition of conjugate linear maps)
+def to_dual_map : F →L[ℝ] (normed_space.dual ℝ F) :=
+linear_map.mk_continuous
+  { to_fun := to_dual' ℝ,
+    map_add' := λ x y, by { ext, simp [inner_add_left] },
+    map_smul' := λ c x, by { ext, simp [inner_smul_left] } }
+  1
+  (λ x, by simp only [norm_to_dual'_apply, one_mul, linear_map.coe_mk])
+
+@[simp] lemma to_dual_map_apply {x y : F} : to_dual_map x y = ⟪x, y⟫_ℝ := rfl
+
+/-- In an inner product space, the norm of the dual of a vector `x` is `∥x∥` -/
+@[simp] lemma norm_to_dual_map_apply (x : F) : ∥to_dual_map x∥ = ∥x∥ := norm_to_dual'_apply _ _
+
+lemma to_dual_map_isometry : isometry (@to_dual_map F _) :=
+add_monoid_hom.isometry_of_norm _ norm_to_dual_map_apply
+
+lemma to_dual_map_injective : function.injective (@to_dual_map F _) :=
+to_dual_map_isometry.injective
+
+@[simp] lemma ker_to_dual_map : (@to_dual_map F _).ker = ⊥ :=
+linear_map.ker_eq_bot.mpr to_dual_map_injective
+
+@[simp] lemma to_dual_map_eq_iff_eq {x y : F} : to_dual_map x = to_dual_map y ↔ x = y :=
+((linear_map.ker_eq_bot).mp (@ker_to_dual_map F _)).eq_iff
+
+variables [complete_space F]
+
+/--
+Fréchet-Riesz representation: any `ℓ` in the dual of a real Hilbert space `F` is of the form
+`λ u, ⟪y, u⟫` for some `y` in `F`.  See `inner_product_space.to_dual` for the continuous linear
+equivalence thus induced.
+-/
+-- TODO extend to `is_R_or_C` (requires a definition of conjugate linear maps)
+lemma range_to_dual_map : (@to_dual_map F _).range = ⊤ :=
+linear_map.range_eq_top.mpr (to_dual'_surjective ℝ F)
+
+/--
+Fréchet-Riesz representation: If `F` is a Hilbert space, the function that takes a vector in `F` to
+its dual is a continuous linear equivalence.  -/
+def to_dual : F ≃L[ℝ] (normed_space.dual ℝ F) :=
+continuous_linear_equiv.of_isometry to_dual_map.to_linear_map to_dual_map_isometry range_to_dual_map
+
+/--
+Fréchet-Riesz representation: If `F` is a Hilbert space, the function that takes a vector in `F` to
+its dual is an isometry.  -/
+def isometric.to_dual : F ≃ᵢ normed_space.dual ℝ F :=
+{ to_equiv := to_dual.to_linear_equiv.to_equiv,
+  isometry_to_fun := to_dual'_isometry ℝ F}
+
+@[simp] lemma to_dual_apply {x y : F} : to_dual x y = ⟪x, y⟫_ℝ := rfl
+
+@[simp] lemma to_dual_eq_iff_eq {x y : F} : to_dual x = to_dual y ↔ x = y :=
+(@to_dual F _ _).injective.eq_iff
+
+lemma to_dual_eq_iff_eq' {x x' : F} : (∀ y : F, ⟪x, y⟫_ℝ = ⟪x', y⟫_ℝ) ↔ x = x' :=
+begin
+  split,
+  { intros h,
+    have : to_dual x = to_dual x' → x = x' := to_dual_eq_iff_eq.mp,
+    apply this,
+    simp_rw [←to_dual_apply] at h,
+    ext z,
+    exact h z },
+  { rintros rfl y,
+    refl }
+end
+
+@[simp] lemma norm_to_dual_apply (x : F) : ∥to_dual x∥ = ∥x∥ := norm_to_dual_map_apply x
+
+/-- In a Hilbert space, the norm of a vector in the dual space is the norm of its corresponding
+primal vector. -/
+lemma norm_to_dual_symm_apply (ℓ : normed_space.dual ℝ F) : ∥to_dual.symm ℓ∥ = ∥ℓ∥ :=
+begin
+  have : ℓ = to_dual (to_dual.symm ℓ) := by simp only [continuous_linear_equiv.apply_symm_apply],
+  conv_rhs { rw [this] },
+  refine eq.symm (norm_to_dual_apply _),
+end
+
+end real
+
+end inner_product_space

src/analysis/normed_space/inner_product.lean

@@ -424,7 +424,7 @@ lemma inner_smul_real_right {x y : E} {r : ℝ} : ⟪x, (r : 𝕜) • y⟫ = r
 by { rw [inner_smul_right, algebra.smul_def], refl }
 
 /-- The inner product as a sesquilinear form. -/
-def sesq_form_of_inner : sesq_form 𝕜 E conj_to_ring_equiv :=
+def sesq_form_of_inner : sesq_form 𝕜 E (conj_to_ring_equiv 𝕜) :=
 { sesq := λ x y, ⟪y, x⟫,    -- Note that sesquilinear forms are linear in the first argument
   sesq_add_left := λ x y z, inner_add_right,
   sesq_add_right := λ x y z, inner_add_left,

src/analysis/normed_space/operator_norm.lean

@@ -154,6 +154,19 @@ end
 
 end normed_field
 
+section add_monoid_hom
+
+lemma add_monoid_hom.isometry_of_norm (f : E →+ F) (hf : ∀ x, ∥f x∥ = ∥x∥) : isometry f :=
+begin
+  intros x y,
+  simp_rw [edist_dist],
+  congr',
+  simp_rw [dist_eq_norm, ←add_monoid_hom.map_sub],
+  exact hf (x - y),
+end
+
+end add_monoid_hom
+
 variables [nondiscrete_normed_field 𝕜] [normed_space 𝕜 E] [normed_space 𝕜 F] [normed_space 𝕜 G]
 (c : 𝕜) (f g : E →L[𝕜] F) (h : F →L[𝕜] G) (x y z : E)
 include 𝕜

src/data/complex/is_R_or_C.lean

@@ -206,6 +206,7 @@ begin
   { rintros ⟨r, rfl⟩, apply conj_of_real }
 end
 
+variables (K)
 /-- Conjugation as a ring equivalence. This is used to convert the inner product into a
 sesquilinear product. -/
 def conj_to_ring_equiv : K ≃+* Kᵒᵖ :=
@@ -216,6 +217,10 @@ def conj_to_ring_equiv : K ≃+* Kᵒᵖ :=
   map_mul' := λ x y, by simp [mul_comm],
   map_add' := λ x y, by simp }
 
+variables {K}
+
+@[simp] lemma ring_equiv_apply {x : K} : (conj_to_ring_equiv K x).unop = x† := rfl
+
 lemma eq_conj_iff_re {z : K} : conj z = z ↔ ((re z) : K) = z :=
 eq_conj_iff_real.trans ⟨by rintro ⟨r, rfl⟩; simp, λ h, ⟨_, h.symm⟩⟩