Zulip Chat Archive

Stream: maths

Topic: Exponential Banach Algebra


view this post on Zulip Anatole Dedecker (Apr 19 2021 at 13:00):

I was searching for interesting things to do in Lean, and I thought about defining the general exponential function in a Banach Algebra. How hard do you think it would be to use this definition to replace complex.exp and real.exp ? I mean, this would obviously involve refactoring big chunks of proofs, but do you think the formal_multilinear_series is mature enough for this definition ? If not, should I still work on the general definition, PR it, and add a "TODO : merge" somewhere, or is it better to wait and do both at once ?

Related question : I see that my use case (exponential of bounded linear maps) is mentionned in the docstring of analysis.analytic.basic. Is anyone working on that already ?


Last updated: Jun 17 2021 at 17:28 UTC