Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegral_sin_div_kernel_symmetric_eq_two_mul_zero_to

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1132 to 1150

Source documentation

The symmetric finite sine integral is twice its positive half.

Exact Lean statement

theorem intervalIntegral_sin_div_kernel_symmetric_eq_two_mul_zero_to (A : ℝ) :
    (∫ v in (-A)..A,
      if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)) =
      2 * ∫ v in 0..A,
        if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem intervalIntegral_sin_div_kernel_symmetric_eq_two_mul_zero_to (A : ℝ) :    (∫ v in (-A)..A,      if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)) =      2 * ∫ v in 0..A,        if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ) := by  let k : ℝ → ℂ := fun v => if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)  have hleft : (∫ v in (-A)..0, k v) = ∫ v in 0..A, k v := by    exact intervalIntegral_sin_div_kernel_neg_zero_eq_zero_to A  have hsplit : (∫ v in (-A)..0, k v) + (∫ v in 0..A, k v) =      ∫ v in (-A)..A, k v := by    exact intervalIntegral.integral_add_adjacent_intervals      (intervalIntegrable_sin_div_kernel (-A) 0)      (intervalIntegrable_sin_div_kernel 0 A)  calc    (∫ v in (-A)..A, k v) = (∫ v in (-A)..0, k v) + (∫ v in 0..A, k v) := by      rw [hsplit]    _ = (∫ v in 0..A, k v) + (∫ v in 0..A, k v) := by      rw [hleft]    _ = 2 * ∫ v in 0..A, k v := by ring