feat(analysis/special_functions/exponential): derivative of `u ↦ exp …

…𝕂 (u • x)` (#19062)

Revived from an old branch of @ADedecker, golfed using new lemmas that I added in the meantime.

src/analysis/special_functions/exponential.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2021 Anatole Dedecker. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Anatole Dedecker
+Authors: Anatole Dedecker, Eric Wieser
 -/
 import analysis.normed_space.exponential
 import analysis.calculus.fderiv_analytic
@@ -24,17 +24,24 @@ We prove most result for an arbitrary field `𝕂`, and then specialize to `𝕂
   `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 `𝔸 = 𝕂`)
 - `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
+  then given a point `x` in the disk of convergence, `exp 𝕂` has strict Fréchet-derivative
   `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp_of_lt_radius` for the case
   `𝔸 = 𝕂`)
+- `has_strict_fderiv_at_exp_smul_const_of_mem_ball`: even when `𝔸` is non-commutative, if we have
+  an intermediate algebra `𝕊` which is commutative, then the function `(u : 𝕊) ↦ exp 𝕂 (u • x)`,
+  still has strict Fréchet-derivative `exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x` at `t` if
+  `t • x` is in the radius of convergence.
 
 ### `𝕂 = ℝ` or `𝕂 = ℂ`
 
 - `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 `𝔸 = 𝕂`)
-- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` as strict
+- `has_strict_fderiv_at_exp` : if `𝔸` is commutative, then given any point `x`, `exp 𝕂` has strict
   Fréchet-derivative `exp 𝕂 x • 1 : 𝔸 →L[𝕂] 𝔸` at x (see also `has_strict_deriv_at_exp` for the
   case `𝔸 = 𝕂`)
+- `has_strict_fderiv_at_exp_smul_const`: even when `𝔸` is non-commutative, if we have
+  an intermediate algebra `𝕊` which is commutative, then the function `(u : 𝕊) ↦ exp 𝕂 (u • x)`
+  still has strict Fréchet-derivative `exp 𝕂 (t • x) • (1 : 𝔸 →L[𝕂] 𝔸).smul_right x` at `t`.
 
 ### Compatibilty with `real.exp` and `complex.exp`
 
@@ -211,3 +218,192 @@ end
 
 lemma real.exp_eq_exp_ℝ : real.exp = exp ℝ :=
 by { ext x, exact_mod_cast congr_fun complex.exp_eq_exp_ℂ x }
+
+/-! ### Derivative of $\exp (ux)$ by $u$
+
+Note that since for `x : 𝔸` we have `normed_ring 𝔸` not `normed_comm_ring 𝔸`, we cannot deduce
+these results from `has_fderiv_at_exp_of_mem_ball` applied to the algebra `𝔸`.
+
+One possible solution for that would be to apply `has_fderiv_at_exp_of_mem_ball` to the
+commutative algebra `algebra.elemental_algebra 𝕊 x`. Unfortunately we don't have all the required
+API, so we leave that to a future refactor (see leanprover-community/mathlib#19062 for discussion).
+
+We could also go the other way around and deduce `has_fderiv_at_exp_of_mem_ball` from
+`has_fderiv_at_exp_smul_const_of_mem_ball` applied to `𝕊 := 𝔸`, `x := (1 : 𝔸)`, and `t := x`.
+However, doing so would make the aformentioned `elemental_algebra` refactor harder, so for now we
+just prove these two lemmas independently.
+
+A last strategy would be to deduce everything from the more general non-commutative case,
+$$\frac{d}{dt}e^{x(t)} = \int_0^1 e^{sx(t)} \left(\frac{d}{dt}e^{x(t)}\right) e^{(1-s)x(t)} ds$$
+but this is harder to prove, and typically is shown by going via these results first.
+
+TODO: prove this result too!
+-/
+
+section exp_smul
+variables {𝕂 𝕊 𝔸 : Type*}
+variables (𝕂)
+
+open_locale topology
+open asymptotics filter
+
+section mem_ball
+variables [nontrivially_normed_field 𝕂] [char_zero 𝕂]
+variables [normed_comm_ring 𝕊] [normed_ring 𝔸]
+variables [normed_space 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸]
+variables [is_scalar_tower 𝕂 𝕊 𝔸]
+variables [complete_space 𝔸]
+
+lemma has_fderiv_at_exp_smul_const_of_mem_ball
+  (x : 𝔸) (t : 𝕊) (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x) t :=
+begin
+  -- TODO: prove this via `has_fderiv_at_exp_of_mem_ball` using the commutative ring
+  -- `algebra.elemental_algebra 𝕊 x`. See leanprover-community/mathlib#19062 for discussion.
+  have hpos : 0 < (exp_series 𝕂 𝔸).radius := (zero_le _).trans_lt htx,
+  rw has_fderiv_at_iff_is_o_nhds_zero,
+  suffices :
+    (λ h, exp 𝕂 (t • x) * (exp 𝕂 ((0 + h) • x) - exp 𝕂 ((0 : 𝕊) • x)
+      - ((1 : 𝕊 →L[𝕂] 𝕊).smul_right x) h))
+    =ᶠ[𝓝 0] (λ h, exp 𝕂 ((t + h) • x) - exp 𝕂 (t • x)
+      - (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x) h),
+  { refine (is_o.const_mul_left _ _).congr' this (eventually_eq.refl _ _),
+    rw ← @has_fderiv_at_iff_is_o_nhds_zero _ _ _ _ _ _ _ _
+      (λ u, exp 𝕂 (u • x)) ((1 : 𝕊 →L[𝕂] 𝕊).smul_right x) 0,
+    have : has_fderiv_at (exp 𝕂) (1 : 𝔸 →L[𝕂] 𝔸) ((1 : 𝕊 →L[𝕂] 𝕊).smul_right x 0),
+    { rw [continuous_linear_map.smul_right_apply, continuous_linear_map.one_apply, zero_smul],
+      exact has_fderiv_at_exp_zero_of_radius_pos hpos },
+    exact this.comp 0 ((1 : 𝕊 →L[𝕂] 𝕊).smul_right x).has_fderiv_at },
+  have : tendsto (λ h : 𝕊, h • x) (𝓝 0) (𝓝 0),
+  { rw ← zero_smul 𝕊 x,
+    exact tendsto_id.smul_const x },
+  have : ∀ᶠ h in 𝓝 (0 : 𝕊), h • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius :=
+    this.eventually (emetric.ball_mem_nhds _ hpos),
+  filter_upwards [this],
+  intros h hh,
+  have : commute (t • x) (h • x) := ((commute.refl x).smul_left t).smul_right h,
+  rw [add_smul t h, exp_add_of_commute_of_mem_ball this htx hh, zero_add, zero_smul, exp_zero,
+      continuous_linear_map.smul_right_apply, continuous_linear_map.one_apply,
+      continuous_linear_map.smul_apply, continuous_linear_map.smul_right_apply,
+      continuous_linear_map.one_apply, smul_eq_mul, mul_sub_left_distrib, mul_sub_left_distrib,
+      mul_one],
+end
+
+lemma has_fderiv_at_exp_smul_const_of_mem_ball'
+  (x : 𝔸) (t : 𝕊) (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (((1 : 𝕊 →L[𝕂] 𝕊).smul_right x).smul_right (exp 𝕂 (t • x))) t :=
+begin
+  convert has_fderiv_at_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1,
+  ext t',
+  show commute (t' • x) (exp 𝕂 (t • x)),
+  exact (((commute.refl x).smul_left t').smul_right t).exp_right 𝕂,
+end
+
+lemma has_strict_fderiv_at_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕊)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_strict_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x) t :=
+let ⟨p, hp⟩ := analytic_at_exp_of_mem_ball (t • x) htx in
+have deriv₁ : has_strict_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x)) _ t,
+  from hp.has_strict_fderiv_at.comp t
+    ((continuous_linear_map.id 𝕂 𝕊).smul_right x).has_strict_fderiv_at,
+have deriv₂ : has_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x)) _ t,
+  from has_fderiv_at_exp_smul_const_of_mem_ball 𝕂 x t htx,
+(deriv₁.has_fderiv_at.unique deriv₂) ▸ deriv₁
+
+lemma has_strict_fderiv_at_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕊)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_strict_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (((1 : 𝕊 →L[𝕂] 𝕊).smul_right x).smul_right (exp 𝕂 (t • x))) t :=
+let ⟨p, hp⟩ := analytic_at_exp_of_mem_ball (t • x) htx in
+begin
+  convert has_strict_fderiv_at_exp_smul_const_of_mem_ball 𝕂 _ _ htx using 1,
+  ext t',
+  show commute (t' • x) (exp 𝕂 (t • x)),
+  exact (((commute.refl x).smul_left t').smul_right t).exp_right 𝕂,
+end
+
+variables {𝕂}
+
+lemma has_strict_deriv_at_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_strict_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
+by simpa using (has_strict_fderiv_at_exp_smul_const_of_mem_ball 𝕂 x t htx).has_strict_deriv_at
+
+lemma has_strict_deriv_at_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_strict_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
+by simpa using (has_strict_fderiv_at_exp_smul_const_of_mem_ball' 𝕂 x t htx).has_strict_deriv_at
+
+lemma has_deriv_at_exp_smul_const_of_mem_ball (x : 𝔸) (t : 𝕂)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
+(has_strict_deriv_at_exp_smul_const_of_mem_ball x t htx).has_deriv_at
+
+lemma has_deriv_at_exp_smul_const_of_mem_ball' (x : 𝔸) (t : 𝕂)
+  (htx : t • x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius) :
+  has_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
+(has_strict_deriv_at_exp_smul_const_of_mem_ball' x t htx).has_deriv_at
+
+end mem_ball
+
+section is_R_or_C
+variables [is_R_or_C 𝕂]
+variables [normed_comm_ring 𝕊] [normed_ring 𝔸]
+variables [normed_algebra 𝕂 𝕊] [normed_algebra 𝕂 𝔸] [algebra 𝕊 𝔸] [has_continuous_smul 𝕊 𝔸]
+variables [is_scalar_tower 𝕂 𝕊 𝔸]
+variables [complete_space 𝔸]
+
+variables (𝕂)
+
+lemma has_fderiv_at_exp_smul_const (x : 𝔸) (t : 𝕊) :
+  has_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x) t :=
+has_fderiv_at_exp_smul_const_of_mem_ball 𝕂 _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_fderiv_at_exp_smul_const' (x : 𝔸) (t : 𝕊) :
+  has_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (((1 : 𝕊 →L[𝕂] 𝕊).smul_right x).smul_right (exp 𝕂 (t • x))) t :=
+has_fderiv_at_exp_smul_const_of_mem_ball' 𝕂 _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_strict_fderiv_at_exp_smul_const (x : 𝔸) (t : 𝕊) :
+  has_strict_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (exp 𝕂 (t • x) • (1 : 𝕊 →L[𝕂] 𝕊).smul_right x) t :=
+has_strict_fderiv_at_exp_smul_const_of_mem_ball 𝕂 _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_strict_fderiv_at_exp_smul_const' (x : 𝔸) (t : 𝕊) :
+  has_strict_fderiv_at (λ u : 𝕊, exp 𝕂 (u • x))
+    (((1 : 𝕊 →L[𝕂] 𝕊).smul_right x).smul_right (exp 𝕂 (t • x))) t :=
+has_strict_fderiv_at_exp_smul_const_of_mem_ball' 𝕂 _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+variables {𝕂}
+
+lemma has_strict_deriv_at_exp_smul_const (x : 𝔸) (t : 𝕂) :
+  has_strict_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
+has_strict_deriv_at_exp_smul_const_of_mem_ball _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_strict_deriv_at_exp_smul_const' (x : 𝔸) (t : 𝕂) :
+  has_strict_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
+has_strict_deriv_at_exp_smul_const_of_mem_ball' _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_deriv_at_exp_smul_const (x : 𝔸) (t : 𝕂) :
+  has_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (exp 𝕂 (t • x) * x) t :=
+has_deriv_at_exp_smul_const_of_mem_ball _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+lemma has_deriv_at_exp_smul_const' (x : 𝔸) (t : 𝕂) :
+  has_deriv_at (λ u : 𝕂, exp 𝕂 (u • x)) (x * exp 𝕂 (t • x)) t :=
+has_deriv_at_exp_smul_const_of_mem_ball' _ _ $
+  (exp_series_radius_eq_top 𝕂 𝔸).symm ▸ edist_lt_top _ _
+
+end is_R_or_C
+
+end exp_smul