RFC Exp function

Status quo

We have three definitions:

• Real.exp : ℝ → ℝ
• Complex.exp : ℂ → ℂ
• NormedSpace.exp (𝕂 : Type*) {A : Type*} [...] [Algebra 𝕂 A] : A → A

The first 2 definitions work for specific types, the last one generalizes both but takes an extra argument K which is used to compute ((n ! : ℕ) : 𝕂)⁻¹ • x ^ n.

Goals

We want to merge these three definitions into one (leanprover-community/mathlib4#8372). The new definition must work at least for Banach algebras over rational, real, complex, and p-adic numbers.

We also want to avoid increasing (or preferably even reduce) the imports necessary for Real.exp.

Approaches

Fix 𝕂 = ℚ in the definition

We can require that our ring is an algebra over rational numbers. We do not require that this is a normed algebra, so the definition works for algebras over p-adic numbers.

The main downside of this approach is that we don't have instances deducing [Algebra ℚ A] from [Algebra ℝ A] or [Algebra ℚ_[p] A]. So, with this approach we have a choice

• either add these instances, opening another door for non-defeq instance diamonds;
• or require users to explicitly assume [Algebra ℚ A] to work with exp.

Split on the base field

We can leave NormedSpace.exp as is, but merge Real.exp with Complex.exp into a new definition Real.exp that works for any Banach algebra over real numbers. Algebras over p-adics can use NormedSpace.exp directly.

Use DividedPowers

... or a similar typeclass/structure. This approach has the same downsides as fixing the base field to be rational numbers. In addition, using DividedPowers specifically add unnecessary imports to the definition of Real.exp.

References

• Zulip thread
• Github issue
• Github PR