Source indexedtheorem · leanprover/lean4:v4.32.0

fourierIntegral_self_add_deriv_deriv

PrimeNumberTheoremAnd.Fourier · PrimeNumberTheoremAnd/Fourier.lean:59 to 67

Mathematical statement

Exact Lean statement

theorem fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) :
    (1 + u ^ 2) * 𝓕 (f : ℝ → ℂ) u =
      𝓕 (fun u : ℝ => (f u - (1 / (4 * π ^ 2)) * deriv^[2] f u : ℂ)) u

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem fourierIntegral_self_add_deriv_deriv (f : W21) (u : ℝ) :    (1 + u ^ 2) * 𝓕 (f : ℝ → ℂ) u =      𝓕 (fun u : ℝ => (f u - (1 / (4 * π ^ 2)) * deriv^[2] f u : ℂ)) u := by  have l1 : Integrable (fun x => (((π : ℂ) ^ 2)⁻¹ * 4⁻¹) * deriv (deriv f) x) := by    apply Integrable.const_mul ; simpa [iteratedDeriv_succ] using f.integrable le_rfl  have l4 : Differentiable ℝ f := f.differentiable  have l5 : Differentiable ℝ (deriv f) := f.deriv.differentiable  simp [f.hf, l1, add_mul, Real.fourier_deriv f.hf' l5 f.hf'', Real.fourier_deriv f.hf l4 f.hf']  field_simp [pi_ne_zero] ; ring_nf ; simp