Fourier Transform for Schwartz function

Stream: new members

[T H]

Hi. This is the first time using Zulip. If something’s wrong please teach me how I should do.

I want to show that Fourier Transform 𝓕 sends Schwartz functions (rapidly decreasing functions) to Schwartz functions. I consider only the simple 𝓕 (given in docs#Real.fourierIntegral) and 𝓢(E ; ℝ) for Schwartz space.

Given required smoothness and decay conditions, how can I express “𝓕 ϕ ∈ 𝓢” in Lean? As far as I know, since 𝓢 is defined as a type, “𝓕 ϕ : 𝓢” can’t be a conclusion of theorem like

theorem FT_of_s_is_s (x : 𝓢(E, ℝ)) : 𝓕 x : 𝓢 := by
— smoothness and decay condition

I indeed want to show it having type 𝓢, not just stating explicit conditions in the theorem, because I’ll use it to define 𝓕 for tempered distribution. Any help will be appreciated.

[Ruben Van de Velde]

I recall some things in that direction happening recently... Let me look

[Ruben Van de Velde]

There we are: #12144 and docs#SchwartzMap.fourierTransformCLM

[T H]

Thanks! I didn’t noticed that file because I used packages downloaded with MIL before. I’ll read the proof.