Source indexedtheorem · leanprover/lean4:v4.32.0

normalized_sinc_smul_eq_sin_div

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:291 to 316

Source documentation

The normalized sinc kernel is the usual sin (T * u) / (π * u) kernel, with the removable value at u = 0 made explicit.

Exact Lean statement

theorem normalized_sinc_smul_eq_sin_div (T u : ℝ) (z : E) :
    (1 / (2 * π) : ℝ) • ((2 * T * Real.sinc (T * u) : ℂ) • z) =
      (if u = 0 then (T / π : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • z

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem normalized_sinc_smul_eq_sin_div (T u : ℝ) (z : E) :    (1 / (2 * π) : ℝ) • ((2 * T * Real.sinc (T * u) : ℂ) • z) =      (if u = 0 then (T / π : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) • z := by  by_cases hu : u = 0  · subst u    rw [if_pos rfl]    simp only [one_div, mul_inv_rev, mul_zero, Real.sinc_zero, ofReal_one, mul_one]    rw [← smul_assoc]    congr 1    rw [RCLike.real_smul_eq_coe_mul]    push_cast    field_simp [Real.pi_ne_zero]    ring_nf    rfl  · rw [if_neg hu]    by_cases hT : T = 0    · subst T      simp    · rw [Real.sinc_of_ne_zero (mul_ne_zero hT hu)]      rw [← smul_assoc]      congr 1      rw [RCLike.real_smul_eq_coe_mul]      push_cast      field_simp [Real.pi_ne_zero, hT, hu]      ring_nf      rfl