English
The Fourier transform is self-adjoint with respect to the bilinear form that uses the product in the target space; equivalently, the transform and its flip pair under the bilinear form to yield equal integrals.
Русский
Преобразование Фурье самосопряжено относительно билинейной формы; эквивалентно тому, что преобразование и его обратное образуют одинаковые интегралы при соответствующем билинейном виде.
LaTeX
$$$$ \\int \\mathrm{fourierIntegral}(e,\\mu,L,f)(\\xi) \\cdot g(\\xi) \\, d\\nu(\\xi) = \\int f(x) \\cdot \\mathrm{fourierIntegral}(e,\\nu,L.flip,g)(x) \\, d\\mu(x). $$$$
Lean4
/-- The Fourier transform satisfies `∫ 𝓕 f * g = ∫ f * 𝓕 g`, i.e., it is self-adjoint.
Version where the multiplication is replaced by a general bilinear form `M`. -/
theorem integral_bilin_fourierIntegral_eq_flip {f : V → E} {g : W → F} (M : E →L[ℂ] F →L[ℂ] G) (he : Continuous e)
(hL : Continuous fun p : V × W ↦ L p.1 p.2) (hf : Integrable f μ) (hg : Integrable g ν) :
∫ ξ, M (fourierIntegral e μ L f ξ) (g ξ) ∂ν = ∫ x, M (f x) (fourierIntegral e ν L.flip g x) ∂μ :=
by
by_cases hG : CompleteSpace G; swap; · simp [integral, hG]
calc
_ = ∫ ξ, M.flip (g ξ) (∫ x, e (-L x ξ) • f x ∂μ) ∂ν := rfl
_ = ∫ ξ, (∫ x, M.flip (g ξ) (e (-L x ξ) • f x) ∂μ) ∂ν :=
by
congr with ξ
apply (ContinuousLinearMap.integral_comp_comm _ _).symm
exact (fourierIntegral_convergent_iff he hL _).2 hf
_ = ∫ x, (∫ ξ, M.flip (g ξ) (e (-L x ξ) • f x) ∂ν) ∂μ :=
by
rw [integral_integral_swap]
have : Integrable (fun (p : W × V) ↦ ‖M‖ * (‖g p.1‖ * ‖f p.2‖)) (ν.prod μ) :=
(hg.norm.mul_prod hf.norm).const_mul _
apply this.mono
· -- This proof can be golfed but becomes very slow; breaking it up into steps
-- speeds up compilation.
change AEStronglyMeasurable (fun p : W × V ↦ (M (e (-(L p.2) p.1) • f p.2) (g p.1))) _
have A : AEStronglyMeasurable (fun (p : W × V) ↦ e (-L p.2 p.1) • f p.2) (ν.prod μ) :=
by
refine (Continuous.aestronglyMeasurable ?_).smul hf.1.comp_snd
exact he.comp (hL.comp continuous_swap).neg
have A' : AEStronglyMeasurable (fun p ↦ (g p.1, e (-(L p.2) p.1) • f p.2) : W × V → F × E) (Measure.prod ν μ) :=
hg.1.comp_fst.prodMk A
have B : Continuous (fun q ↦ M q.2 q.1 : F × E → G) := M.flip.continuous₂
apply B.comp_aestronglyMeasurable A'
· filter_upwards with ⟨ξ, x⟩
rw [Function.uncurry_apply_pair, Submonoid.smul_def, (M.flip (g ξ)).map_smul, ← Submonoid.smul_def,
Circle.norm_smul, ContinuousLinearMap.flip_apply, norm_mul, norm_norm M, norm_mul, norm_norm, norm_norm,
mul_comm (‖g _‖), ← mul_assoc]
exact M.le_opNorm₂ (f x) (g ξ)
_ = ∫ x, (∫ ξ, M (f x) (e (-L.flip ξ x) • g ξ) ∂ν) ∂μ := by
simp only [ContinuousLinearMap.flip_apply, ContinuousLinearMap.map_smul_of_tower, ContinuousLinearMap.coe_smul',
Pi.smul_apply, LinearMap.flip_apply]
_ = ∫ x, M (f x) (∫ ξ, e (-L.flip ξ x) • g ξ ∂ν) ∂μ :=
by
congr with x
apply ContinuousLinearMap.integral_comp_comm
apply (fourierIntegral_convergent_iff he _ _).2 hg
exact hL.comp continuous_swap
