Exponential Banach Algebra

Stream: maths

[Anatole Dedecker]

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 ?

[rtertr (Sonia)]

Hi @Anatole Dedecker
Did you ever work further with this?
Kind regards,
Sonia

[Anatole Dedecker]

Yes, this is in mathlib now! See docs#exp

[rtertr (Sonia)]

Ah, great! Thank you!

[Eric Wieser]

Note that we still have docs#exp, docs#real.exp, docs#complex.exp, and docs#power_series.exp

[Alistair Tucker]

Anatole Dedecker said:

... to use this definition to replace complex.exp and real.exp...

I guess that hasn't happened exactly. Might it?

[Eric Wieser]

There was still some annoyance about what to do with the extra field argument consumed by exp

[Eric Wieser]

I think we concluded it was probably ok to just hard-code it to rat, but there were some complications

[rtertr (Sonia)]

If I want to generalize schwartz_map (fin d -> ℝ) ℂ to the form schwartz_map (Bananch_space) ℂ, what would the notation for the Bananch space be? :)

[Eric Wieser]

I think https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/exponential.20in.20banach.20algebras/near/248773988 is the thread that has more info

[Eric Wieser]

It would be A, where you write variables {A} [normed_ring A] [normed_algebra ℝ A] [complete_space A] I believe

[rtertr (Sonia)]

Ah great, thank you :D Why would it be [normed_algebra ℝ A] with the real?

[Eric Wieser]

Mainly because I'm trying to keep things easy for you. Strictly speaking you could write {𝕂 : Type u_1} {𝔸 : Type u_2} [is_R_or_C 𝕂] [normed_ring 𝔸] [normed_algebra 𝕂 𝔸] [complete_space 𝔸] but the extra generality is illusory since every complex normed algebra is also a real normed algebra

[rtertr (Sonia)]

when I try to add it I get the error 'invalid variable binder type update, 'A' is not a variable'.

import analysis.schwartz_space
import analysis.normed_space.exponential
import tactic

section

noncomputable theory

namespace new

variables {A} [normed_ring A] [normed_algebra ℝ A] [complete_space A]

def gaussian_complex  {d:ℕ } {a:ℂ} (ha:0<a.re): schwartz_map A ℂ :=
  { to_fun := λ x : (A), exp (-a * ‖x‖^2),
    smooth' :=
    begin
      sorry,
    end,
    decay' :=
    begin
      sorry,
    end}

end new

[Eric Wieser]

That error is asking you to write {A : Type*}

[Eric Wieser]

It sounds like you actually need normed_algebra ℂ A though if you want to be able to multiply by a complex number

[Eric Wieser]

Note that you're not actually use the exp in A there; you're applying it to a complex number still

[rtertr (Sonia)]

If I replace exp with complex.exp, then it is okay with it, but would it then defeat the purpose? I guess already taking the norm makes it go from A |--> ℝ and I won't need the Banach exponential?

import analysis.schwartz_space
import analysis.normed_space.exponential
import tactic
import data.complex.exponential

section

noncomputable theory

namespace new

open complex

variables {A : Type*} [normed_ring A] [normed_algebra ℝ A] [complete_space A]

def gaussian_complex {a:ℂ} (ha:0<a.re): schwartz_map A ℂ :=
  { to_fun := λ x : (A), complex.exp (-a * ‖x‖^2),
    smooth' :=
    begin
      sorry,
    end,
    decay' :=
    begin
      sorry,
    end}

end new

[Eric Wieser]

Yes, there's no point switching from docs#complex.exp to docs#exp if you're still going to exponentiate complex numbers

[rtertr (Sonia)]

Okay, great, thank you!

[rtertr (Sonia)]

And why does Lean have [normed_ring A] [normed_algebra ℝ A] and not a notation for normed vector space?

[Eric Wieser]

You need a multiplication to take the exponential, which is why docs#exp_add_of_commute uses that

[Eric Wieser]

If you just need a normed (real) vector space write [normed_add_comm_group A] [normed_space ℝ A]

[rtertr (Sonia)]

ah, okay, so I guess since I go to the complex exponential, then I can just stay with the last option?

[rtertr (Sonia)]

What is the difference between [normed_algebra ℝ A] and [normed_space ℝ A]? They both have norm_smul_le, but one has to_module and the other one to_algebra? :)

[Eric Wieser]

normed_algebra = normed_space + algebra

[Anatole Dedecker]

Alistair Tucker said:

Anatole Dedecker said:

... to use this definition to replace complex.exp and real.exp...

I guess that hasn't happened exactly. Might it?

The main reason, on top of what Eric said, is that we want docs#real.exp to be quite elementary, whereas docs#exp has a ton of dependencies. This is also why docs#real is not defined using docs#uniform_space.completion

[Eric Wieser]

(𝕂 : Type u_1) {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) doesn't feel like many dependencies to me

[Eric Wieser]

Although admittedly the lemmas need many more dependencies

[Eric Wieser]

Eric Wieser said:

There was still some annoyance about what to do with the extra field argument consumed by exp

It seems I had two abandoned branches where I tried this, branch#eric-wieser/exp-rat and branch#eric-wieser/exp-very-rat

[Anatole Dedecker]

Eric Wieser said:

(𝕂 : Type u_1) {𝔸 : Type u_2} [field 𝕂] [ring 𝔸] [algebra 𝕂 𝔸] [topological_space 𝔸] [topological_ring 𝔸] (x : 𝔸) doesn't feel like many dependencies to me

I meant dependencies in the sense of the import tree : the operator norm for multilinear maps is quite a heavy import

[Eric Wieser]

The operator norm is only needed for the lemmas though, right?

[Eric Wieser]

We could define exp somewhere low down, prove all the properties about it for real the current way, then do the heavy operator norm stuff later

[Eric Wieser]

Having redundant special cases of proofs seems slightly less bad than having redundant special cases of definitions

[Notification Bot]

17 messages were moved from this topic to #new members > Typeclasses for Banach Algebra by Eric Wieser.