English
The Fourier transform of a sum equals the sum of Fourier transforms, assuming integrability of the summands.
Русский
Преобразование Фурье суммы равно сумме преобразований Фурье с предположением интегрируемости слагаемых.
LaTeX
$$$$ \\mathrm{fourierIntegral}(e, \\mu, L, f + g) = \\mathrm{fourierIntegral}(e, \\mu, L, f) + \\mathrm{fourierIntegral}(e, \\mu, L, g). $$$$
Lean4
/-- For any `w`, the Fourier integral is convergent iff `f` is integrable. -/
theorem fourierIntegral_convergent_iff (he : Continuous e) (hL : Continuous fun p : V × W ↦ L p.1 p.2) {f : V → E}
(w : W) : Integrable (fun v : V ↦ e (-L v w) • f v) μ ↔ Integrable f μ := by
-- first prove one-way implication
have aux {g : V → E} (hg : Integrable g μ) (x : W) : Integrable (fun v : V ↦ e (-L v x) • g v) μ :=
by
have c : Continuous fun v ↦ e (-L v x) := he.comp (hL.comp (.prodMk_left _)).neg
simp_rw [← integrable_norm_iff (c.aestronglyMeasurable.smul hg.1), Circle.norm_smul]
exact hg.norm
refine ⟨fun hf ↦ ?_, fun hf ↦ aux hf w⟩
have := aux hf (-w)
simp_rw [← mul_smul (e _) (e _) (f _), ← e.map_add_eq_mul, LinearMap.map_neg, neg_add_cancel, e.map_zero_eq_one,
one_smul] at this
exact this
