Topic: Exponential Banach Algebra
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
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