refactor(analysis/{normed_space, inner_product_space}/dual): redefine…

… using `linear_isometry` (#9569)

Linear isometric embeddings appear naturally when studying the duals of normed spaces:  the map `λ y, ⟪x, y⟫` from an inner product space to its dual is a linear isometric embedding++, and so is the canonical map from a normed space to its double dual**.

When these natural maps were defined last year, we didn't have the definition `linear_isometry` (notation: `X →ₗᵢ[R] Y`), so they were defined as continuous linear maps which satisfied the predicate `isometry`, and several lemmas were proven ad-hoc which are now available as general lemmas about  `linear_isometry`.

This PR refactors to use the `linear_isometry` structure.  Lemmas deleted (I have been enthusiastic here, and can scale back if desired ...):
normed_space.inclusion_in_double_dual_isometry
inner_product_space.to_dual_map_isometry
inner_product_space.to_dual_map_injective
inner_product_space.ker_to_dual_map
inner_product_space.to_dual_map_eq_iff_eq 
inner_product_space.range_to_dual_map
inner_product_space.isometric.to_dual
inner_product_space.to_dual_eq_iff_eq
inner_product_space.to_dual_eq_iff_eq'
inner_product_space.norm_to_dual_apply
inner_product_space.norm_to_dual_symm_apply

++ (over `ℝ` -- over `ℂ` it's conjugate-linear, which will be dealt with in future PRs)
** over `ℝ` or `ℂ`

docs/overview.yaml

@@ -253,7 +253,7 @@ Analysis:
     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'
+    isometric inclusion in double dual: 'normed_space.inclusion_in_double_dual_li'
     completeness of spaces of bounded continuous functions: 'bounded_continuous_function.complete_space'
 
   Differentiability:

docs/undergrad.yaml

@@ -213,7 +213,7 @@ Bilinear and Quadratic Forms Over a Vector Space:
   Euclidean and Hermitian spaces:
     Euclidean vector spaces: 'inner_product_space'
     Hermitian vector spaces: 'inner_product_space'
-    dual isomorphism in the euclidean case: 'inner_product_space.isometric.to_dual'
+    dual isomorphism in the euclidean case: 'inner_product_space.to_dual'
     orthogonal complement: 'submodule.orthogonal'
     Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
     norm: 'inner_product_space.of_core.to_has_norm'

src/analysis/inner_product_space/dual.lean

@@ -10,17 +10,15 @@ import analysis.normed_space.dual
 # The Fréchet-Riesz representation theorem
 
 We 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 `𝕜`
+will require the definition of conjugate-linear maps). We define `to_dual_map`, a linear isometric
+embedding of `E` into its dual, which maps an element `x` of the space to `λ y, ⟪x, y⟫`. 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.
+Finally, under the hypothesis of completeness (i.e., for Hilbert spaces), we upgrade this to
+`to_dual`, a linear isometric *equivalence* of `E` onto its dual; that is, we establish the
+surjectivity of `to_dual'`.  This is the Fréchet-Riesz representation theorem: every element of the
+dual of a Hilbert space `E` has the form `λ u, ⟪x, u⟫` for some `x : E`.
 
 ## References
 
@@ -136,89 +134,33 @@ end is_R_or_C
 
 section real
 
-variables {F : Type*} [inner_product_space ℝ F]
+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),
+`λ y, ⟪x, y⟫` is an isometric linear embedding. 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])
+def to_dual_map : F →ₗᵢ[ℝ] (normed_space.dual ℝ F) :=
+{ to_fun := to_dual' ℝ,
+  map_add' := λ x y, by { ext, simp [inner_add_left] },
+  map_smul' := λ c x, by { ext, simp [inner_smul_left] },
+  norm_map' := norm_to_dual'_apply ℝ }
 
-@[simp] lemma to_dual_map_apply {x y : F} : to_dual_map x y = ⟪x, y⟫_ℝ := rfl
+variables {F}
 
-/-- 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 F _).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
+@[simp] lemma to_dual_map_apply {x y : F} : to_dual_map F x y = ⟪x, y⟫_ℝ := rfl
 
-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)
+variables (F) [complete_space 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
+its dual is an isometric linear equivalence.  -/
+def to_dual : F ≃ₗᵢ[ℝ] (normed_space.dual ℝ F) :=
+linear_isometry_equiv.of_surjective (to_dual_map F) (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 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
+variables {F}
 
-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
+@[simp] lemma to_dual_apply {x y : F} : to_dual F x y = ⟪x, y⟫_ℝ := rfl
 
 end real
 

src/analysis/normed_space/dual.lean

@@ -8,19 +8,17 @@ 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.
+In this file we define the topological dual `normed_space.dual` of a normed space, and the
+continuous linear map `normed_space.inclusion_in_double_dual` from a normed space into its double
+dual.
 
-We also prove that, for base field `𝕜` with `[is_R_or_C 𝕜]`, this map is an isometry.
+For base field `𝕜 = ℝ` or `𝕜 = ℂ`, this map is actually an isometric embedding; we provide a
+version `normed_space.inclusion_in_double_dual_li` of the map which is of type a bundled linear
+isometric embedding, `E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E))`.
 
 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.
 
-## TODO
-
-Express the construction `inclusion_in_double_dual_isometry` as a `linear_isometry` (not
-difficult, just overlooked).
-
 ## Tags
 
 dual
@@ -97,15 +95,17 @@ begin
 end
 
 /-- 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,
-  { exact double_dual_bound 𝕜 E x },
-  { rw continuous_linear_map.norm_def,
+def inclusion_in_double_dual_li : E →ₗᵢ[𝕜] (dual 𝕜 (dual 𝕜 E)) :=
+{ norm_map' := begin
+    intros x,
+    apply le_antisymm,
+    { exact double_dual_bound 𝕜 E x },
+    rw continuous_linear_map.norm_def,
     apply le_cInf continuous_linear_map.bounds_nonempty,
     rintros c ⟨hc1, hc2⟩,
-    exact norm_le_dual_bound 𝕜 x hc1 hc2 },
-end
+    exact norm_le_dual_bound 𝕜 x hc1 hc2
+  end,
+  .. inclusion_in_double_dual 𝕜 E }
 
 end bidual_isometry
 

src/analysis/normed_space/linear_isometry.lean

@@ -343,6 +343,13 @@ e.isometry.comp_continuous_on_iff
   continuous (e ∘ f) ↔ continuous f :=
 e.isometry.comp_continuous_iff
 
+/-- Construct a linear isometry equiv from a surjective linear isometry. -/
+noncomputable def of_surjective (f : E₁ →ₗᵢ[R] F)
+  (hfr : function.surjective f) :
+  E₁ ≃ₗᵢ[R] F :=
+{ norm_map' := f.norm_map,
+  .. linear_equiv.of_bijective f.to_linear_map f.injective hfr }
+
 variables (R)
 /-- The negation operation on a normed space `E`, considered as a linear isometry equivalence. -/
 def neg : E ≃ₗᵢ[R] E :=