Source indexedtheorem · leanprover/lean4:v4.32.0

integrable_truncated_fourier_kernel_prod

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:152 to 167

Source documentation

The truncated oscillatory Fourier kernel is product-integrable when the source is integrable. This is the finite-height Fubini input for principal-value inversion.

Exact Lean statement

theorem integrable_truncated_fourier_kernel_prod
    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) :
    Integrable
      (fun z : ℝ × ℝ => Complex.exp (((z.1 * (x - z.2) : ℝ) : ℂ) * I) • f z.2)
      ((volume.restrict (Set.Ioc (-T) T)).prod volume)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integrable_truncated_fourier_kernel_prod    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) :    Integrable      (fun z : ℝ × ℝ => Complex.exp (((z.1 * (x - z.2) : ℝ) : ℂ) * I) • f z.2)      ((volume.restrict (Set.Ioc (-T) T)).prod volume) := by  have hconst : Integrable (fun _ : ℝ => (1 : ℂ))      (volume.restrict (Set.Ioc (-T) T)) := by    exact MeasureTheory.integrable_const (1 : ℂ)  have hprod := hconst.smul_prod hf  refine hprod.mono ?_ ?_  · exact (by fun_prop : Continuous        (fun z : ℝ × ℝ => Complex.exp (((z.1 * (x - z.2) : ℝ) : ℂ) * I)))        |>.aestronglyMeasurable.smul hf.aestronglyMeasurable.comp_snd  · filter_upwards with z    rw [norm_smul, Complex.norm_exp_ofReal_mul_I, one_mul]    simp