Source indexedtheorem · leanprover/lean4:v4.32.0

fourierInvTrunc_fourier_eq_integral_kernel

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:172 to 185

Source documentation

Fubini swaps the finite-height inverse Fourier integral into the standard Dirichlet-kernel form. The hypothesis 0 ≤ T is the only orientation condition needed for the interval integral.

Exact Lean statement

theorem fourierInvTrunc_fourier_eq_integral_kernel
    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) (hT : 0 ≤ T) :
    fourierInvTrunc (𝓕 f) x T =
      (1 / (2 * π) : ℝ) •
        ∫ y : ℝ,
          ∫ t in (-T)..T, Complex.exp (((t * (x - y) : ℝ) : ℂ) * I) • f y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourierInvTrunc_fourier_eq_integral_kernel    {f : ℝ → E} (hf : Integrable f) (x T : ℝ) (hT : 0 ≤ T) :    fourierInvTrunc (𝓕 f) x T =      (1 / (2 * π) : ℝ) •        ∫ y : ℝ,          ∫ t in (-T)..T, Complex.exp (((t * (x - y) : ℝ) : ℂ) * I) • f y := by  rw [fourierInvTrunc_fourier_eq_integral_integral]  congr 1  have hle : -T ≤ T := by linarith  rw [intervalIntegral.integral_of_le hle]  rw [MeasureTheory.integral_integral_swap    (integrable_truncated_fourier_kernel_prod (E := E) hf x T)]  congr with y  rw [← intervalIntegral.integral_of_le hle]