[Merged by Bors] - feat(analysis/normed_space): affine map with findim domain is continuous

src/analysis/normed_space/add_torsor.lean

@@ -298,6 +298,19 @@ variables {𝕜 : Type*} [normed_field 𝕜] [normed_space 𝕜 V]
 
 open affine_map
 
+/-- If `f` is an affine map, then its linear part is continuous iff `f` is continuous. -/
+lemma affine_map.continuous_linear_iff [normed_space 𝕜 V'] {f : P →ᵃ[𝕜] P'} :
+  continuous f.linear ↔ continuous f :=
+begin
+  inhabit P,
+  have : (f.linear : V → V') =
+    (isometric.vadd_const $ f $ default P).to_homeomorph.symm ∘ f ∘
+      (isometric.vadd_const $ default P).to_homeomorph,
+  { ext v, simp },
+  rw this,
+  simp only [homeomorph.comp_continuous_iff, homeomorph.comp_continuous_iff'],
+end
+
 @[simp] lemma dist_center_homothety (p₁ p₂ : P) (c : 𝕜) :
   dist p₁ (homothety p₁ c p₂) = ∥c∥ * dist p₁ p₂ :=
 by simp [homothety_def, norm_smul, ← dist_eq_norm_vsub, dist_comm]

src/analysis/normed_space/basic.lean

@@ -78,6 +78,9 @@ variables [normed_group α] [normed_group β]
 lemma dist_eq_norm (g h : α) : dist g h = ∥g - h∥ :=
 normed_group.dist_eq _ _
 
+lemma dist_eq_norm' (g h : α) : dist g h = ∥h - g∥ :=
+by rw [dist_comm, dist_eq_norm]
+
 @[simp] lemma dist_zero_right (g : α) : dist g 0 = ∥g∥ :=
 by rw [dist_eq_norm, sub_zero]
 

src/analysis/normed_space/finite_dimension.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.operator_norm
+import analysis.normed_space.add_torsor
 import topology.bases
 import linear_algebra.finite_dimensional
 import tactic.omega
@@ -164,6 +165,11 @@ begin
   rw linear_equiv.symm_apply_apply
 end
 
+theorem affine_map.continuous_of_finite_dimensional {PE PF : Type*}
+  [metric_space PE] [normed_add_torsor E PE] [metric_space PF] [normed_add_torsor F PF]
+  [finite_dimensional 𝕜 E] (f : PE →ᵃ[𝕜] PF) : continuous f :=
+affine_map.continuous_linear_iff.1 f.linear.continuous_of_finite_dimensional
+
 /-- The continuous linear map induced by a linear map on a finite dimensional space -/
 def linear_map.to_continuous_linear_map [finite_dimensional 𝕜 E] (f : E →ₗ[𝕜] F') : E →L[𝕜] F' :=
 { cont := f.continuous_of_finite_dimensional, ..f }

src/analysis/normed_space/operator_norm.lean

@@ -706,6 +706,8 @@ def apply (v : E) : (E →L[𝕜] F) →L[𝕜] F :=
 
 variables {𝕜 F}
 
+@[simp] lemma apply_apply (v : E) (f : E →L[𝕜] F) : apply 𝕜 F v f = f v := rfl
+
 section multiplication_linear
 variables (𝕜) (𝕜' : Type*) [normed_ring 𝕜'] [normed_algebra 𝕜 𝕜']