exponential in banach algebras

Stream: general

[Anatole Dedecker]

Hello everyone ! I recently opened #8576 wich defines exponential in a Banach algebra. As written in the PR description, it is not completely ready for review, but I wanted to open the PR anyway because I'd like to get as many opinions as possibles on my code as soon as possible. I also have a few specific questions about design decisions :

• Explicit parameters : currently, both the field and the algebra are explicit parameters. I think the field has to be explicit anyway because it can't be inferred and a type can be a normed algebra over two distinct fields. But the algebra could be inferred 1) when the function is applied 2) by explicitely giving the type of the function. In my opinion it's more readable if it is explicit, because I feel like exp ℝ reads as "real exponential", not "the exponential in an arbitrary Banach $\R$-algebra", so having exp ℝ ℝ and exp ℝ 𝔸 is better to me, but I'd like your opinion on that.
• Normal form for "in the disc of convergence" : if the base field is not $\R$ or $\mathbb{C}$, the exponential map is not well-defined everywhere (p-adics are a counterexample). So I have multiple lemmas requiring for some variable to be in the disc of convergence, and I don't know if I should write it as ↑∥x∥₊ < (exp_series 𝕂 𝔸).radius or x ∈ emetric.ball (0 : 𝔸) (exp_series 𝕂 𝔸).radius. Currently I just use whatever is more convenient in the proof but that's a bad heuristic, so I'd like your opinion on that too.
• Future of complex.exp and real.exp : In the PR, I prove that this general definition agrees with complex.exp and real.exp. The question is : should the new definition replace the old ones ? That is, do we want anyone using real.exp to import a whole chunk of the analysis and topology library of mathlib ? In my opinion this is not a big problem since in most cases you want to use the derivative of exp anyway so you end up importing analysis, but I'm not experienced enough to take this decision.

Thanks in advance !

[Patrick Massot]

About the last question, I would get rid of real.exp and complex.exp, especially their ugly proofs of differentiability. But I guess @Mario Carneiro has a different opinion.

[Mario Carneiro]

I don't mind having a less ugly proof of differentiability, but the definition of real.exp should not depend on a "huge chunk of analysis", which I'm sure is even larger than the huge chunk of topology that originally motivated the redefinition of real

[Patrick Massot]

We could keep declaration of real.exp, especially since exp ℝ ℝ is indeed a bit bad to read, but reproving all its properties from the general theory.

[Patrick Massot]

I still miss the good old days when real numbers were defined properly.

[Mario Carneiro]

having a proof of equivalence seems fine to me, and will help with all the advanced material

[Mario Carneiro]

the real numbers are defined properly, the way they are in the textbooks

[Mario Carneiro]

they just aren't defined in neo-Bourbaki style

[Patrick Massot]

I'm sure we would understand the performance issues now, and have fast real numbers properly defined.

[Patrick Massot]

That's not how they are defined in good textbooks.

[Patrick Massot]

And our definition wasn't neo-Bourbaki, it was good old Bourbaki.

[Notification Bot]

Anatole Dedecker has marked this topic as resolved.

[Notification Bot]

Anatole Dedecker has marked this topic as unresolved.

[Yury G. Kudryashov]

What's wrong with having (relatively) large dependencies for real/exp/whatever? Especially if it reduces the total amount of LOC we need to maintain.

[Yury G. Kudryashov]

I understand that before CI it was a problem.

[Scott Morrison]

I don't think there's a huge problem. But CI is still an issue (we have some ad-hoc runners helping the CI queue, while we get more online), and the total compilation time is still a huge pain when refactoring anything low level. Having to wait several hours between rounds of changes is not efficient.

[Scott Morrison]

But I agree reducing compile time can't come at the arbitrary expense of good library design.

[Yury G. Kudryashov]

It's not clear that changing the definition of exp to something based on the general exponential function will increase the total compile time.

[Yury G. Kudryashov]

(and yes, I think that analytic functions should be used in more places)

[Eric Wieser]

Perhaps I'm missing something mathematically; but what's the benefit of defining docs#exp over an arbitrary base ring 𝕂 vs just using ℚ?

Is docs#exp_series meaningful today in the absence of docs#char_zero? It looks to me like it ends up truncating the terms that would be a divide by zero, which doesn't seem particularly useful.

[Yury G. Kudryashov]

docs#padic.char_zero

[Yury G. Kudryashov]

AFAIR, @Kevin Buzzard asked to define it over any field.

[Damiano Testa]

I'm certainly in favour of a general field. Whether assuming char_zero or not, it depends. It might be fun if some identities also work without the assumption...

[Kevin Buzzard]

I need it over the p-adic numbers which are characteristic 0. I don't have any use for it in char p

[Eric Wieser]

Whether the identities work or not without char_zero; is it reasonable to define $exp(x) = 1 + x + \frac{x^2}{2}$ in characteristic 3? Because that's what we do right now, and it seems like nonsense to me, because the terms we're removing aren't zero in real life, they're undefined.

[Eric Wieser]

(regarding my rat suggestion, perhaps I'm under the false impression that every char_zero normed algebra over a field must also be a normed algebra over the rationals)

[Johan Commelin]

I guess that in char p > 0 the correct thing is to use something like https://en.wikipedia.org/wiki/Divided_power_structure

[Kevin Buzzard]

I agree that 1+x+x^2/2 is not a useful function in char 3 (or at least not useful to me). Note that Johan's suggestion involves a lot of extra structure on a ring, basically you're saying "give me a whole bunch of elements $c_n(x)$ satisfying axioms which are satisfied by $x^n/n!$ and then just add the $c_n(x)$ up instead" (in fact we don't add them up, we do other things with them, but that's another story). If the ring is a $\mathbb{Q}$-algebra then there are unique choices for the $c_n(x)$, but in char p there can be others. Note that you don't attempt to define these when $x=1$, you do it only for "small" $x$ (all $x$ in an ideal).

[Kevin Buzzard]

However let me stress that the usual exponential and logarithm play a useful role much earlier on in the $p$-adic theory (the story of when things converge is different, but the basic ideas are the same).

[Eric Wieser]

I'm not even claiming that 1+x+x^2 in characteristic 3 isn't a useful function, just that it's not deserving of the name exp

[Kevin Buzzard]

People aren't going to use exp in char 3 so maybe it doesn't matter what it's called?

[Yaël Dillies]

Eric Wieser said:

I'm not even claiming that 1+x+x^2 in characteristic 3 isn't a useful function, just that it's not deserving of the name exp

1 + x - x^2, you mean?

[Eric Wieser]

I'm advocating for putting [char_zero 𝕂] on the definition (even though it would be unused), as a clear indication than the name only makes sense in that situation

[Eric Wieser]

And then my follow up question is "if I do that, is there any A for which 𝕂 = ℚ isn't a valid choice?"

[Kevin Buzzard]

What is A here? We'll need it for Q-algebras with a notion of convergence.

[Eric Wieser]

docs#exp

[Eric Wieser]

𝔸 is the algebra in which we're computing the exponential

[Eric Wieser]

𝕂 is some nonsense argument that doesn't actually matter, see docs#exp_eq_exp

[Yaël Dillies]

Won't you then have to carry normed_space ℚ 𝔸 everywhere? I'm hitting something similar in #13379 where I could prove stuff about normed_space ℚ E but if you do you will need to assume that all your real normed spaces are also rational normed spaces (unless I missed an instance?)

[Eric Wieser]

I'm currently trying to work out if this is true:

instance normed_algebra_rat {𝕜} [normed_division_ring 𝕜] [char_zero 𝕜] : normed_algebra ℚ 𝕜 :=

[Kevin Buzzard]

given that a normed field is not a normed ring which is a field (because the conventions on norms are different for rings and fields) I think it's only wise to check these things carefully!

[Eric Wieser]

I can't seem to prove it, likely because it's not true

[Eric Wieser]

Fundamentally it seems I need some typeclass that says that the norm preserves casts of rationals / naturals / integers

[Yaël Dillies]

Many many lemmas under analysis.convex. need such a typeclass.

[Eric Wieser]

I think "preserves cast of nat" probably implies all the rest?

[Eric Wieser]

Is there a more mathematical notion for this?

[Yaël Dillies]

I did manage to prove a few results that were a bit surprising in that direction. Let me dig out...

[Eric Wieser]

(some examples: docs#pi.normed_space satisfies such a typeclass, docs#euclidean_space does not)

[Reid Barton]

Eric Wieser said:

I'm currently trying to work out if this is true:

instance normed_algebra_rat {𝕜} [normed_division_ring 𝕜] [char_zero 𝕜] : normed_algebra ℚ 𝕜 :=

Unless I'm confused, the p-adics are a counterexample.

[Yaël Dillies]

Yaël Dillies said:

Many many lemmas under analysis.convex. need such a typeclass.

The stereotypical example is docs#convex_on_norm

[Kevin Buzzard]

docs#normed_algebra

[Yaël Dillies]

Oh wait, it already exists?!

[Eric Wieser]

Reid, docs#padic_norm_e.norm_int_le_one does seem to confirm you're correct

[Kevin Buzzard]

normed_algebra ℚ 𝕜 needs normed_field ℚ -- is there an instance of this? Number theorists have lots of norms that they want to put on the rationals.

[Reid Barton]

Yes, the real one docs#rat.normed_field

[Yaël Dillies]

@Anatole Dedecker, turns out docs#normed_algebra is what we wanted all along.

[Reid Barton]

Over the reals, I take it?

[Yaël Dillies]

We wanted to state lemmas more generally than for ℝ.

[Eric Wieser]

Yael, it sounds like you're talking about something different to what I was asking about

[Yaël Dillies]

I believe it's related, because the answer to your question is also an answer to mine.

[Eric Wieser]

#13384 is the strongest instance I was able to prove

[Anatole Dedecker]

Just wanted to comment since I'm the author of the exp files. Indeed the case of a field with nonzero characteristic is a bit stupid. I must admit that I didn't have a lot of other examples in mind than real and complex at the time, I barely knew about p-adics, so I was really over-generalizing without thinking much about it :sweat_smile:

[Anatole Dedecker]

Yaël Dillies said:

Anatole Dedecker, turns out docs#normed_algebra is what we wanted all along.

Oh is it ? I have to find what was the problem again :sweat_smile: (Since it seems not to be clear, Yael is talking about related problem we faced while trying to generalize the base field)

[Eric Wieser]

(the base field of exp or the base field of normed_algebra?)

[Anatole Dedecker]

The base field for convexity, it is not related to exponential

[Anatole Dedecker]

I still think we should definitely be able to make everything an exponential over the rational though, and it connects with something that has been talked about before : we should remove the dependence on the norm in the definition of exp, so that we can have an exponential for matrices that is completely independent of the norm that the user wants to put on its matrices. Of course all the theorems related to the convergence radius, or differentiability, will depend on a norm, but it may allow us to reserve the normed_algebra hypothesis for cases where it is really needed.

[Anatole Dedecker]

I'm not completely sure, but I even think that docs#exp_series_radius_eq_top could be done with just the assumption that we indeed have a normed algebra over Q

[Yaël Dillies]

The problem was that ∥a • x + b • y∥ is not necessarily a • ∥x∥, so we couldn't turn convex combinations within the norm to convex combinations outside the norm.

[Eric Wieser]

From @Heather Macbeth's comment on #13384, I realize the answer is probably "yes, it suffices to only provide exp if a normed ℚ-algebra structure is available on A, but different choices of the ring A might need a different normed_field structure on ℚ to the one that's currently canonical (docs#rat.normed_field)"

[Scott Morrison]

Which means we want don't want to specialize to Q, so users can provide a type synonym carrying an alternative normed_field structure?

[Riccardo Brasca]

Even if I really like p-adic norms, I think docs#rat.normed_field is a reasonable instance. We can use type synonyms for p-adic norms on Q.

[Riccardo Brasca]

I didn't see Scott's answer :grinning:

[Kevin Buzzard]

Eric: That sounds right to me. The power series for the exponential function converges for x=p^2 if Q has the p-adic norm as does the power series for log(1+x). One proof that exp and log define inverse bijections between a small disc in Qp centre 0 and a small disc centre 1 is "it's true for the reals because of calculus, so the formal power series must be inverse of each other so it works for the p-adics too"

[Kevin Buzzard]

I'm not sure I care about norms on Q, I don't think I want to use exp and log on Q, only on Qp

[Eric Wieser]

Kevin, you realize that I'm talking about exp ℚ A : A → A, right? Would you call this "exp on ℚ" or "exp on A"?

[Eric Wieser]

Regarding making the exponential work over matrices without picking a norm, #13426 takes a step towards this goal

[Anatole Dedecker]

Oh indeed, thanks !

[Eric Wieser]

I've a branch elsewhere that does the rest, which I'll rebase once that is merged

[Eric Wieser]

After that change we can obviously just remove 𝕂 from the definition (in favor of using ℚ internally), as the definition doesn't depend on its normed or even topological space structure any more

[Eric Wieser]

(the requirements are now just [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] [has_continuous_const_smul 𝕂 𝔸])

[Kevin Buzzard]

I'm sorry to cause all this trouble just from this claim (which I've never followed up on) that "number theorists use p-adic log I promise"..

[Eric Wieser]

Following up on claims like that is what your students are for, right? ;)

[Eric Wieser]

I'm confused again about @Kevin Buzzard's p-adic norm speculations; I was able to show that for any two normed algebras over different fields, (exp_series 𝕂 𝔸).radius = (exp_series 𝕂' 𝔸).radius; so it seems there would be no motivation for putting a different norm on $\mathbb{Q}$ anyway.

[Eric Wieser]

Either that, or the existing lemmas stated in terms of docs#formal_multilinear_series.radius are of no use in the p-adic case as they require too strong a sense of convergence

[Eric Wieser]

Either way, it increasingly seems like there's no point even mentioning any other field in the lemmas

[Eric Wieser]

(My original plan was to leave 𝕂 in the lemmas but not the definitions, but that creates a lot of annoyance for... nothing?)

[Kevin Buzzard]

The formal exponential power series $\sum x^n/n!$ converges in a p-adic field iff $|x|< |p|^{1/(p-1)}$ and in particular the answer depends on $p$.

[Eric Wieser]

Is a padic field a normed algebra over Q? My guess is that it must not be

[Eric Wieser]

Because if it were, then I have a proof that it converges everywhere

[Kevin Buzzard]

When you say Q do you mean "Q with some fixed norm on it that isn't the p-adic norm"?

[Eric Wieser]

Any norm

[Kevin Buzzard]

docs#normed_algebra

[Eric Wieser]

See my comment above about the radius of convergence being equal for all choices of field (...that satisfy docs#nondiscrete_normed_field and normed_algebra)

[Kevin Buzzard]

There is [normed_field k] in that definition, which says to me the incorrect (in number theory) statement "there's only one norm on the rationals"

[Eric Wieser]

Sure, but that's not important here

[Eric Wieser]

Let's say you can pick a type synonym number_theory_rat and put whatever norm you like on it

[Eric Wieser]

My claim is that no matter what you do, it won't satisfy that typeclass

[Kevin Buzzard]

I can't see any problem with making Qp into a normed algebra over Q

[Eric Wieser]

Is Qp a docs#complete_space?

[Riccardo Brasca]

Qp seems a normed algebra

[Riccardo Brasca]

Yes, it is complete, as metric space

[Kevin Buzzard]

The norm of n! is not n! in the p-adic case. Does this help?

[Kevin Buzzard]

Any integer has norm at most 1

[Riccardo Brasca]

Eric Wieser said:

I'm confused again about Kevin Buzzard's p-adic norm speculations; I was able to show that for any two normed algebras over different fields, (exp_series 𝕂 𝔸).radius = (exp_series 𝕂' 𝔸).radius; so it seems there would be no motivation for putting a different norm on $\mathbb{Q}$ anyway.

But here we are changing 𝔸, aren't we?

[Eric Wieser]

Sure, but I think I also have a proof that (exp_series ℚ A).radius = ⊤ for one particular choice of norm on Q, and any A

[Eric Wieser]

I'll check if I had any unexpected typeclasses that I haven't mentioned here

[Riccardo Brasca]

But this depends on the particular norm, right? Qp is a normed algebra over Q with the p-adic norm

[Eric Wieser]

Ah thanks, you've made me realize my confusion. The escape is "there is no normed_algebra Q Qp instance possible using the default norm on Q"

[Kevin Buzzard]

I can certainly believe that. If you're doing p-adic stuff then the norm on Q coming from the map Q -> R and the usual norm on R plays no role

[Kevin Buzzard]

Fields like R and Qp are compete with respect to one canonical norm, but Q lives in all of these and gets a different norm from each inclusion

[Kevin Buzzard]

Same goes for Z

[Eric Wieser]

(deleted)