split(analysis/normed_space/exponential): split file to minimize depe…

…ndencies (#9932)

As suggested by @urkud, this moves all the results depending on derivatives, `complex.exp` and `real.exp` to a new file `analysis/special_function/exponential`. That way the definitions of `exp` and `[complex, real].exp` are independent, which means we could eventually redefine the latter in terms of the former without breaking the import tree.

src/analysis/normed_space/exponential.lean

@@ -3,12 +3,9 @@ Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Anatole Dedecker
 -/
-import analysis.calculus.deriv
-import analysis.calculus.fderiv_analytic
 import analysis.specific_limits
-import data.complex.exponential
+import analysis.analytic.basic
 import analysis.complex.basic
-import topology.metric_space.cau_seq_filter
 
 /-!
 # Exponential in a Banach algebra
@@ -17,47 +14,35 @@ In this file, we define `exp 𝕂 𝔸`, the exponential map in a normed algebra
 normed field `𝕂`. Although the definition doesn't require `𝔸` to be complete, we need to assume it
 for most results.
 
-We then prove basic results, as described below.
+We then prove some basic results, but we avoid importing derivatives here to minimize dependencies.
+Results involving derivatives and comparisons with `real.exp` and `complex.exp` can be found in
+`analysis/special_functions/exponential`.
 
-## Main result
+## Main results
 
 We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂 = ℝ` or `𝕂 = ℂ`.
 
 ### General case
 
-- `has_strict_fderiv_at_exp_zero_of_radius_pos` : `exp 𝕂 𝔸` has strict Fréchet-derivative
-  `1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero
-  (see also `has_strict_deriv_at_exp_zero_of_radius_pos` for the case `𝔸 = 𝕂`)
 - `exp_add_of_commute_of_lt_radius` : if `𝕂` has characteristic zero, then given two commuting
   elements `x` and `y` in the disk of convergence, we have
   `exp 𝕂 𝔸 (x+y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y)`
 - `exp_add_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative, then given two
   elements `x` and `y` in the disk of convergence, we have
   `exp 𝕂 𝔸 (x+y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y)`
-- `has_strict_fderiv_at_exp_of_lt_radius` : if `𝕂` has characteristic zero and `𝔸` is commutative,
-  then given a point `x` in the disk of convergence, `exp 𝕂 𝔸` as strict Fréchet-derivative
-  `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case
-  `𝔸 = 𝕂`)
 
 ### `𝕂 = ℝ` or `𝕂 = ℂ`
 
 - `exp_series_radius_eq_top` : the `formal_multilinear_series` defining `exp 𝕂 𝔸` has infinite
   radius of convergence
-- `has_strict_fderiv_at_exp_zero` : `exp 𝕂 𝔸` has strict Fréchet-derivative `1 : 𝔸 →L[𝕂] 𝔸` at zero
-  (see also `has_strict_deriv_at_exp_zero` for the case `𝔸 = 𝕂`)
 - `exp_add_of_commute` : given two commuting elements `x` and `y`, we have
   `exp 𝕂 𝔸 (x+y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y)`
 - `exp_add` : if `𝔸` is commutative, then we have `exp 𝕂 𝔸 (x+y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y)`
   for any `x` and `y`
-- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂 𝔸` as strict
-  Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the
-  case `𝔸 = 𝕂`)
 
 ### Other useful compatibility results
 
 - `exp_eq_exp` : if `𝔸` is a normed algebra over two fields `𝕂` and `𝕂'`, then `exp 𝕂 𝔸 = exp 𝕂' 𝔸`
-- `complex.exp_eq_exp_ℂ_ℂ` : `complex.exp = exp ℂ ℂ`
-- `real.exp_eq_exp_ℝ_ℝ` : `real.exp = exp ℝ ℝ`
 
 -/
 
@@ -203,23 +188,6 @@ begin
     exact (has_fpower_series_on_ball_exp_of_radius_pos h).analytic_at_of_mem hx }
 end
 
-/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has strict Fréchet-derivative
-`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
-lemma has_strict_fderiv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
-begin
-  convert (has_fpower_series_at_exp_zero_of_radius_pos h).has_strict_fderiv_at,
-  ext x,
-  change x = exp_series 𝕂 𝔸 1 (λ _, x),
-  simp [exp_series_apply_eq]
-end
-
-/-- The exponential in a Banach-algebra `𝔸` over a normed field `𝕂` has Fréchet-derivative
-`1 : 𝔸 →L[𝕂] 𝔸` at zero, as long as it converges on a neighborhood of zero. -/
-lemma has_fderiv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝔸).radius) :
-  has_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
-(has_strict_fderiv_at_exp_zero_of_radius_pos h).has_fderiv_at
-
 /-- In a Banach-algebra `𝔸` over a normed field `𝕂` of characteristic zero, if `x` and `y` are
 in the disk of convergence and commute, then `exp 𝕂 𝔸 (x + y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y)`. -/
 lemma exp_add_of_commute_of_mem_ball [char_zero 𝕂]
@@ -256,78 +224,13 @@ lemma exp_add_of_mem_ball [char_zero 𝕂] {x y : 𝔸}
   exp 𝕂 𝔸 (x + y) = (exp 𝕂 𝔸 x) * (exp 𝕂 𝔸 y) :=
 exp_add_of_commute_of_mem_ball (commute.all x y) hx hy
 
-/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of
-characteristic zero has Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in the
-disk of convergence. -/
-lemma has_fderiv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
-begin
-  have hpos : 0 < (exp_series 𝕂 𝔸).radius := (zero_le _).trans_lt hx,
-  rw has_fderiv_at_iff_is_o_nhds_zero,
-  suffices : (λ h, exp 𝕂 𝔸 x * (exp 𝕂 𝔸 (0 + h) - exp 𝕂 𝔸 0 - continuous_linear_map.id 𝕂 𝔸 h))
-    =ᶠ[𝓝 0] (λ h, exp 𝕂 𝔸 (x + h) - exp 𝕂 𝔸 x - exp 𝕂 𝔸 x • continuous_linear_map.id 𝕂 𝔸 h),
-  { refine (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _),
-    rw ← has_fderiv_at_iff_is_o_nhds_zero,
-    exact has_fderiv_at_exp_zero_of_radius_pos hpos },
-  have : ∀ᶠ h in 𝓝 (0 : 𝔸), h ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius :=
-    emetric.ball_mem_nhds _ hpos,
-  filter_upwards [this],
-  intros h hh,
-  rw [exp_add_of_mem_ball hx hh, exp_zero, zero_add, continuous_linear_map.id_apply, smul_eq_mul],
-  ring
-end
-
-/-- The exponential map in a commutative Banach-algebra `𝔸` over a normed field `𝕂` of
-characteristic zero has strict Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x` in
-the disk of convergence. -/
-lemma has_strict_fderiv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝔸}
-  (hx : x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
-let ⟨p, hp⟩ := analytic_at_exp_of_mem_ball x hx in
-hp.has_fderiv_at.unique (has_fderiv_at_exp_of_mem_ball hx) ▸ hp.has_strict_fderiv_at
-
 end any_field_comm_algebra
 
-section deriv
-
-variables {𝕂 : Type*} [nondiscrete_normed_field 𝕂] [complete_space 𝕂]
-
-/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
-`exp 𝕂 𝕂 x` at any point `x` in the disk of convergence. -/
-lemma has_strict_deriv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝕂}
-  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
-by simpa using (has_strict_fderiv_at_exp_of_mem_ball hx).has_strict_deriv_at
-
-/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
-`exp 𝕂 𝕂 x` at any point `x` in the disk of convergence. -/
-lemma has_deriv_at_exp_of_mem_ball [char_zero 𝕂] {x : 𝕂}
-  (hx : x ∈ emetric.ball (0 : 𝕂) (exp_series 𝕂 𝕂).radius) :
-  has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
-(has_strict_deriv_at_exp_of_mem_ball hx).has_deriv_at
-
-/-- The exponential map in a complete normed field `𝕂` of characteristic zero has strict derivative
-`1` at zero, as long as it converges on a neighborhood of zero. -/
-lemma has_strict_deriv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝕂).radius) :
-  has_strict_deriv_at (exp 𝕂 𝕂) 1 0 :=
-(has_strict_fderiv_at_exp_zero_of_radius_pos h).has_strict_deriv_at
-
-/-- The exponential map in a complete normed field `𝕂` of characteristic zero has derivative
-`1` at zero, as long as it converges on a neighborhood of zero. -/
-lemma has_deriv_at_exp_zero_of_radius_pos (h : 0 < (exp_series 𝕂 𝕂).radius) :
-  has_deriv_at (exp 𝕂 𝕂) 1 0 :=
-(has_strict_deriv_at_exp_zero_of_radius_pos h).has_deriv_at
-
-end deriv
-
 section is_R_or_C
 
 section any_algebra
 
-variables {𝕂 𝔸 : Type*} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸]
-
-variables (𝕂 𝔸)
+variables (𝕂 𝔸 : Type*) [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸]
 
 /-- In a normed algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ`, the series defining the exponential map
 has an infinite radius of convergence. -/
@@ -405,18 +308,6 @@ lemma exp_analytic (x : 𝔸) :
   analytic_at 𝕂 (exp 𝕂 𝔸) x :=
 analytic_at_exp_of_mem_ball x ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict Fréchet-derivative
-`1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
-lemma has_strict_fderiv_at_exp_zero :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
-has_strict_fderiv_at_exp_zero_of_radius_pos (exp_series_radius_pos 𝕂 𝔸)
-
-/-- The exponential in a Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has Fréchet-derivative
-`1 : 𝔸 →L[𝕂] 𝔸` at zero. -/
-lemma has_fderiv_at_exp_zero :
-  has_fderiv_at (exp 𝕂 𝔸) (1 : 𝔸 →L[𝕂] 𝔸) 0 :=
-has_strict_fderiv_at_exp_zero.has_fderiv_at
-
 end complete_algebra
 
 local attribute [instance] char_zero_R_or_C
@@ -443,46 +334,8 @@ lemma exp_add {x y : 𝔸} : exp 𝕂 𝔸 (x + y) = (exp 𝕂 𝔸 x) * (exp 
 exp_add_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
   ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
 
-/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has strict
-Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
-lemma has_strict_fderiv_at_exp {x : 𝔸} :
-  has_strict_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
-has_strict_fderiv_at_exp_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _)
-
-/-- The exponential map in a commutative Banach-algebra `𝔸` over `𝕂 = ℝ` or `𝕂 = ℂ` has
-Fréchet-derivative `exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸` at any point `x`. -/
-lemma has_fderiv_at_exp {x : 𝔸} :
-  has_fderiv_at (exp 𝕂 𝔸) (exp 𝕂 𝔸 x • 1 : 𝔸 →L[𝕂] 𝔸) x :=
-has_strict_fderiv_at_exp.has_fderiv_at
-
 end comm_algebra
 
-section deriv
-
-variables {𝕂 : Type*} [is_R_or_C 𝕂]
-
-local attribute [instance] char_zero_R_or_C
-
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `exp 𝕂 𝕂 x` at any point
-`x`. -/
-lemma has_strict_deriv_at_exp {x : 𝕂} : has_strict_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
-has_strict_deriv_at_exp_of_mem_ball ((exp_series_radius_eq_top 𝕂 𝕂).symm ▸ edist_lt_top _ _)
-
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `exp 𝕂 𝕂 x` at any point `x`. -/
-lemma has_deriv_at_exp {x : 𝕂} : has_deriv_at (exp 𝕂 𝕂) (exp 𝕂 𝕂 x) x :=
-has_strict_deriv_at_exp.has_deriv_at
-
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `1` at zero. -/
-lemma has_strict_deriv_at_exp_zero : has_strict_deriv_at (exp 𝕂 𝕂) 1 0 :=
-has_strict_deriv_at_exp_zero_of_radius_pos (exp_series_radius_pos 𝕂 𝕂)
-
-/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has derivative `1` at zero. -/
-lemma has_deriv_at_exp_zero :
-  has_deriv_at (exp 𝕂 𝕂) 1 0 :=
-has_strict_deriv_at_exp_zero.has_deriv_at
-
-end deriv
-
 end is_R_or_C
 
 section scalar_tower
@@ -509,33 +362,7 @@ begin
   rw exp_series_eq_exp_series 𝕂 𝕂' 𝔸 n x
 end
 
-end scalar_tower
-
-section complex
-
-lemma complex.exp_eq_exp_ℂ_ℂ : complex.exp = exp ℂ ℂ :=
-begin
-  refine funext (λ x, _),
-  rw [complex.exp, exp_eq_tsum_field],
-  exact tendsto_nhds_unique x.exp'.tendsto_limit
-    (exp_series_field_summable x).has_sum.tendsto_sum_nat
-end
-
 lemma exp_ℝ_ℂ_eq_exp_ℂ_ℂ : exp ℝ ℂ = exp ℂ ℂ :=
 exp_eq_exp ℝ ℂ ℂ
 
-end complex
-
-section real
-
-lemma real.exp_eq_exp_ℝ_ℝ : real.exp = exp ℝ ℝ :=
-begin
-  refine funext (λ x, _),
-  rw [real.exp, complex.exp_eq_exp_ℂ_ℂ, ← exp_ℝ_ℂ_eq_exp_ℂ_ℂ, exp_eq_tsum, exp_eq_tsum_field,
-      ← re_to_complex, ← re_clm_apply, re_clm.map_tsum (exp_series_summable' (x : ℂ))],
-  refine tsum_congr (λ n, _),
-  rw [re_clm.map_smul, ← complex.of_real_pow, re_clm_apply, re_to_complex, complex.of_real_re,
-      smul_eq_mul, one_div, mul_comm, div_eq_mul_inv]
-end
-
-end real
+end scalar_tower