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