chore(analysis/inner_product/projections): generalize some lemmas (#1…

…0608)

* generalize a few lemmas from `[finite_dimensional 𝕜 ?x]` to `[complete_space ?x]`;
* drop unneeded TC assumption in `isometry.tendsto_nhds_iff`;
* image of a complete set/submodule under an isometry is a complete set/submodule.

src/analysis/inner_product_space/projection.lean

@@ -498,21 +498,26 @@ begin
   { simp }
 end
 
+lemma linear_isometry.map_orthogonal_projection {E E' : Type*} [inner_product_space 𝕜 E]
+  [inner_product_space 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [complete_space p]
+  (x : E) :
+  f (orthogonal_projection p x) = orthogonal_projection (p.map f.to_linear_map) (f x) :=
+begin
+  refine (eq_orthogonal_projection_of_mem_of_inner_eq_zero (submodule.apply_coe_mem_map _ _) $
+    λ y hy, _).symm,
+  rcases hy with ⟨x', hx', rfl : f x' = y⟩,
+  rw [f.coe_to_linear_map, ← f.map_sub, f.inner_map_map,
+    orthogonal_projection_inner_eq_zero x x' hx']
+end
+
 /-- Orthogonal projection onto the `submodule.map` of a subspace. -/
 lemma orthogonal_projection_map_apply {E E' : Type*} [inner_product_space 𝕜 E]
-  [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [finite_dimensional 𝕜 p]
+  [inner_product_space 𝕜 E'] (f : E ≃ₗᵢ[𝕜] E') (p : submodule 𝕜 E) [complete_space p]
   (x : E') :
   (orthogonal_projection (p.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x : E')
   = f (orthogonal_projection p (f.symm x)) :=
-begin
-  apply eq_orthogonal_projection_of_mem_of_inner_eq_zero,
-  { exact ⟨orthogonal_projection p (f.symm x), submodule.coe_mem _, by simp⟩, },
-  rintros w ⟨a, ha, rfl⟩,
-  suffices : inner (f (f.symm x - orthogonal_projection p (f.symm x))) (f a) = (0:𝕜),
-  { simpa using this },
-  rw f.inner_map_map,
-  exact orthogonal_projection_inner_eq_zero _ _ ha,
-end
+by simpa only [f.coe_to_linear_isometry, f.apply_symm_apply]
+  using (f.to_linear_isometry.map_orthogonal_projection p (f.symm x)).symm
 
 /-- The orthogonal projection onto the trivial submodule is the zero map. -/
 @[simp] lemma orthogonal_projection_bot : orthogonal_projection (⊥ : submodule 𝕜 E) = 0 :=
@@ -634,13 +639,13 @@ lemma reflection_mem_subspace_eq_self {x : E} (hx : x ∈ K) : reflection K x =
 
 /-- Reflection in the `submodule.map` of a subspace. -/
 lemma reflection_map_apply {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
-  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] (x : E') :
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [complete_space K] (x : E') :
   reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) x = f (reflection K (f.symm x)) :=
 by simp [bit0, reflection_apply, orthogonal_projection_map_apply f K x]
 
 /-- Reflection in the `submodule.map` of a subspace. -/
 lemma reflection_map {E E' : Type*} [inner_product_space 𝕜 E] [inner_product_space 𝕜 E']
-  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [finite_dimensional 𝕜 K] :
+  (f : E ≃ₗᵢ[𝕜] E') (K : submodule 𝕜 E) [complete_space K] :
   reflection (K.map (f.to_linear_equiv : E →ₗ[𝕜] E')) = f.symm.trans ((reflection K).trans f) :=
 linear_isometry_equiv.ext $ reflection_map_apply f K
 

src/analysis/normed_space/linear_isometry.lean

@@ -85,6 +85,17 @@ f.to_linear_map.map_smul c x
 protected lemma isometry : isometry f :=
 f.to_linear_map.to_add_monoid_hom.isometry_of_norm f.norm_map
 
+@[simp] lemma is_complete_image_iff {s : set E} : is_complete (f '' s) ↔ is_complete s :=
+is_complete_image_iff f.isometry.uniform_inducing
+
+lemma is_complete_map_iff [ring_hom_surjective σ₁₂] {p : submodule R E} :
+  is_complete (p.map f.to_linear_map : set E₂) ↔ is_complete (p : set E) :=
+f.is_complete_image_iff
+
+instance complete_space_map [ring_hom_surjective σ₁₂] (p : submodule R E) [complete_space p] :
+  complete_space (p.map f.to_linear_map) :=
+(f.is_complete_map_iff.2 $ complete_space_coe_iff_is_complete.1 ‹_›).complete_space_coe
+
 @[simp] lemma dist_map (x y : E) : dist (f x) (f y) = dist x y := f.isometry.dist_eq x y
 @[simp] lemma edist_map (x y : E) : edist (f x) (f y) = edist x y := f.isometry.edist_eq x y
 
@@ -398,6 +409,10 @@ e.isometry.comp_continuous_on_iff
   continuous (e ∘ f) ↔ continuous f :=
 e.isometry.comp_continuous_iff
 
+instance complete_space_map (p : submodule R E) [complete_space p] :
+  complete_space (p.map (e.to_linear_equiv : E →ₛₗ[σ₁₂] E₂)) :=
+e.to_linear_isometry.complete_space_map p
+
 include σ₂₁
 /-- Construct a linear isometry equiv from a surjective linear isometry. -/
 noncomputable def of_surjective (f : F →ₛₗᵢ[σ₁₂] E₂)

src/topology/metric_space/isometry.lean

@@ -133,10 +133,10 @@ theorem isometry.closed_embedding [complete_space α] [emetric_space β]
   {f : α → β} (hf : isometry f) : closed_embedding f :=
 hf.antilipschitz.closed_embedding hf.lipschitz.uniform_continuous
 
-lemma isometry.tendsto_nhds_iff [complete_space α] [emetric_space β] {ι : Type*} {f : α → β}
+lemma isometry.tendsto_nhds_iff [emetric_space β] {ι : Type*} {f : α → β}
   {g : ι → α} {a : filter ι} {b : α} (hf : isometry f) :
   filter.tendsto g a (𝓝 b) ↔ filter.tendsto (f ∘ g) a (𝓝 (f b)) :=
-hf.closed_embedding.tendsto_nhds_iff
+hf.embedding.tendsto_nhds_iff
 
 end emetric_isometry --section