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

[eric-wieser]

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

---

[eric-wieser]

@ADedecker said

I have a last question, did you check whether 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.

I'm pretty sure it can be, and now they're in the same file. My only hesitation is that it feels like I should be deducing them in the other direction!

[ADedecker]

@ADedecker said

I have a last question, did you check whether 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.

I'm pretty sure it can be, and now they're in the same file. My only hesitation is that it feels like I should be deducing them in the other direction!

That's precisely why the algebra.adjoin approach feels morally better! I guess it's not that bad if you see u ↦ u • x as some kind of inclusion map, but that's probably a bit far-fetched.

I think it's completely fine to leave it as is, but I'll leave a comment along the lines of:

We can't deduce this from `has_fderiv_at_exp_of_lt_radius` because we don't assume that `𝔹` is commutative.
We could actually go the other way around and deduce `has_fderiv_at_exp_of_lt_radius` from this,
but this would be a bit over-engineered so we just do both proofs separately.

[ADedecker]

I'll have a closer look tomorrow, feel free to ping me on Zulip if I forget, it would be nice to stay ahead of the porting tide.

[eric-wieser]

I attempted the adjoin version as follows:

instance subalgebra.normed_algebra' {R' : Type*} {R : Type*} {A : Type*} [comm_ring R]
  [semi_normed_ring A]
  [algebra R A] (S : subalgebra R A) [normed_field R'] [algebra R' R]
  [normed_algebra R' A] [is_scalar_tower R' R A] : normed_algebra R' ↥S :=
@normed_algebra.induced _ R' S A _ (subring_class.to_ring S) S.algebra' _ _ _
  (S.val.restrict_scalars R')

instance elemental_algebra.normed_comm_ring (R) {A} [comm_ring R] [normed_ring A] [algebra R A] (a : A):
  normed_comm_ring (algebra.elemental_algebra R a) :=
{ ..algebra.elemental_algebra.comm_ring,
  ..subalgebra.normed_ring  (algebra.elemental_algebra R a) }

instance elemental_algebra.is_closed (R) {A} [comm_ring R] [ring A] [algebra R A]
  [uniform_space A] [topological_ring A] [complete_space A] (a : A):
  complete_space (algebra.elemental_algebra R a) :=
is_closed.complete_space_coe $ subalgebra.is_closed_topological_closure _

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
  let 𝔹' := (algebra.elemental_algebra 𝔸 x),
  letI : normed_comm_ring 𝔹' := elemental_algebra.normed_comm_ring 𝔸 x,
  letI : normed_algebra 𝕂 𝔹' := subalgebra.normed_algebra' _,
  letI : is_closed ↑𝔹' := subalgebra.is_closed_topological_closure _,
  let x' : 𝔹' := t • ⟨x, algebra.self_mem_elemental_algebra _ _⟩,
  let s := (exp_series 𝕂 𝔹'),
  have hx' : x' ∈ emetric.ball (0 : 𝔹') (exp_series 𝕂 𝔹').radius,
  { rw [mem_emetric_ball_zero_iff] at htx ⊢,
    refine htx.trans_le _,
    let coeL : 𝔹' →L[𝕂] 𝔹 := (𝔹'.to_submodule.subtypeL : _).restrict_scalars 𝕂,
    have := (exp_series 𝕂 𝔹').radius_le_radius_continuous_linear_map_comp coeL,
    sorry },
  have := has_fderiv_at_exp_of_mem_ball hx',
  sorry
end

I don't know if the first sorry is true. The second one probably is, but looks annoying.

[eric-wieser]

It would be nice to stay ahead of the porting tide.

I've opted for leaving a TODO comment about the alternative proof strategy above, so as to not fall too far behind. A reasonable number of the things we'd need for the subalgebra proof are missing.

[ADedecker]

A reasonable number of the things we'd need for the subalgebra proof are missing.

I was expecting that. Thanks for giving it a try anyway!

[eric-wieser]

I think it's completely fine to leave it as is, but I'll leave a comment along the lines of:

Is the existing comment sufficient, or do you want something more prominent? Feel free to suggest something in the diff.

[ADedecker]

Thanks!

maintainer merge

[github-actions]

🚀 Pull request has been placed on the maintainer queue by ADedecker.

[dupuisf]

Thanks!

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

• Build mathlib
• Lint mathlib
• Lint style
• Run tests