Zulip Chat Archive

Stream: maths

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 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) (Mar 16 2023 at 14:35):

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

Anatole Dedecker (Mar 16 2023 at 14:40):

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

rtertr (Sonia) (Mar 16 2023 at 14:41):

Ah, great! Thank you!

Eric Wieser (Mar 16 2023 at 15:10):

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

Alistair Tucker (Mar 16 2023 at 15:15):

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 (Mar 16 2023 at 15:15):

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

Eric Wieser (Mar 16 2023 at 15:15):

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

rtertr (Sonia) (Mar 16 2023 at 15:16):

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 (Mar 16 2023 at 15:16):

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 (Mar 16 2023 at 15:17):

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

rtertr (Sonia) (Mar 16 2023 at 15:18):

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

Eric Wieser (Mar 16 2023 at 15:19):

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) (Mar 16 2023 at 15:26):

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 (Mar 16 2023 at 15:27):

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

Eric Wieser (Mar 16 2023 at 15:28):

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

Eric Wieser (Mar 16 2023 at 15:29):

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

rtertr (Sonia) (Mar 16 2023 at 15:36):

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 (Mar 16 2023 at 15:36):

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

rtertr (Sonia) (Mar 16 2023 at 15:40):

Okay, great, thank you!

rtertr (Sonia) (Mar 16 2023 at 15:42):

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

Eric Wieser (Mar 16 2023 at 15:44):

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

Eric Wieser (Mar 16 2023 at 15:44):

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

rtertr (Sonia) (Mar 16 2023 at 15:46):

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

rtertr (Sonia) (Mar 16 2023 at 15:50):

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 (Mar 16 2023 at 15:51):

normed_algebra = normed_space + algebra

Anatole Dedecker (Mar 16 2023 at 16:00):

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 (Mar 16 2023 at 16:00):

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

Eric Wieser (Mar 16 2023 at 16:01):

Although admittedly the lemmas need many more dependencies

Eric Wieser (Mar 16 2023 at 16:02):

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 (Mar 16 2023 at 16:05):

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 (Mar 16 2023 at 16:06):

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

Eric Wieser (Mar 16 2023 at 16:06):

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 (Mar 16 2023 at 16:06):

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

Notification Bot (Mar 17 2023 at 21:12):

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


Last updated: Dec 20 2023 at 11:08 UTC