Real.exp

Stream: mathlib4

[Scott Morrison]

Have a look at this:

import Mathlib

open Real

#time example (x : ℝ) : 0 < exp x      := exp_pos _ -- 250ms
#time example (x : ℝ) : 0 < Real.exp x := exp_pos _ -- 2ms

[Scott Morrison]

Even with open Real, Lean tries _root_.exp first, and tries to coerce x : ℝ to a type.
This typeclass search goes haywire, and takes a long time to fail.

[Scott Morrison]

This definitely needs fixing.

[Scott Morrison]

I think the correct solution is just to namespace docs#exp. Suggestions?

[Scott Morrison]

(Ah, this is the same as https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Crazy.20unification.20quests)

[Scott Morrison]

NormedSpace.exp? TopologicalRing.exp? formalExp? banachExp?

[Eric Wieser]

Ideally we just merge them, but maybe we need your suggestion as a short-term fix

[Scott Morrison]

I think people are still going to want to be able to write Real.exp x rather than exp \bbR x.

[Scott Morrison]

But yes, I think we should fix this first.

[Scott Morrison]

I think my preferred solution is just the namespace the entire file either NormedSpace or Analysis.NormedSpace.

[Scott Morrison]

(This might be considered as setting a good example. :-)

[Scott Morrison]

(Although I guess the good example would be namespacing it Mathlib.Analysis.NormedSpace. :-)

[Eric Wieser]

Scott Morrison said:

I think people are still going to want to be able to write Real.exp x rather than exp \bbR x.

Yes, part of the task of merging them is to remove the (hopefully?) useless argument!

[Eric Wieser]

NormedSpace feels like a bit of a lie, since some results don't require a norm at all; but maybe that's no worse than "module" being a semimodule or docs#Ring.inverse working on monoids with zero

[Scott Morrison]

/poll How should we rename _root_.exp?

[Scott Morrison]

I'd like to fix this, as currently with import Mathlib and open Real, exp is pretty much unusable.

[Scott Morrison]

(My intention, if we move this into a namespace, is that all the lemmas about it in the same file will move to the same namespace.)

[Eric Wieser]

Note that we already have a workaround, which is to use the rexp notation

[Scott Morrison]

Yes, but that requires special knowledge, and there's no way to deliver it to someone who writes import Mathlib open Lean, and then observes that Lean doesn't work. :-)

[Scott Morrison]

(An alternative solution would be to protect Real.exp??)

[Eric Wieser]

I don't think we need both rexp notation and unprotected Real.exp, but I think that's more of an argument for removing the notation.

[Jireh Loreaux]

I'll just say that I would really prefer not to namespace the current docs#exp, but as yet I don't have an alternative solution to propose. Protecting docs#Real.exp is not my favorite idea either.

[Scott Morrison]

I'm hesitant to get derailed onto long-term solutions, because I would like a short-term fix first.

Nevertheless, I appreciate Jireh's unhappiness about this, so:

1. Could we change Lean's name resolution so it tries the "deeper-namespaced" alternatives first?
2. Could we change Lean's name resolution so it doesn't even try _root_.X if Y.X is available and Y is open?
3. Could we remove Real.exp and Complex.exp entirely, in favour of the current _root_.exp?
4. Could we decide we want to namespace everything, and then NormedSpace.exp would not feel so lonely?

I think 1. and 2. sound fragile and complicated and unlikely to win the relevant hearts and minds. :-)

Number 4. sounds great to me, but that is a battle for another day!

Number 3. may well work, but someone would need to do the work in Mathlib. I'm actually a bit confused why there is the field argument of _root_.exp in the first place. Couldn't we just fix K = Q? Do we say anything interesting about exp outside of that situation?

[Eric Wieser]

I think your list got mangled. Fixed!

[Eric Wieser]

The K=Q thing always comes around to p-adics (we have at least one thread about this)

[Eric Wieser]

I think the answer is that the definitions don't need K, but most of the lemmas do

[Eric Wieser]

It would help a lot of someone could write some basic results for exp on p-adics so that they can act as a sanity check for any refactors!

[Kevin Buzzard]

A toy API would be that if p is prime and q=4 if p=2 and q=p otherwise, then exp and log are inverse group isomorphisms between (qZ_p,+) and (1+qZ_p,*). The correct API would be that if K is a nonarchimedean local field of characteristic zero then there are neighborhoods of 0 and 1 for which the same holds.

[Eric Wieser]

Unfortunately we don't have log yet so that looks a bit out of reach

[Scott Morrison]

Isn't it still K=Q for the p-adics, though?

[Kevin Buzzard]

The source is $q\Z_p$. I'm not sure I understand the question.

[Eric Wieser]

No, it's K = WithADifferentNorm ℚ

[Scott Morrison]

(Sorry, Kevin, wasn't responding to your post.)

[Eric Wieser]

But like I said earlier, that only matters in the lemmas, since the def doesn't even need the topology on K, let alone the norm

[Scott Morrison]

I see, so we could plausibly remove K as an argument for exp itself, and just use the non-normed rationals there.

[Kevin Buzzard]

(note that the power series defining exp doesn't converge in general over the p-adics)

[Scott Morrison]

And then lemmas would refer to a possibly-non-standard norm on the rationals? Or a type synonym for the rationals? That sounds a bit icky.

[Eric Wieser]

Scott Morrison said:

I see, so we could plausibly remove K as an argument for exp itself, and just use the non-normed rationals there.

Yes, and I think I had a branch for this in mathlib3, but it was rather annoying having to write ℚ explicitly in all the lemmas

[Eric Wieser]

Here's the previous thread

[Eric Wieser]

The branches was https://github.com/leanprover-community/mathlib/compare/eric-wieser/exp-rat, where https://github.com/leanprover-community/mathlib/compare/eric-wieser/exp-rat...eric-wieser/exp-very-rat added one more commit that probably breaks the p-adics

[Eric Wieser]

I created !3#19244 which is a bit easier to comment on

[Eric Wieser]

Ported in #8370

[Johan Commelin]

@Kevin Buzzard You are saying that you want to define exp and log on spaces that are not $\mathbb{Q}$-vector spaces, right? Or is there another claim that you make which I'm missing?

[Eric Wieser]

My understanding was that Kevin is still only interested in Q-algebras, but wants to consider normed Q-algebras where the norm on ℚ is not the one induced through the reals

[Kevin Buzzard]

yeah I have no idea why we have put the real norm on Q. For me Q has no canonical norm. It's R which has the norm.

[Eric Wieser]

I think #8370 preserves the capability to work with that norm structure, but drops the ability to work with stupid rings where 1/n! = 0

[Eric Rodriguez]

Eric Wieser said:

I think #8370 preserves the capability to work with that norm structure, but drops the ability to work with stupid rings where 1/n! = 0

isn't this all char-p rings?

[Eric Wieser]

Yes, but is exp (defined via the power series) meaningful in those? 1/n! = 0 is a junk value; in normal mathematics you'd just declare the whole thing undefined, right?

[Eric Wieser]

I guess exp x would still be defined in a char-p ring if x^p = 0

[Johan Commelin]

I guess https://en.wikipedia.org/wiki/Divided_power_structure might be relevant

[Eric Wieser]

The fact that it talks about a divided power structure "on $I$" doesn't bode well; it sounds like that's going to result in another undesirable signature for exp

[Johan Commelin]

Yeah, I don't think we should have this in our type signature for exp

[Eric Wieser]

I guess we could have a typeclass for the special case where I = top

[Eric Wieser]

But at the end of the day, we'd just be replacing Algebra Rat A in #8370 with TopDividedPower A, which could always come in a later refactor

[Johan Commelin]

Kevin Buzzard said:

A toy API would be that if p is prime and q=4 if p=2 and q=p otherwise, then exp and log are inverse group isomorphisms between (qZ_p,+) and (1+qZ_p,*). The correct API would be that if K is a nonarchimedean local field of characteristic zero then there are neighborhoods of 0 and 1 for which the same holds.

(note that the power series defining exp doesn't converge in general over the p-adics)

So the main question is: do we want to capture examples like this? Or should this just be a different function.

[Eric Wieser]

Can we write that example as a mwe?

[Eric Wieser]

It's not clear to me that even the current docs#exp supports it, in which case removing the K argument doesn't make things worse

[Johan Commelin]

I think that's right.

[Johan Commelin]

Hmm, atm docs#Real.exp is defined in terms of docs#Complex.exp which is not defined in terms of docs#exp. So if we refactor docs#exp by removing the K, what does that buy us again?

[Eric Wieser]

We can then eliminate Real.exp and Complex.exp entirely

[Johan Commelin]

Shouldn't we first refactor those two, so that they are defined in terms of _root_.exp?

[Scott Morrison]

It does seem better to do that first, before changing the signature of _root_.exp.

[Eric Wieser]

I think we could do things in either order

[Eric Wieser]

I filed #8372 as the task of merging them

[Scott Morrison]

I think the plan is

• someone (me?) is going to move _root_.exp to NormedSpace.exp
• perhaps the discussion at example (p : P) : Q := p means the original problem goes away at some point anyway.
• later, someone refactors Real.exp in terms of NormedSpace.exp
• either before or after, someone changes the signature of NormedSpace.exp.

[Johan Commelin]

Sounds good to me.

[Eric Wieser]

Do we ultimately move NormedSpace.exp back to _root_.exp?

[Johan Commelin]

And once we have rings with canonical divided power structures, we can refactor exp so that it also works for Z_p

[Johan Commelin]

I think Real.exp and Complex.exp can be removed, at the end of all those refactors

[Jireh Loreaux]

There is one perhaps significant issue about removing Real.exp and Complex.exp in favor of implementations using docs#exp: it screws with the import hierarchy. Right now, these are defined in Data.Complex.Exponential, whose imports are only

Mathlib.Algebra.GeomSum
Mathlib.Data.Complex.Basic
Mathlib.Data.Nat.Choose.Sum

But docs#exp needs:

Mathlib.Analysis.Analytic.Basic
Mathlib.Analysis.Complex.Basic
Mathlib.Data.Finset.NoncommProd
Mathlib.Topology.Algebra.Algebra
Mathlib.Analysis.Normed.Field.InfiniteSum
Mathlib.Data.Nat.Choose.Cast

[Jireh Loreaux]

And by "screws with the import hierarchy" I mean that we have to define Real.exp and Complex.exp much later. We may view this as problematic if we want outside users to be using bits of Mathlib.

[Eric Wieser]

I think docs#exp could use much less for the definition

[Jireh Loreaux]

fair enough

[Heather Macbeth]

Jireh Loreaux said:

There is one perhaps significant issue about removing Real.exp and Complex.exp in favor of implementations using docs#exp: it screws with the import hierarchy. Right now, these are defined in Data.Complex.Exponential

And note that Bochner integration depends on rpow which depends on Real.exp.

[Johan Commelin]

/-
Copyright (c) 2023 Johan Commelin. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Johan Commelin
-/
import Mathlib.Algebra.Algebra.Basic
import Mathlib.Algebra.BigOperators.NatAntidiagonal
import Mathlib.Data.Nat.Choose.Multinomial
import Mathlib.RingTheory.Ideal.Basic
import Mathlib.Tactic.FieldSimp

universe u

open BigOperators

variable {A : Type u} [Semiring A]

/-- C_{n, m} = \frac{(mn)!}{(m!)^n n!} -/
def divpowC (m n : ℕ) : ℕ :=
  (m*n).factorial / (m.factorial ^n * n.factorial)

/--
Let `A` be a commutative semiring with an ideal `I`.
A *divided power structure* (or *PD-structure*, after the French "puissances divisées") on `I`
is a collection of maps `γ n : A → A` for `n : ℕ` such that:

* `γ 0 x = 1` and `γ 1 x = x` for `x ∈ I`, while `γ n x ∈ I` for `n > 0`.
* `γ n (x + y) = ∑_{i+j=n} (γ i x) * (γ j y)` for `x, y ∈ I`.
* `γ n (λ • x) = λ^n • γ n x` for `λ : A, x ∈ I`.
* `(γ m x) * (γ n x) = ((m, n)) • γ (m+n) x` for `x ∈ I`, where `((m, n)) = \frac{(m+n)!}{m! n!}` is an integer.
* `γ n (γ m x) = C_{n, m} • γ (m * n) x` for `x ∈ I` and `m > 0`,
  where `C_{n, m} = divpowC m n = \frac{(mn)!}{(m!)^n n!}` is an integer.
-/
structure DividedPowerStructure (I : Ideal A) where
  divpow : A → ℕ → A
  divpow_zero : ∀ {x}, x ∈ I → divpow x 0 = 1
  divpow_add : ∀ {x y}, x ∈ I → y ∈ I → ∀ n,
    divpow (x+y) n = ∑ p in Finset.antidiagonal n, divpow x p.1 * divpow y p.2
  divpow_smul : ∀ a : A, ∀ {x}, x ∈ I → ∀ n, divpow (a • x) n = a^n * divpow x n
  divpow_mul_divpow : ∀ {x}, x ∈ I → ∀ m n,
    divpow x m * divpow x n = (m + n).choose m • divpow x (m+n)
  divpow_divpow : ∀ {x}, x ∈ I → ∀ m n, m > 0 →
    divpow (divpow x m) n = divpowC m n • divpow x (m*n)
  divpow_of_not_mem : ∀ {x}, x ∉ I → ∀ n, divpow x n = 0

class DivPow (α : Type u) where
  divpow : α → ℕ → α

-- TODO: this notation is ambiguous, what are good alternatives?
notation x"^["n"]" => DivPow.divpow x n

class DividedPowerRing (A : Type u) [Semiring A] (I : outParam $ Ideal A)
  extends DividedPowerStructure I

instance (A : Type u) [Semiring A] (I : Ideal A) [h : DividedPowerRing A I] : DivPow A :=
  ⟨h.divpow⟩

/-- Every `ℚ`-algebra is a divided power ring -/
instance (A : Type u) [CommRing A] [Algebra ℚ A] : DividedPowerRing A ⊤ where
  divpow x n := (n.factorial : ℚ)⁻¹ • x ^ n
  divpow_zero {x} hx := by simp only [Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, one_smul]
  divpow_add {x} {y} hx hy n := by
    have : ∀ n : ℕ, (n.factorial : ℚ) ≠ 0 := fun n ↦ Nat.cast_ne_zero.mpr n.factorial_ne_zero
    apply smul_right_injective _ (this n)
    dsimp only
    rw [smul_inv_smul₀ (this n), (Commute.all _ _).add_pow', Finset.smul_sum]
    apply Finset.sum_congr rfl
    simp only [Finset.mem_antidiagonal, nsmul_eq_mul, Algebra.mul_smul_comm, Algebra.smul_mul_assoc,
      Prod.forall]
    simp only [← mul_smul]
    rintro a b rfl
    rw [← Nat.add_choose_mul_factorial_mul_factorial]
    push_cast
    simp only [mul_assoc, mul_inv_cancel_left₀ (this _)]
    rw [← nsmul_eq_mul, nsmul_eq_smul_cast ℚ, Nat.choose_symm_add]
    field_simp
  divpow_smul a {x} hx n := by simp [mul_pow]
  divpow_mul_divpow {x} hx m n := by
    rw [nsmul_eq_smul_cast ℚ]
    dsimp only
    simp only [Algebra.mul_smul_comm, Algebra.smul_mul_assoc, Finset.mem_singleton, ne_eq, pow_add,
     ← mul_smul]
    congr 1
    have : ∀ n : ℕ, (n.factorial : ℚ) ≠ 0 := fun n ↦ Nat.cast_ne_zero.mpr n.factorial_ne_zero
    field_simp
    norm_cast
    rw [← mul_assoc, add_comm, Nat.add_choose_mul_factorial_mul_factorial]
  divpow_divpow {x} hx m n hm := by
    dsimp only [divpowC]
    simp only [Algebra.smul_def, mul_pow, pow_mul]
    simp only [← Algebra.smul_def, ← map_pow, map_natCast, nsmul_eq_smul_cast ℚ, ← mul_smul]
    congr 1
    have : ∀ n : ℕ, (n.factorial : ℚ) ≠ 0 := fun n ↦ Nat.cast_ne_zero.mpr n.factorial_ne_zero
    field_simp
    sorry
  divpow_of_not_mem {x} hx := False.elim (hx <| Submodule.mem_top)

-- TODO: define `DividedPowerRing` on `ℤₚ`

[Johan Commelin]

Here's a start on divided power rings. One sorry left, but I really need to start grading exams again.

[Kevin Buzzard]

Aren't @Antoine Chambert-Loir and @María Inés de Frutos Fernández working on this?

[Eric Wieser]

Interestingly https://stacks.math.columbia.edu/tag/07GL defines them as maps from I to I, but somehow assumes that 1 is in I

[Kevin Buzzard]

de Jong can't be assuming $1$ is in $I$, because then $I$ would be $R$ and we definitely want cases where $I$ isn't $R$. Do you mean $\gamma_0(x)=1$? It's only $\gamma_n$ for $n>0$ which land in $I$.

[Adam Topaz]

Yeah $\gamma_0$ is defined just as a convenience

[Antoine Chambert-Loir]

Kevin Buzzard said:

A toy API would be that if p is prime and q=4 if p=2 and q=p otherwise, then exp and log are inverse group isomorphisms between (qZ_p,+) and (1+qZ_p,*). The correct API would be that if K is a nonarchimedean local field of characteristic zero then there are neighborhoods of 0 and 1 for which the same holds.

and even the explicit neighborhood on which that holds…

[Antoine Chambert-Loir]

Kevin Buzzard said:

Aren't Antoine Chambert-Loir and María Inés de Frutos Fernández working on this?

Yes, @María Inés de Frutos Fernández and I wrote a lot of stuff on divided power structures. This is accessible at https://github.com/AntoineChambert-Loir/DividedPowers4

[Kevin Buzzard]

Accessible to you maybe :-) Is the repo private?

[Antoine Chambert-Loir]

It seems so… I don't think it hurts making it public.

[Antoine Chambert-Loir]

Adam Topaz said:

Yeah $\gamma_0$ is defined just as a convenience

It's actually important to define it in this way, so that the binomial formula holds neatly (without binomial coefficients).

[Johan Commelin]

Aah, I didn't mean to duplicate efforts! Thanks for posting that repo!

[Kevin Buzzard]

You've got a fair way to go before you catch up Johan :-)

[Yaël Dillies]

Johan Commelin said:

Here's a start on divided power rings. One sorry left, but I really need to start grading exams again.

I think grading rings would be much more useful to the mathlib community. :upside_down:

[Eric Wieser]

Hey, I already graded rings!

[Eric Wieser]

(though if anyone fancies grading a PR that grades more rings, there's #7394 ...)

[Mario Carneiro]

Jireh Loreaux said:

There is one perhaps significant issue about removing Real.exp and Complex.exp in favor of implementations using docs#exp: it screws with the import hierarchy. Right now, these are defined in Data.Complex.Exponential, whose imports are only

Mathlib.Algebra.GeomSum
Mathlib.Data.Complex.Basic
Mathlib.Data.Nat.Choose.Sum

But docs#exp needs:

Mathlib.Analysis.Analytic.Basic
Mathlib.Analysis.Complex.Basic
Mathlib.Data.Finset.NoncommProd
Mathlib.Topology.Algebra.Algebra
Mathlib.Analysis.Normed.Field.InfiniteSum
Mathlib.Data.Nat.Choose.Cast

I am very much against a change that involves this kind of huge import creep. This kind of thing is making it impossible to break mathlib into useful subsets.

[Eric Wieser]

This is a straw man argument, exp can be defined with tsum alone

[Mario Carneiro]

If there is a way to do it without the imports, great

[Eric Wieser]

All those other files are to prove results about it, but we can evaluate those on a case-by-case basis

[Mario Carneiro]

but I consider that a prerequisite to any such refactor

[Eric Wieser]

Ah, I guess tsum is still a heavier import than taking the limit of a cauchy series

[Mario Carneiro]

I would actually like to have Real.exp without even topological spaces, unsure where it is sitting now

[Mario Carneiro]

apparently it used to not be a dependency but it has since been introduced via Mathlib.Data.Real.Sqrt

[Mario Carneiro]

not sure why square roots are a dependency of exp though

[Mario Carneiro]

oh Real.Sqrt is a dependency of Complex.Basic, so this is one of those transitive faux dependencies It's used directly, square roots define abs which is part of the cauchy structure on complexes used in the exp proof

[Yury G. Kudryashov]

What's wrong with topological spaces? (I would redefine reals using generic UniformSpace completion but I remember that you weren't happy about this possible refactor)

[Yury G. Kudryashov]

We can definitely avoid talking about analytic functions near the definition of exp.

[Scott Morrison]

#8436 chore: exp -> NormedSpace.exp

[Eric Wieser]

I've rebased my #8370 which removes the 𝕂 argument from NormedSpace.exp

[Yury G. Kudryashov]

Github hides discussions by default, so let's ask @Kevin Buzzard here: are you OK with this refactor? The new definition will work for p-adic numbers, since they're a Rat-algebra.

[Yury G. Kudryashov]

We may have an issue with algebras over p-adic numbers that don't have a global Rat-algebra instance though.

[Yury G. Kudryashov]

I guess, you'll need to add a (local) instance from p-adic algebra to Rat-algebra with semi-outparam p (and make sure that it doesn't create diamonds by redefining qsmul on p-adics, if needed).

[Jireh Loreaux]

I'm not a fan of the need for Algebra ℚ A instances in various places now. I'm not necessarily trying to veto, but I think this is quite unpleasant.

[Yury G. Kudryashov]

Should we add [Algebra Real A] : Algebra Rat A?

[Yury G. Kudryashov]

Another option is to leave NormedSpace.exp as is but add

• Real.exp that works for real algebras, including Complex;
• Padic.exp that works for algebras over Padic (BTW, should it be PAdic?)

[Kevin Buzzard]

I'm fine about the removal of the explicit K but I wonder if there's a better way to do Algebra Q A.

[Eric Wieser]

Yury G. Kudryashov said:

Should we add [Algebra Real A] : Algebra Rat A?

This will probably create instance diamonds

[Eric Wieser]

Yury G. Kudryashov said:

We may have an issue with algebras over p-adic numbers that don't have a global Rat-algebra instance though.

I think in practice we should have these instances anyway

[Eric Wieser]

The annoyance is more the abstract case where we have to add mathematically "redundant" assumptions, which I assume is what Jireh dislikes here

[Yury G. Kudryashov]

Eric Wieser said:

Yury G. Kudryashov said:

We may have an issue with algebras over p-adic numbers that don't have a global Rat-algebra instance though.

I think in practice we should have these instances anyway

Which instances are you talking about?

[Yury G. Kudryashov]

We have [SMul Complex K] : SMul Real K without diamonds. Can we have the same for Real -> Rat and Padic -> Rat?

[Yury G. Kudryashov]

Then [Algebra Rat A] would be a reasonable assumption.

[Eric Wieser]

Yury G. Kudryashov said:

We have [SMul Complex K] : SMul Real K without diamonds.

I don't think this is true in general. We have a hack that just about works for the cases we care about, but already falls apart as soon as we introduce right actions

[Eric Wieser]

Yury G. Kudryashov said:

Which instances are you talking about?

I meant

instance : Algebra Rat SomeConcreteAlgebraOverAPadicNumber

[Scott Carnahan]

If we want a function that allows for real exponentials with few imports, but also exponentials for more general rings, would it be worthwhile to make a custom class for defining exponentials? For example:

import Mathlib.Algebra.Order.CauSeq.BigOperators
import Mathlib.Analysis.Normed.Ring.Basic

open Finset Nat CauSeq Finset IsAbsoluteValue

/-- A class that allows us to define exponential functions without division. -/
class CauchyDividedPower (A : Type*) [NormedRing A] where
  /-- A divided power function -/
  dpow : ℕ → A → A
  /-- A submonoid where divided powers give a Cauchy sequence. -/
  support : AddSubmonoid A
  dpow_null : ∀ {n x} (_ : x ∉ support), dpow n x = 0
  dpow_zero : ∀ {x} (_ : x ∈ support), dpow 0 x = 1
  dpow_one : ∀ {x} (_ : x ∈ support), dpow 1 x = x
  dpow_add : ∀ {n} {x y} (_ : x ∈ support) (_ : y ∈ support) (_ : x * y = y * x),
    dpow n (x + y) = Finset.sum (range (n + 1)) fun k ↦ dpow k x * dpow (n - k) y
  mul_dpow : ∀ {m n} {x} (_ : x ∈ support),
    dpow m x * dpow n x = choose (m + n) m • dpow (m + n) x
  cauchy : ∀ x, IsCauSeq (‖·‖) fun n => ∑ m ∈ range n, ‖dpow m x‖

namespace CauchyDividedPower

variable {A : Type*} [NormedRing A]

/-- The Cauchy sequence defining the exponential. -/
def exp' [IsAbsoluteValue (R := A) (‖·‖)] [CauchyDividedPower A] (x : A) : CauSeq A (‖·‖) :=
  ⟨fun n => ∑ m ∈ range n, dpow m x, (cauchy x).of_abv⟩

/-- The exponential function. -/
noncomputable def exp [IsAbsoluteValue (R := A) (‖·‖)] [CauSeq.IsComplete A (‖·‖)]
    [CauchyDividedPower A] (x : A) : A :=
  CauSeq.lim (exp' x)

end CauchyDividedPower

The usual results exp_zero and exp_add more or less follow the standard arguments.

[Antoine Chambert-Loir]

For a related notion, see docs#DividedPowers

[Antoine Chambert-Loir]

We have an exponential, as docs#DividedPowers.exp, valued in docs#PowerSeries, but this would be exp (a • X), rather than exp a.

[Yury G. Kudryashov]

Usage of DividedPowers or similar typeclass won't solve the problem mentioned by @Jireh Loreaux

[Johan Commelin]

How about a notation typeclass for exp, and then a typeclass LawfulExp (todo: better name) that has things like exp (x + y) = exp x * exp y (and maybe something about continuity???). And then instances of LawfulExp coming from various places like Scott's Cauchy divided powers, and the algebraic divided powers that Antoine and Maria-Ines have worked on.
And then the reals could slot in however they want. Possibly by just providing low-level proofs.

[Jireh Loreaux]

Then you have to ensure defeq of the function? That doesn't seem different. (e.g., you still have to unify NormedSpace.exp and Real.exp). And it's still not clear how you are avoiding the Algebra Q A instances.

Maybe I'm missing something crucial?

[Johan Commelin]

I'm quickly reaching the end of my comfort zone now, but couldn't NormedAlgebra (or whatever) then extend this LawfulExp? And then the instance for Real takes care of the defeq by forgetful inheritance.

[Johan Commelin]

But maybe I'm overengineering, or just missing a simple mathematical obstacle.

[Jireh Loreaux]

The problem is that an \R-algebra is not a \Q-algebra (via an instance), and so NormedAlgebra couldn't have an Exp or LawfulExp instance (because it wouldn't know how to find the field parameter).

[Yury G. Kudryashov]

Also, you have exp (x + y) = exp x * exp y only if x and y commute, and over some fields they also have to be small enough, because exp has a finite radius of convergence.

[Yury G. Kudryashov]

So, there is no one-size-fits-all LawfulExp.

[Johan Commelin]

Good point. I retract my suggestion (-;

[Yury G. Kudryashov]

I think that we should start creating webpages for design decisions like this one, where different approaches with pros and cons are listed.

[Yury G. Kudryashov]

Should we do it in gh wiki, in issues, or somewhere else?

[Bryan Gin-ge Chen]

I agree we should explicitly document more of our design decisions, but maybe as comments in the code / library notes depending on how important / how much there is to say?

[Yury G. Kudryashov]

I suggest to do some of this when we're discussing decisions, so that people can read a relatively short document instead of a long Zulip+github thread.

[Yury G. Kudryashov]

Once the decision is made, parts of this can be copy+pasted (with edits) to the relevant module docstrings / library notes etc.

[Bryan Gin-ge Chen]

Ah, I see. Yes, in that case maybe a mathlib4 wiki page is lowest friction. With an issue there's the possibility that discussion gets spread out.

[Yury G. Kudryashov]

I've created https://github.com/leanprover-community/mathlib4/wiki/RFC-Exp-function

[Yury G. Kudryashov]

Feel free to expand it.

[Jireh Loreaux]

I've added a small bit about keeping imports to Real.exp small.

[Yuyang Zhao]

Does the actual definition of Algebra Rat A matter here? Can we use some Prop-valued classes or even junk values?

[Eric Wieser]

We need the $\mathbb{Q}$-action (or divided power structure) on A to write $\frac{1}{n}x^n$, which is data however you spin it

[Eric Wieser]

SMul ℚ A would suffice but is not any less annoying than Algebra ℚ A

[Yuyang Zhao]

We might obtain the data using Classical.choice here.

[Yuyang Zhao]

I'll try it later today.

[Yuyang Zhao]

branch#exp_rat_junkvalue

[Yury G. Kudryashov]

@Eric Wieser What's wrong with using Classical.choice to get data inside an irreducible definition (note: I've missed the message above and suggested something similar on github)? You get a definition that works for any field. Of course, you need K to prove any lemma, but this isn't worse than the current situation.

[Yury G. Kudryashov]

More precisely, I suggest that we

• leave expSeries as is;
• redefine exp so that it calls expSeries if Algebra Rat A is nonempty.

This way we can argue about partial sums of the series (and compute them, if needed) and have exp that works for any ring with topology.

[Yury G. Kudryashov]

If we want to drop [CharZero K] assumptions in the very basic lemmas, then the definition of exp can take the route I described on github (if \exists (K : Type) (_ : DivisionRing K), Nonempty (Module K A)) instead.