Source indexedlemma · leanprover/lean4:v4.32.0

tail_indicator_sin_div_eq_sin_smul_quotient

PrimeNumberTheoremAnd.LaplaceInversion · PrimeNumberTheoremAnd/LaplaceInversion.lean:731 to 754

Source documentation

Pointwise tail algebra for the sine kernel.

Exact Lean statement

lemma tail_indicator_sin_div_eq_sin_smul_quotient
    (f : ℝ → E) (x T : ℝ) {R : ℝ} (hR : 0 < R) (u : ℝ) :
    (Set.Ioc (-R) R)ᶜ.indicator
        (fun u : ℝ =>
          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •
            f (x - u)) u =
      (Real.sin (T * u) : ℂ) •
        (Set.Ioc (-R) R)ᶜ.indicator
          (fun u : ℝ => (if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) •
            f (x - u)) u

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tail_indicator_sin_div_eq_sin_smul_quotient    (f : ℝ → E) (x T : ℝ) {R : ℝ} (hR : 0 < R) (u : ℝ) :    (Set.Ioc (-R) R)ᶜ.indicator        (fun u : ℝ =>          (if u = 0 then (0 : ℂ) else (Real.sin (T * u) / (π * u) : ℂ)) •            f (x - u)) u =      (Real.sin (T * u) : ℂ) •        (Set.Ioc (-R) R)ᶜ.indicator          (fun u : ℝ => (if u = 0 then (0 : ℂ) else (1 / (π * u) : ℂ)) •            f (x - u)) u := by  by_cases huSet : u ∈ (Set.Ioc (-R) R)ᶜ  · rw [Set.indicator_of_mem huSet, Set.indicator_of_mem huSet]    have hu_not : u ∉ Set.Ioc (-R) R := by simpa using huSet    have hu_ne : u ≠ 0 := by      intro h0      apply hu_not      have hzmem : (0 : ℝ) ∈ Set.Ioc (-R) R := by        exact ⟨by linarith, hR.le⟩      simpa [h0] using hzmem    rw [if_neg hu_ne, if_neg hu_ne, ← smul_assoc]    congr 1    simp only [div_eq_mul_inv]    ring  · rw [Set.indicator_of_notMem huSet, Set.indicator_of_notMem huSet, smul_zero]