Real.exp

Stream: Is there code for X?

[Jeremy Avigad]

Given that the theorem Real.summable_pow_div_factorial is in the library, it was surprising to me that the theorem Real.exp_eq_tsum below was so tricky to prove. Could I have done it without having to deal with NormedSpace.exp?

import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog

#check Real.summable_pow_div_factorial

theorem Real.HasSum_pow_div_factorial (x : ℝ) :
    HasSum (fun n => x^n / ↑n.factorial) (Real.exp x) := by
  rw [Real.exp_eq_exp_ℝ]
  convert NormedSpace.exp_series_hasSum_exp' (x : ℝ) using 1
  field_simp

theorem Real.exp_eq_tsum (x : ℝ) :
    Real.exp x = ∑' (n : ℕ), x^n / ↑n.factorial :=
  HasSum.tsum_eq (Real.HasSum_pow_div_factorial x) |>.symm

BTW, the complex versions go through the same way.

[Eric Wieser]

There's an open issue somewhere about merging the three exps

[Eric Wieser]

But going via NormedSpace.exp feels like the right approach to me

[Jireh Loreaux]

I thought the reason we didn't want to merge them was due to import hierarchy reasons. Am I wrong?

[Eric Wieser]

Maybe, but NormedSpace.exp doesn't actually mention a norm at all, so it could be moved to a much earlier file

[Jireh Loreaux]

Also, there's a much shorter proof since we have the tsum result for NormedSpace.exp:

import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog

theorem Real.exp_eq_tsum (x : ℝ) :
    Real.exp x = ∑' (n : ℕ), x^n / ↑n.factorial := by
  rw [Real.exp_eq_exp_ℝ, NormedSpace.exp_eq_tsum_div]

[Jireh Loreaux]

Found with guessing or @loogle NormedSpace.exp, tsum

[loogle]

:search: NormedSpace.exp_eq_tsum_div, NormedSpace.exp_eq_tsum

[Jeremy Avigad]

Thanks, Eric and Jireh. Even with loogle and leansearch, it took me an embarrassingly long time to figure out how to do it. Once you know that the canonical way to do it is to go through NormedSpace.exp, it's straightforward.

[Ruben Van de Velde]

I'm not entirely sure that it is the canonical way, but there's certainly room for API development

[Jireh Loreaux]

I would consider NormedSpace.exp the canonical way. If Eric is right and we can unify all these without increasing imports much, then we should do that (although I'm not going to do it at the moment).

[Jireh Loreaux]

If we can, then we can also drop the stupid namespace :laughing: