Schwartz Space

Stream: general

[rtertr (Sonia)]

Hi everyone,
I am trying to work with the Schwartz space from analysis.schwartz_space.
I want to produce small proofs such as 'f : 𝓢(E, F) --> x*f : 𝓢(E, F)' and 'f: 𝓢(E, F) --> f.fderiv: 𝓢(E, F)'.
Unfortunately, I already have issues with this proof, which makes me think I am setting up the proof incorrectly.

lemma fderiv_schwartz (f : schwartz_map ℝ ℂ  ): (f: schwartz_map ℝ  ℂ ) :=
begin
  sorry,
end

I would like to do something like this eventually

lemma fourier_transform (f : schwartz_map  ℝ ℂ  ) : (real.fourier_integral f : schwartz_map  ℝ ℂ  ) :=
begin
  sorry,
end

Furthermore, I wanted to show that the Gaussian function is in the Schwartz space.
I have the proofs lemma gaussian_smooth: cont_diff ℝ ⊤ (λ (x : ℝ), exp (-x^2)) :=
and lemma gaussian_decay (a:ℝ) (ha: 0<a): ∀ (k n : ℕ), ∃ (C : ℝ), ∀ x, ‖x‖^k * ‖iterated_fderiv ℝ n (λ (x : ℝ), exp (-a*x^2)) x‖ ≤ C :=
and def gaussian:=exp (x^2) (Not sure how to give it right way to write the function )

It does not complain with this set up, but I have a feeling that it perceives gaussian_smooth and gaussian_decay as functions, and not the proofs supporting gaussian.

lemma in_schwartz_map ( gaussian gaussian_smooth gaussian_decay: schwartz_map  ℝ ℂ   ): 1=1:=
begin
  sorry,
end

I am just a little confused when it comes to structures. From my understanding, I need to give the arguments to_fun,smooth',decay', but when and where do I give these arguments.

Kind regards,
Sonia

[Yaël Dillies]

Hey! schwartz_map ℝ ℂ is a structure, so "elements" (understand, terms) of it are Schwartz functions. In particular, they are not functions ℝ → ℂ. There is a way to consider f : schwartz_map ℝ ℂ as a function ℝ → ℂ, namely by inserting a coercion to functions, coe_fn. If f : schwartz_map ℝ ℂ, then ⇑f : ℝ → ℂ (but confusingly you have to let Lean insert the ⇑ for you). The other way, proving that a function f : ℝ → ℂis a Schwartz function, amounts to constructing a schwartz_map ℝ ℂ whose to_fun field is defined as f.

[Yaël Dillies]

Here is a toy example to show that the zero map is a Schwartz map

example : schwartz_map ℝ ℂ :=
{ to_fun := 0,
  smooth' := sorry, -- your proof of smoothness here
  decay' := sorry } -- your proof of decay here

[Eric Wieser]

Also, make sure to check out #backticks for posting code on Zulip

[rtertr (Sonia)]

Okay, so I try to write :

 { to_fun := (λ (x : ℝ), exp (-x ^ 2)),
  smooth' := gaussian_smooth,
  decay' := gaussian_decay}

Then it says:

type mismatch at field 'smooth''
gaussian_smooth
has type
cont_diff ℝ ⊤ (λ (x : ℝ), exp (-x ^ 2))
but is expected to have type
cont_diff ℝ ⊤ (λ (x : ℝ), ↑(exp (-x ^ 2)))

and similarly for decay'. Is there a quick fix here? Is it the same as coe_fn?

[Yaël Dillies]

Hard to say! Can you follow the instructions at #mwe?

[Yaël Dillies]

My guess is that you proved that x ↦ exp (- x ^ 2) was smooth as a function ℝ → ℝ while Lean expects you to prove it's smooth as a function ℝ → ℂ.

[rtertr (Sonia)]

So I am trying to make a mwe, but it is taking some time :sweat_smile: . But I saw you needed to provide
cont_diff ℝ ⊤ self.to_fun by definition, and so my proof is cont_diff ℝ ⊤ (λ (x : ℝ), exp (-x^2)) but yeah, I am not sure why it has ℝ by definition :D

[rtertr (Sonia)]

So I tried to make it as small as possible.
The decay proof has a sorry, because it was building upon other lemmas.

import analysis.schwartz_space
import analysis.special_functions.exp_deriv

namespace real

noncomputable theory

open complex

lemma gaussian_decay:  ∀ (k n : ℕ), ∃ (C : ℝ), ∀ x, ‖x‖^k * ‖iterated_fderiv ℝ n (λ (x : ℝ), exp (-x^2)) x‖ ≤ C :=
begin
  sorry,
end

lemma gaussian_smooth:  cont_diff ℝ ⊤ (λ (x : ℝ), exp (-x^2)) :=
begin
  have hid: cont_diff ℝ ⊤ (λ (x : ℝ), x),
    apply cont_diff_id,
  have hsq: cont_diff ℝ ⊤ (λ (x : ℝ), x^2),
    apply cont_diff.pow hid (2:ℕ),
  have hsqneg: cont_diff ℝ ⊤ (λ (x : ℝ), -x^2),
    apply cont_diff.neg hsq,
  have hexp: cont_diff ℝ ⊤ (λ (x : ℝ), exp x),
    apply cont_diff.exp,
    exact hid,
  apply cont_diff.comp hexp hsqneg,
end

example : schwartz_map ℝ ℂ :=
{ to_fun := (λ (x : ℝ), exp (-x ^ 2)),
  smooth' := gaussian_smooth,
  decay' := gaussian_decay}

lemma gaussian_smooth_2:  cont_diff ℝ ⊤ (λ (x : ℝ), ↑(exp (-x ^ 2))) :=  -- tried to make a new proof the way it was desired, but it would not recognize it, unfortunately.
begin
  sorry,
end

end real

[Yaël Dillies]

Yeah so the problem is exactly what I said. gaussian_smooth proves smoothness a function ℝ → ℝ and smooth' expects smoothness of the "same" function but as ℝ → ℂ.

[Yaël Dillies]

They are related by composing with the coercion coe : ℝ → ℂ. So you can bridge the gap by using the fact that the compositiion of smooth functions is smooth. But I don't know where is the fact that the coercion is smooth.

[rtertr (Sonia)]

Okay, thank you so much! Would the statement then be cont_diff ℂ ⊤ (λ (x : ℝ), exp (-x^2)) instead? :D

[Yaël Dillies]

Yep, sounds like it.

[rtertr (Sonia)]

Thank you! :D

[rtertr (Sonia)]

But just one question, in the definition of the Schwartz space, it says you need to give a proof of smooth' : cont_diff ℝ ⊤ self.to_fun so I think even if I show cont_diff ℂ ⊤ (λ (x : ℝ), ↑exp (-x^2)) I might still be in trouble

[Yaël Dillies]

Oh I might be wrong then. The best way for you to prove the right statement is to prove whatever the goal inside the smooth' field.

[rtertr (Sonia)]

ah, okay great! I will try that then :D Thank you again

[Jireh Loreaux]

@Moritz Doll will know how to address your issues I'm sure.

[Moritz Doll]

Good morning. It is great to hear that you want to prove that the Fourier transform is a map from the Schwartz space to itself. This is a very nontrivial problem and I would suggest to start with the Gaussian, that should be way easier.
The definition should be

def gaussian : 𝓢(ℝ, ℝ) :=
  { to_fun := λ x, exp (-x^2),
    smooth' :=
    begin
      sorry,
    end,
    decay' :=
    begin
      sorry,
    end }

As for the coercion, the differentiable version is:

lemma complex.differentiable_at_coe {f : E → ℝ} {x : E} (hf : differentiable_at ℝ f x) :
  differentiable_at ℝ (λ y, (f y : ℂ)) x :=
complex.of_real_clm.differentiable_at.comp _ hf

and I think the cont_diff version is very similar (I haven't checked)

[David Loeffler]

@rtertr Great to see someone else interested in this stuff! I've been working for a while myself on Fourier transforms, Poisson summation (which finally made it into mathlib a week or two back), etc. One of the goals of that project was to apply Poisson summation to the Gaussian, in order to get the transformation law for the Jacobi theta function (+ hence the functional equation of Riemann zeta). If you can prove that the Gaussian is in the Schwartz space (ideally the slightly more general statement that $exp( -a * x ^ 2)$ is Schwartz for any $0 < a$) then that would certainly be very useful for my project, so we should definitely coordinate.

[rtertr (Sonia)]

@David Loeffler Hi David,
That sounds great! I am a third year undergraduate student trying to do my thesis on Fourier transforms in Lean.
Right now I have
lemma gaussian_decay (a:ℝ) (ha: 0<a): ∀ (k n : ℕ), ∃ (C : ℝ), ∀ x, ‖x‖^k * ‖iterated_fderiv ℝ n (λ (x : ℝ), exp (-a*x^2)) x‖ ≤ C
with a few minor sorrys along the way. I would love to do some collaboration. I would just have to discuss it with my thesis advisor first probably :D

[rtertr (Sonia)]

Hi, I was thinking a bit about the Schwartz map. In LEAN, the maps goes between two real normed vector spaces,
[normed_add_comm_group E] [normed_space ℝ E].
I was wondering why does the field need to be ℝ? I see that iterated fderiv and cont diff require a nontrivially normed field k.
Could the Schwartz space exist between [normed_add_comm_group E] [normed_space k E]?
Kind regards

[David Loeffler]

Is this generalisation useful? E.g. if you take the field to be $\mathbb{C}$, then the definitions make perfect sense, but I'm pretty sure that the resulting space is zero.

[rtertr (Sonia)]

Okay, interesting! Why would the space become zero?

[Moritz Doll]

Liouville's theorem + Schwartz functions vanish at infinity

[Eric Wieser]

Is this generalisation useful?

It sounds like the generalization is useful to have in mathlib because it allows you to formally prove that mathematically it is not useful!

[Moritz Doll]

I disagree, we would have to keep repeating everywhere that we consider the real derivative, which is the only sensible choice. There are more general ways to phrase this and this should not clutter up the Schwartz space.

[Eric Wieser]

(I was mostly joking :smile:)

[Moritz Doll]

oh sorry, I did not get that.

[Kevin Buzzard]

yeah someone once joked about how it would be great to have modules over semirings and look what happened then :-/

[Eric Wieser]

Hey, it let us unify the nsmul lemmas with smul lemmas everywhere, so I think that was maybe worth it!

[Giovanni Mascellani]

Kevin Buzzard said:

yeah someone once joked about how it would be great to have modules over semirings and look what happened then :-/

A professor of mine used to joke over giving a course on algebraically closed finite fields and prove all sort of wonderful properties, only to show in the last lecture that there aren't.

[Eric Rodriguez]

Modules over semirings suffer from the fact that normal equivalences that are used in theory building don't hold - I'm thinking linear independence is broken right now, iirc

[Eric Rodriguez]

But I don't see what's the issue with making schwartz spaces over all fields and then we just decide to only build the theory over R-VSs

[Kevin Buzzard]

I don't see the issue of making groups over all notational symbols and then just asking the user to supply * every time they want to use * as a group law. But the people typing in the group theory theorems do.

[Kevin Buzzard]

It's not about what is possible, it's about what people want to do in practice. This is why the mathematicians have to have the final word on questions such as this.

[Anatole Dedecker]

I don’t think modules of semirings is the right analogy here, because even if the theory is not very developed there are still concrete examples where it allows for some code factorization. Here there is absolutely nothing to say about Schwartz maps over $\mathbb{C}$ because they are all zero. I don’t know anything about the p-adic case, but I would definitely argue in favor of sticking to real differentiable maps.

[Kevin Buzzard]

@Anatole Dedecker what's the definition? I can try and figure out the p-adic story. Maybe it will turn out to be terrifically interesting and then Eric is vindicated :-)

[Anatole Dedecker]

https://en.wikipedia.org/wiki/Schwartz_space or docs#schwartz_map

[Kevin Buzzard]

@Olivier Taïbi aren't these used by Jacquet-Langlands in the p-adic case? My memory is that this is the language they use, but when I tried to understand what they were doing I wondered whether they were just using it as an abbreviation for "locally constant function" or some such thing. Jacquet-Langlands never define the word IIRC.

[Eric Rodriguez]

Kevin Buzzard said:

I don't see the issue of making groups over all notational symbols and then just asking the user to supply * every time they want to use * as a group law. But the people typing in the group theory theorems do.

This would've been great - means we can state eckmann hilton easily! Reminds me of the theorems stated comparing two topologies, too :)

[Sophie Morel]

Kevin Buzzard said:

Olivier Taïbi aren't these used by Jacquet-Langlands in the p-adic case? My memory is that this is the language they use, but when I tried to understand what they were doing I wondered whether they were just using it as an abbreviation for "locally constant function" or some such thing. Jacquet-Langlands never define the word IIRC.

Usually what we call "Schwartz space" in the p-adic case is the space of locally constant functions with compact support. Then we have a nice Fourier transform on it. I don't think that there is a good notion of differentiable maps on totally disconnected groups with values in something like $\mathbb{C}$. Now if we're talking p-adic maps on p-adic groups, that's another story...

[Olivier Taïbi]

Sophie Morel said:

Kevin Buzzard said:

Olivier Taïbi aren't these used by Jacquet-Langlands in the p-adic case? My memory is that this is the language they use, but when I tried to understand what they were doing I wondered whether they were just using it as an abbreviation for "locally constant function" or some such thing. Jacquet-Langlands never define the word IIRC.

Usually what we call "Schwartz space" in the p-adic case is the space of locally constant functions with compact support. Then we have a nice Fourier transform on it. I don't think that there is a good notion of differentiable maps on totally disconnected groups with values in something like $\mathbb{C}$. Now if we're talking p-adic maps on p-adic groups, that's another story...

Yes, and these are certainly enough for Jacquet-Langlands. There are also weaker notions (i.e. bigger spaces, more similar to the real case) that are useful, see what google found.

[Sophie Morel]

In case someone who is not familiar with p-adic functions follows Olivier's link: "smooth" in that context means "locally constant" !

[David Loeffler]

Exactly: the useful generalisation of Schwartz functions in the p-adic case is functions whose source is p-adic but whose target is real / complex. As Kevin, Sophie, and Olivier (knowing my mathematical tastes) will probably have guessed, this is a mathematical structure that I am personally extremely interested in and definitely would want mathlib to have in future. But this notion of p-adic Schwartz functions can't sensibly be gotten simply by making a general definition for an arbitrary normed field $\mathbb{k}$ which recovers the usual one for $\mathbb{R}$, and then plugging in $\mathbb{Q}_p$ to this; it will need to be set up separately.

[David Loeffler]

There are also spaces of differentiable functions with p-adic source and target, which are important in p-adic Langlands theory and in Iwasawa theory – this is the theory described in Colmez's lovely little monograph "Fonctions d'une variable p-adique". But these behave very differently from complex Schwartz functions, and the term "Schwartz space" is not usually used for them ("locally analytic functions" is the usual jargon).

[Kevin Buzzard]

Just spelling it out for those who don't know the area: the point is that number theorists definitely want to consider functions $f:\mathbb{Q}_p\to\mathbb{C}$ which are locally constant (this does not imply constant because $\mathbb{Q}_p$ is a long way from being connected), but one cannot differentiate these functions in the usual manner because $(f(x+h)-f(x))/h$ doesn't typecheck (numerator is complex, denominator is p-adic). So we call them "Schwarz functions" (at least if they're compactly supported) but we're not using a generalisation of the mathlib definition, it's more like an analogy.

[Kevin Buzzard]

Because JL never wrote down the definition I was never sure whether they were allowing locally constant functions which didn't have compact support but which were decaying sufficiently fast that the integral converged anyway; I have some pencil note about this on p1 of my copy of the book! This is one reason why I was interested in finding out what was actually going on.

[David Loeffler]

Definitely in Jacquet-Langlands theory (& also in Tate's thesis, etc), one wants to allow non-compactly-supported, but L^1, functions from p-adic spaces to R. Integrating these functions is what gives you L-factors, and the failure of these functions to be compactly supported is exactly what makes the L-factors be non-trivial and interesting objects.

[Kevin Buzzard]

Yes, they definitely show up in Tate. I was just wondering whether they were Schwarz functions :-) If we allow x/y to make sense if x is the complex number 0 and y is p-adic (and we let the quotient be 0), then probably they satisfy the definition :-)

[Olivier Taïbi]

I believe you can prove JL (at least for GL_2) without L-functions, if you prove a trace formula which is not restricted to regular semi-simple support and prove transfer from D^x to GL_2(F) (the regular semi-simple version is easy, in general you need to consider Shalika germs, and so integrable functions on p-adic spaces).
In Deligne's paper he uses Godement-Jacquet L-functions to show that there are only finitely many automorphic representations which are prescribed outside some finite set S of places, with no a priori bound on ramification at S. I forget if JL use a similar trick or prove transfer.

[Olivier Taïbi]

(of course L-functions are interesting and essential for other reasons)

[Chris Hughes]

(deleted)

[David Loeffler]

I believe you can prove JL (at least for GL_2) without L-functions [...] (of course L-functions are interesting and essential for other reasons)

Maybe we're talking slightly at cross-purposes here; I understood Kevin's reference to "Jacquet-Langlands" to mean the entire theory developed in Jacquet and Langlands' SLN 114 volume, whose primary goal (as they explicitly state in the introduction) is to establish analytic continuation + functional equation for GL2 automorphic L-functions. The theorem about functoriality between GL2 and quaternion algebras in section 16 of that book, which posterity happens to have assigned the name "the Jacquet-Langlands theorem", is explicitly described as an "afterthought" in their introduction.

The suggestion that one might only be interested in L-functions as a tool for proving Langlands functoriality results seems quite bizarre to me – personally, for me, the reverse is true: I'm only interested in Langlands functoriality if I can use it to help me prove theorems about L-functions!

Anyway, I think we are all in agreement that (a) mathlib will definitely need to have some kind of p-adic Schwartz spaces in due course, but (b) their definition is sufficiently different from the real-analytic versions that they will need to be developed separately, so mechanically generalising the real-analytic theory with [nontrivially_normed_field k] everywhere is probably not useful.