Source indexedtheorem · leanprover/lean4:v4.32.0

fourierInvTrunc_fourier_eq_integral_integral

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:125 to 147

Mathematical statement

Exact Lean statement

theorem fourierInvTrunc_fourier_eq_integral_integral
    (f : ℝ → E) (x T : ℝ) :
    fourierInvTrunc (𝓕 f) x T =
      (1 / (2 * π) : ℝ) •
        ∫ t in (-T)..T,
          ∫ y : ℝ, Complex.exp (((t * (x - y) : ℝ) : ℂ) * I) • f y

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourierInvTrunc_fourier_eq_integral_integral    (f : ℝ → E) (x T : ℝ) :    fourierInvTrunc (𝓕 f) x T =      (1 / (2 * π) : ℝ) •        ∫ t in (-T)..T,          ∫ y : ℝ, Complex.exp (((t * (x - y) : ℝ) : ℂ) * I) • f y := by  unfold fourierInvTrunc  congr 1  refine intervalIntegral.integral_congr ?_  intro t _ht  change Complex.exp (((t * x : ℝ) : ℂ) * I) • 𝓕 f (t / (2 * π)) =    ∫ y : ℝ, Complex.exp (((t * (x - y) : ℝ) : ℂ) * I) • f y  rw [Real.fourier_real_eq_integral_exp_smul]  rw [← MeasureTheory.integral_smul]  congr with y  rw [← smul_assoc]  congr 1  rw [smul_eq_mul]  rw [← Complex.exp_add]  congr 1  push_cast  field_simp [Real.pi_ne_zero]  ring