feat(analysis/calculus/fderiv/exp): derivative of exp ℝ (A x) in non-commutative rings

[eric-wieser]

This follows the proof on Physics.SE that shows

$$\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$$

There are significant stumbling blocks in the way of proving this, sadly.

---

• depends on: [Merged by Bors] - feat(analysis/special_functions/exponential): derivative of u ↦ exp 𝕂 (u • x) #19062

[eric-wieser]

@ADedecker; do you know if your existing results in nalysis.special_functions.exponential are strong enough to prove this?

[ADedecker]

Ah, I know about this issue. Indeed we don't have what is required to prove them right now, but that shouldn't be too much trouble. I had started to work on something like that bout two years ago (you can have a look at the very old branch more_exponential), and I think at least the statement should be saved:

lemma has_fderiv_at_exp_smul_const_of_mem_ball [char_zero 𝕂] {𝔸' : Type*} [normed_comm_ring 𝔸']
  [normed_algebra 𝕂 𝔸'] [algebra 𝔸' 𝔸] [has_continuous_smul 𝔸' 𝔸] [is_scalar_tower 𝕂 𝔸' 𝔸]
  (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 :=

(of course you can get rid of the radius hypothesis with is_R_or_C)

At the time I wasn't aware of algebra.adjoin so I made this the main lemma and made has_fderiv_at_exp_of_mem_ball a consequence (at least I wanted to, IIRC this caused some troubles), but maybe a more sensible approach would be to (1) prove that exp behaves well under continuous algebra morphisms and (2) consider the closure of the subalgebra algebra.adjoin 𝔸' x (which is complete and commutative), apply has_fderiv_at_exp_of_mem_ball and then (1).

I can have a go at either reviving my old proof or trying the new one if you want.

[eric-wieser]

I was able to revive your old proof with minimal modification. The primed version now follows trivially from the unprimed one.

Is there any advantage to switching to your proposed strategy?

[eric-wieser]

(1) prove that exp behaves well under continuous algebra morphisms

I proved this a while ago, it's map_exp.

[ADedecker]

I was able to revive your old proof with minimal modification. The primed version now follows trivially from the unprimed one.

Thanks a lot!

Is there any advantage to switching to your proposed strategy?

Not really, but with a bit more mathematical maturity than I had two years ago the second approach feels more natural, and this is definitely what we would do on paper. But I think it would be a bit painful in Lean, and we definitely lack some API (for example I can't find the fact that algebra.adjoin is commutative under the obvious hypotheses). So since this one's working I'd say sticking to it is the best solution.

I have a last question, did you check wether has_fderiv_at_exp_of_mem_ball could be made a consequence of this version? If you prefer not to change previous files because of the port that's fine of course, but it would be nice to at least give it a try.

[eric-wieser]

I've extracted all these results to #19062

[ghost]

This PR/issue depends on:

• [Merged by Bors] - feat(analysis/special_functions/exponential): derivative of u ↦ exp 𝕂 (u • x) #19062
  By Dependent Issues (🤖). Happy coding!