English
The Fourier transform on a real inner product space acts on the Schwartz space as a continuous linear map.
Русский
Фурье-преобразование на вещественном пространстве с скобой по скалярам действует на пространства Шварца как непрерывное линейное отображение.
LaTeX
$$$ \mathrm{fourierTransformCLM}: \mathcal{S}(V,E) \to_L[\mathbb{K}] \mathcal{S}(V,E) $$$
Lean4
/-- The Fourier transform on a real inner product space, as a continuous linear map on the
Schwartz space. -/
noncomputable def fourierTransformCLM : 𝓢(V, E) →L[𝕜] 𝓢(V, E) :=
by
refine mkCLM (𝓕 ·) ?_ ?_ ?_ ?_
· intro f g x
simp only [fourierIntegral_eq, add_apply, smul_add]
rw [integral_add]
· exact (fourierIntegral_convergent_iff _).2 f.integrable
· exact (fourierIntegral_convergent_iff _).2 g.integrable
· intro c f x
simp only [fourierIntegral_eq, smul_apply, smul_comm _ c, integral_smul, RingHom.id_apply]
· intro f
exact Real.contDiff_fourierIntegral (fun n _ ↦ integrable_pow_mul volume f n)
· rintro ⟨k, n⟩
refine
⟨Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1),
(2 * π) ^ n * (2 * ↑n + 2) ^ k * (Finset.range (n + 1) ×ˢ Finset.range (k + 1)).card *
2 ^ integrablePower (volume : Measure V) *
(∫ (x : V), (1 + ‖x‖) ^ (-(integrablePower (volume : Measure V) : ℝ))) *
2,
⟨by positivity, fun f x ↦ ?_⟩⟩
apply
(pow_mul_norm_iteratedFDeriv_fourierIntegral_le (f.smooth ⊤)
(fun k n _hk _hn ↦ integrable_pow_mul_iteratedFDeriv _ f k n) le_top le_top x).trans
simp only [mul_assoc]
gcongr
calc
∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1), ∫ (v : V), ‖v‖ ^ p.1 * ‖iteratedFDeriv ℝ p.2 (⇑f) v‖ ≤
∑ p ∈ Finset.range (n + 1) ×ˢ Finset.range (k + 1),
2 ^ integrablePower (volume : Measure V) *
(∫ (x : V), (1 + ‖x‖) ^ (-(integrablePower (volume : Measure V) : ℝ))) *
2 *
((Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)).sup
(schwartzSeminormFamily 𝕜 V E))
f :=
by
apply Finset.sum_le_sum (fun p hp ↦ ?_)
simp only [Finset.mem_product, Finset.mem_range] at hp
apply (f.integral_pow_mul_iteratedFDeriv_le 𝕜 _ _ _).trans
simp only [mul_assoc]
rw [two_mul]
gcongr
· apply Seminorm.le_def.1
have : (0, p.2) ∈ (Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)) := by
simp [hp.2]
apply Finset.le_sup this (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2 (E := V) (F := E))
· apply Seminorm.le_def.1
have :
(p.1 + integrablePower (volume : Measure V), p.2) ∈
(Finset.range (n + integrablePower (volume : Measure V) + 1) ×ˢ Finset.range (k + 1)) :=
by
simp [hp.2]
omega
apply Finset.le_sup this (f := fun p ↦ SchwartzMap.seminorm 𝕜 p.1 p.2 (E := V) (F := E))
_ = _ := by simp [mul_assoc]
