Source indexedtheorem · leanprover/lean4:v4.32.0

integral_Ioi_exp_neg_mul_sinc_eq_arctan_inv_of_integral_swap

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1909 to 1931

Source documentation

Evaluation of the damped sinc integral from the one remaining Fubini swap. The hypothesis is the exact product-integrability/swap term left to prove.

Exact Lean statement

theorem integral_Ioi_exp_neg_mul_sinc_eq_arctan_inv_of_integral_swap
    (a : ℝ) (ha : 0 < a)
    (hswap :
      (∫ x : ℝ in Set.Ioi 0,
        ∫ u : ℝ in Set.Ioi a, Real.exp (-u * x) * Real.sin x) =
      ∫ u : ℝ in Set.Ioi a,
        ∫ x : ℝ in Set.Ioi 0, Real.exp (-u * x) * Real.sin x) :
    ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x =
      Real.arctan a⁻¹

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem integral_Ioi_exp_neg_mul_sinc_eq_arctan_inv_of_integral_swap    (a : ℝ) (ha : 0 < a)    (hswap :      (∫ x : ℝ in Set.Ioi 0,        ∫ u : ℝ in Set.Ioi a, Real.exp (-u * x) * Real.sin x) =      ∫ u : ℝ in Set.Ioi a,        ∫ x : ℝ in Set.Ioi 0, Real.exp (-u * x) * Real.sin x) :    ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x =      Real.arctan a⁻¹ := by  calc    ∫ x : ℝ in Set.Ioi 0, Real.exp (-a * x) * Real.sinc x        = ∫ x : ℝ in Set.Ioi 0,            ∫ u : ℝ in Set.Ioi a, Real.exp (-u * x) * Real.sin x := by          refine integral_congr_ae ?_          filter_upwards [ae_restrict_mem measurableSet_Ioi] with x hx          exact (integral_Ioi_exp_neg_mul_const_mul_sin a x hx).symm    _ = ∫ u : ℝ in Set.Ioi a,          ∫ x : ℝ in Set.Ioi 0, Real.exp (-u * x) * Real.sin x := hswap    _ = ∫ u : ℝ in Set.Ioi a, (1 / (u ^ 2 + 1) : ℝ) := by          refine integral_congr_ae ?_          filter_upwards [ae_restrict_mem measurableSet_Ioi] with u hu          exact integral_Ioi_exp_neg_mul_sin u (lt_trans ha hu)    _ = Real.arctan a⁻¹ := integral_Ioi_one_div_one_add_sq_eq_arctan_inv a ha