feat(analysis/normed_space/inner_product): inner product is infinitel…

…y smooth (#5089)

Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>

src/analysis/normed_space/inner_product.lean

@@ -20,7 +20,6 @@ dot product in `ℝ^n` and provides the means of defining the length of a vector
 two vectors. In particular vectors `x` and `y` are orthogonal if their inner product equals zero.
 We define both the real and complex cases at the same time using the `is_R_or_C` typeclass.
 
-
 ## Main results
 
 - We define the class `inner_product_space 𝕜 E` extending `normed_space 𝕜 E` with a number of basic
@@ -414,10 +413,16 @@ lemma inner_smul_left {x y : E} {r : 𝕜} : ⟪r • x, y⟫ = r† * ⟪x, y
 inner_product_space.smul_left _ _ _
 lemma real_inner_smul_left {x y : F} {r : ℝ} : ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ := inner_smul_left
 
+lemma inner_smul_real_left {x y : E} {r : ℝ} : ⟪(r : 𝕜) • x, y⟫ = r • ⟪x, y⟫ :=
+by { rw [inner_smul_left, conj_of_real, algebra.smul_def], refl }
+
 lemma inner_smul_right {x y : E} {r : 𝕜} : ⟪x, r • y⟫ = r * ⟪x, y⟫ :=
 by rw [←inner_conj_sym, inner_smul_left, ring_hom.map_mul, conj_conj, inner_conj_sym]
 lemma real_inner_smul_right {x y : F} {r : ℝ} : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ := inner_smul_right
 
+lemma inner_smul_real_right {x y : E} {r : ℝ} : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ :=
+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 :=
 { sesq := λ x y, ⟪y, x⟫,    -- Note that sesquilinear forms are linear in the first argument
@@ -1083,8 +1088,8 @@ instance is_R_or_C.inner_product_space : inner_product_space 𝕜 𝕜 :=
   add_left := λ x y z, by simp [inner, add_mul],
   smul_left := λ x y z, by simp [inner, mul_assoc] }
 
-/-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space
-use `euclidean_space 𝕜 (fin n)`.  -/
+/-- The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional
+space use `euclidean_space 𝕜 (fin n)`. -/
 @[reducible, nolint unused_arguments]
 def euclidean_space (𝕜 : Type*) [is_R_or_C 𝕜]
   (n : Type*) [fintype n] : Type* := pi_Lp 2 one_le_two (λ (i : n), 𝕜)
@@ -1093,17 +1098,14 @@ section is_R_or_C_to_real
 
 variables {G : Type*}
 
-variables (𝕜)
+variables (𝕜 E)
 include 𝕜
 
 /-- A general inner product implies a real inner product. This is not registered as an instance
 since it creates problems with the case `𝕜 = ℝ`. -/
 def has_inner.is_R_or_C_to_real : has_inner ℝ E :=
 { inner := λ x y, re ⟪x, y⟫ }
 
-lemma real_inner_eq_re_inner (x y : E) :
-  @has_inner.inner ℝ E (has_inner.is_R_or_C_to_real 𝕜) x y = re ⟪x, y⟫ := rfl
-
 /-- A general inner product space structure implies a real inner product structure. This is not
 registered as an instance since it creates problems with the case `𝕜 = ℝ`, but in can be used in a
 proof to obtain a real inner product space structure from a given `𝕜`-inner product space
@@ -1118,17 +1120,92 @@ def inner_product_space.is_R_or_C_to_real : inner_product_space ℝ E :=
   smul_left := λ x y r, by {
     change re ⟪(r : 𝕜) • x, y⟫ = r * re ⟪x, y⟫,
     simp [inner_smul_left] },
-  ..has_inner.is_R_or_C_to_real 𝕜,
+  ..has_inner.is_R_or_C_to_real 𝕜 E,
   ..normed_space.restrict_scalars ℝ 𝕜 E }
 
+variable {E}
+
+lemma real_inner_eq_re_inner (x y : E) :
+  @has_inner.inner ℝ E (has_inner.is_R_or_C_to_real 𝕜 E) x y = re ⟪x, y⟫ := rfl
+
 omit 𝕜
 
 /-- A complex inner product implies a real inner product -/
 instance inner_product_space.complex_to_real [inner_product_space ℂ G] : inner_product_space ℝ G :=
-inner_product_space.is_R_or_C_to_real ℂ
+inner_product_space.is_R_or_C_to_real ℂ G
 
 end is_R_or_C_to_real
 
+section deriv
+
+variables [normed_space ℝ E] [is_scalar_tower ℝ 𝕜 E]
+
+lemma is_bounded_bilinear_map_inner : is_bounded_bilinear_map ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
+{ add_left := λ _ _ _, inner_add_left,
+  smul_left := λ r x y,
+    by simp only [← algebra_map_smul 𝕜 r x, algebra_map_eq_of_real, inner_smul_real_left],
+  add_right := λ _ _ _, inner_add_right,
+  smul_right := λ r x y,
+    by simp only [← algebra_map_smul 𝕜 r y, algebra_map_eq_of_real, inner_smul_real_right],
+  bound := ⟨1, zero_lt_one, λ x y,
+    by { rw [one_mul, is_R_or_C.norm_eq_abs], exact abs_inner_le_norm x y, }⟩ }
+
+lemma times_cont_diff_inner {n} : times_cont_diff ℝ n (λ p : E × E, ⟪p.1, p.2⟫) :=
+is_bounded_bilinear_map_inner.times_cont_diff
+
+lemma times_cont_diff_at_inner {p : E × E} {n} :
+  times_cont_diff_at ℝ n (λ p : E × E, ⟪p.1, p.2⟫) p :=
+times_cont_diff_inner.times_cont_diff_at
+
+lemma differentiable_inner : differentiable ℝ (λ p : E × E, ⟪p.1, p.2⟫) :=
+times_cont_diff_inner.differentiable le_rfl
+
+lemma continuous_inner : continuous (λ p : E × E, ⟪p.1, p.2⟫) :=
+differentiable_inner.continuous
+
+variables {G : Type*} [normed_group G] [normed_space ℝ G]
+  {f g : G → E} {f' g' : G →L[ℝ] E} {s : set G} {x : G} {n : with_top ℕ}
+
+include 𝕜
+
+lemma times_cont_diff_within_at.inner (hf : times_cont_diff_within_at ℝ n f s x)
+  (hg : times_cont_diff_within_at ℝ n g s x) :
+  times_cont_diff_within_at ℝ n (λ x, ⟪f x, g x⟫) s x :=
+times_cont_diff_at_inner.comp_times_cont_diff_within_at x (hf.prod hg)
+
+lemma times_cont_diff_at.inner (hf : times_cont_diff_at ℝ n f x)
+  (hg : times_cont_diff_at ℝ n g x) :
+  times_cont_diff_at ℝ n (λ x, ⟪f x, g x⟫) x :=
+hf.inner hg
+
+lemma times_cont_diff_on.inner (hf : times_cont_diff_on ℝ n f s) (hg : times_cont_diff_on ℝ n g s) :
+  times_cont_diff_on ℝ n (λ x, ⟪f x, g x⟫) s :=
+λ x hx, (hf x hx).inner (hg x hx)
+
+lemma times_cont_diff.inner (hf : times_cont_diff ℝ n f) (hg : times_cont_diff ℝ n g) :
+  times_cont_diff ℝ n (λ x, ⟪f x, g x⟫) :=
+times_cont_diff_inner.comp (hf.prod hg)
+
+lemma differentiable_within_at.inner (hf : differentiable_within_at ℝ f s x)
+  (hg : differentiable_within_at ℝ g s x) :
+  differentiable_within_at ℝ (λ x, ⟪f x, g x⟫) s x :=
+((differentiable_inner _).has_fderiv_at.comp_has_fderiv_within_at x
+  (hf.prod hg).has_fderiv_within_at).differentiable_within_at
+
+lemma differentiable_at.inner (hf : differentiable_at ℝ f x) (hg : differentiable_at ℝ g x) :
+  differentiable_at ℝ (λ x, ⟪f x, g x⟫) x :=
+(differentiable_inner _).comp x (hf.prod hg)
+
+lemma differentiable_on.inner (hf : differentiable_on ℝ f s) (hg : differentiable_on ℝ g s) :
+  differentiable_on ℝ (λ x, ⟪f x, g x⟫) s :=
+λ x hx, (hf x hx).inner (hg x hx)
+
+lemma differentiable.inner (hf : differentiable ℝ f) (hg : differentiable ℝ g) :
+  differentiable ℝ (λ x, ⟪f x, g x⟫) :=
+λ x, (hf x).inner (hg x)
+
+end deriv
+
 section pi_Lp
 local attribute [reducible] pi_Lp
 variables {ι : Type*} [fintype ι]
@@ -1360,7 +1437,7 @@ This point `v` is usually called the orthogonal projection of `u` onto `K`.
 theorem exists_norm_eq_infi_of_complete_subspace (K : subspace 𝕜 E)
   (h : is_complete (↑K : set E)) : ∀ u : E, ∃ v ∈ K, ∥u - v∥ = ⨅ w : (K : set E), ∥u - w∥ :=
 begin
-  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜,
+  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
   letI : module ℝ E := restrict_scalars.semimodule ℝ 𝕜 E,
   letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let K' : subspace ℝ E := submodule.restrict_scalars ℝ K,
@@ -1419,7 +1496,7 @@ for all `w ∈ K`, `⟪u - v, w⟫ = 0` (i.e., `u - v` is orthogonal to the subs
 theorem norm_eq_infi_iff_inner_eq_zero (K : subspace 𝕜 E) {u : E} {v : E}
   (hv : v ∈ K) : ∥u - v∥ = (⨅ w : (↑K : set E), ∥u - w∥) ↔ ∀ w ∈ K, ⟪u - v, w⟫ = 0 :=
 begin
-  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜,
+  letI : inner_product_space ℝ E := inner_product_space.is_R_or_C_to_real 𝕜 E,
   letI : module ℝ E := restrict_scalars.semimodule ℝ 𝕜 E,
   letI : is_scalar_tower ℝ 𝕜 E := restrict_scalars.is_scalar_tower _ _ _,
   let K' : subspace ℝ E := K.restrict_scalars ℝ,

src/data/complex/is_R_or_C.lean

@@ -75,6 +75,8 @@ See Note [coercion into rings], or `data/nat/cast.lean` for more details. -/
 lemma of_real_alg (x : ℝ) : (x : K) = x • (1 : K) :=
 algebra.algebra_map_eq_smul_one x
 
+lemma algebra_map_eq_of_real : ⇑(algebra_map ℝ K) = coe := rfl
+
 @[simp] lemma re_add_im (z : K) : ((re z) : K) + (im z) * I = z := is_R_or_C.re_add_im_ax z
 @[simp, norm_cast] lemma of_real_re : ∀ r : ℝ, re (r : K) = r := is_R_or_C.of_real_re_ax
 @[simp, norm_cast] lemma of_real_im : ∀ r : ℝ, im (r : K) = 0 := is_R_or_C.of_real_im_ax