Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegral_sin_div_kernel_neg_zero_eq_zero_to

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:1115 to 1129

Source documentation

The negative half of the finite sine integral equals the positive half.

Exact Lean statement

theorem intervalIntegral_sin_div_kernel_neg_zero_eq_zero_to (A : ℝ) :
    (∫ v in (-A)..0,
      if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)) =
      ∫ 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_neg_zero_eq_zero_to (A : ℝ) :    (∫ v in (-A)..0,      if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)) =      ∫ 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 h := intervalIntegral.integral_comp_neg (f := k) (a := 0) (b := A)  rw [neg_zero] at h  rw [← h]  refine intervalIntegral.integral_congr ?_  intro v _hv  by_cases hv : v = 0  · simp [k, hv]  · have hneg : -v ≠ 0 := neg_ne_zero.mpr hv    simp [k, hv, hneg]