chore(analysis/normed_space/linear_isometry): adjust isometry API (#…

…9635)

Now that we have the `linear_isometry` definition, it is better to pass through this definition rather then using a `linear_map` satisfying the `isometry` hypothesis.  To this end, convert old lemma `linear_map.norm_apply_of_isometry` to a new definition `linear_map.to_linear_isometry`, and delete old definition `continuous_linear_equiv.of_isometry`, whose use should be replaced by the pair of definitions`linear_map.to_linear_isometry`, `linear_isometry_equiv.of_surjective`.

src/analysis/normed_space/basic.lean

@@ -342,6 +342,8 @@ instance {r : ℝ} : has_neg (sphere (0:α) r) :=
 rfl
 
 namespace isometric
+-- TODO This material is superseded by similar constructions such as
+-- `affine_isometry_equiv.const_vadd`; deduplicate
 
 /-- Addition `y ↦ y + x` as an `isometry`. -/
 protected def add_right (x : α) : α ≃ᵢ α :=

src/analysis/normed_space/bounded_linear_maps.lean

@@ -31,7 +31,6 @@ is normed) that `∥f x∥` is bounded by a multiple of `∥x∥`. Hence the "bo
 ## Main theorems
 
 * `is_bounded_bilinear_map.continuous`: A bounded bilinear map is continuous.
-* `linear_map.norm_apply_of_isometry`: A linear isometry preserves the norm.
 * `continuous_linear_equiv.is_open`: The continuous linear equivalences are an open subset of the
   set of continuous linear maps between a pair of Banach spaces.  Placed in this file because its
   proof uses `is_bounded_bilinear_map.continuous`.
@@ -497,18 +496,6 @@ 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 (isometry.injective hf) (linear_map.range_eq_top.mp hfr))
-  1 zero_lt_one (λ _, by simp [one_mul, f.norm_apply_of_isometry hf])
-
 namespace continuous_linear_equiv
 
 open set

src/analysis/normed_space/linear_isometry.lean

@@ -161,6 +161,11 @@ instance : monoid (E →ₗᵢ[R] E) :=
 
 end linear_isometry
 
+/-- Construct a `linear_isometry` from a `linear_map` satisfying `isometry`. -/
+def linear_map.to_linear_isometry (f : E →ₛₗ[σ₁₂] E₂) (hf : isometry f) : E →ₛₗᵢ[σ₁₂] E₂ :=
+{ norm_map' := by { simp_rw [←dist_zero_right, ←f.map_zero], exact λ x, hf.dist_eq x _ },
+  .. f }
+
 namespace submodule
 
 variables {R' : Type*} [ring R'] [module R' E] (p : submodule R' E)

src/analysis/normed_space/operator_norm.lean

@@ -400,7 +400,9 @@ begin
   simp [subsingleton.elim x 0]
 end
 
-/-- A continuous linear map is an isometry if and only if it preserves the norm. -/
+/-- A continuous linear map is an isometry if and only if it preserves the norm.
+(Note: Do you really want to use this lemma?  Try using the bundled structure `linear_isometry`
+instead.) -/
 lemma isometry_iff_norm : isometry f ↔ ∀x, ∥f x∥ = ∥x∥ :=
 f.to_linear_map.to_add_monoid_hom.isometry_iff_norm