Source indexedtheorem · leanprover/lean4:v4.32.0

intervalIntegral_sin_div_kernel_scalar_mass_eq_scaled

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:967 to 999

Source documentation

Scaling reduces the finite-window mass of sin (T * u) / (π * u) to the normalized symmetric sine integral at height T * R.

Exact Lean statement

theorem intervalIntegral_sin_div_kernel_scalar_mass_eq_scaled (T R : ℝ) :
    (∫ u in (-R)..R,
      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) =
      (1 / (π : ℂ)) *
        ∫ v in (T * (-R))..(T * R),
          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_scalar_mass_eq_scaled (T R : ℝ) :    (∫ u in (-R)..R,      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) =      (1 / (π : ℂ)) *        ∫ v in (T * (-R))..(T * R),          if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ) := by  let g : ℝ → ℂ := fun v => if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ)  have hpoint : (fun u : ℝ =>      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) =      fun u : ℝ => (1 / (π : ℂ)) * (T • g (T * u)) := by    funext u    by_cases hT : T = 0    · simp [hT, g]    by_cases hu : u = 0    · simp [hu, g]    have hTu : T * u ≠ 0 := mul_ne_zero hT hu    simp [g, hu, hTu]    field_simp [Real.pi_ne_zero, hT, hu]  calc    (∫ u in (-R)..R,      if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ))        = ∫ u in (-R)..R, (1 / (π : ℂ)) * (T • g (T * u)) := by          rw [hpoint]    _ = (1 / (π : ℂ)) * ∫ u in (-R)..R, T • g (T * u) := by          rw [intervalIntegral.integral_const_mul]    _ = (1 / (π : ℂ)) * (T • ∫ u in (-R)..R, g (T * u)) := by          rw [intervalIntegral.integral_smul]    _ = (1 / (π : ℂ)) * ∫ v in (T * (-R))..(T * R), g v := by          rw [intervalIntegral.smul_integral_comp_mul_left]    _ = (1 / (π : ℂ)) *        ∫ v in (T * (-R))..(T * R),          if v = 0 then (0 : ℂ) else (Real.sin v / v : ℂ) := by          rfl