Multiple dimension

Stream: Is there code for X?

[rtertr (Sonia)]

Good evening everyone,
This is a relatively simple question, I think.
So I have been working on showing

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

Now I wish to show the same thing for lean schwartz_map ℝ^d ℂ. Just not quite sure how to proceed since
Lean very much dislikes lean {d:ℕ } {a:ℂ} (ha:0<a.re): schwartz_map ℝ^d ℂ , thus I was thinking there must be some notation for lean ℝ^d somewhere.

[Eric Wieser]

ℝ^d is usually either fin d -> ℝ, or if you need the euclidean norm structure, docs#euclidean_space

[Eric Wieser]

(note that you can't use `lean some_lean_code` to highlight inline lean code, just use `some_lean_code` )

[rtertr (Sonia)]

Do you mean in the big or small lines of code? :D

[Alex J. Best]

For the small ones, but lean is set as the default for big ones anyway, so thats not really needed either

[Eric Wieser]

What's the to_fun that you want for $ℝ^d$? Is it the sum of the squares of the components?

[Eric Wieser]

Because if so, I think you'd do better to define this on an arbitrary normed_algebra ℝ A (or weaker) and replace x ^ 2 with the norm of x squared.

[rtertr (Sonia)]

So, I am trying to do some work on fourier transform on ℝ ^d. I wanted to started with the multiple-dimensional Gaussian function, but I am not quite sure how to write it since it is not happy with the following

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


open complex
open real

noncomputable theory

namespace real

def gaussian_complex  {d:ℕ } {a:ℂ} (ha:0<a.re): schwartz_map (fin d -> ℝ)   ℂ :=
  { to_fun := λ x : (fin d -> ℝ), complex.exp (-a * x^2),
    smooth' :=
    begin
      exact gaussian_smooth_complex a,
    end,
    decay' :=
    begin
      exact gaussian_decay a ha,
    end}

end real

[rtertr (Sonia)]

I guess, the broader, the better :D

[Eric Wieser]

What do you intend x^2 to mean when x is a vector? Because to lean, it means "square each coefficient"

[rtertr (Sonia)]

True, yeah, I guess it would be the norm and then squared!

[Eric Wieser]

Well then you need to write that!

[rtertr (Sonia)]

Yay, great, it worked like that!

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


open complex
open real

noncomputable theory

namespace real

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

end real

But would it then be incorrect to use(fin d -> ℝ) ?

[Eric Wieser]

Yes, the norm on fin d -> ℝ is the inf norm

[Eric Wieser]

I would recommend you generalize to schwartz_map A ℂ, and add typeclasses to A as you find that you need them

[Eric Wieser]

docs#schwartz_map tells you that you need at least [normed_add_comm_group A] [normed_space ℝ A]

[rtertr (Sonia)]

I don't know what typeclasses are, is there a place I can read about them? :D
And thank you for the help!

[Eric Wieser]

I don't know the proofs of the sorries, but that might be enough. Do you already have a proof for the 1D case?

[Eric Wieser]

I would guess #tpil has a relevant section on typeclasses

[rtertr (Sonia)]

Oh, yeah, these sorry's were just for shortening the thing :D I have the proof for 1D so now I will "just" adjust them :sweat_smile:

[Moritz Doll]

You probably want to have an docs#inner_product_space and at some point you will need to assume that you have finite dimensions.

[Moritz Doll]

It might be worthwhile to prove a composition result for docs#schwartz_map that is $f \circ g \in \mathcal{S}$ if $f \in \mathcal{S}$ and $g$ is smooth and polynomially bounded (this should be a sufficient condition, but I haven't checked it).

[Moritz Doll]

The problem is only that we have not very much API for docs#iterated_fderiv, so you have to fill in some of the blanks there.

[Moritz Doll]

(also for Schwartz space question feel free to ping me)

[Sebastien Gouezel]

I am precisely working on bounds for the iterated derivative of the product and composition of maps, in branch#SG_norm_iterated_fderiv_comp. But don't hold your breath, because I have very little Lean time currently.

[Sebastien Gouezel]

Prerequisites PR in #18592.

[Moritz Doll]

@rtertr (Sonia) are you still working on this / do you plan to PR your work at some point?

[rtertr (Sonia)]

Hi, yes, I got it to work for the inner space product :D Couldn't do it for the Banach unfortunately! Will submit some time soon, will try to have the Fourier inversion formula as well (but let's see:))