Source indexedlemma · leanprover/lean4:v4.32.0

ZetaAppendix.tendsto_sine_over_pi_series_of_not_int

PrimeNumberTheoremAnd.IEANTN.ZetaAppendix · PrimeNumberTheoremAnd/IEANTN/ZetaAppendix.lean:2446 to 2459

Mathematical statement

Exact Lean statement

lemma tendsto_sine_over_pi_series_of_not_int {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :
    Tendsto
      (fun N : ℕ ↦
        ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) /
          (Real.pi * (n + 1 : ℝ)))
      atTop (𝓝 (1 / 2 - Int.fract x))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma tendsto_sine_over_pi_series_of_not_int {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :    Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) /          (Real.pi * (n + 1 : ℝ)))      atTop (𝓝 (1 / 2 - Int.fract x)) := by  have h := (tendsto_sine_series_of_not_int hx).const_mul (1 / Real.pi)  refine h.congr' ?_ |>.trans_eq ?_  · filter_upwards with N    rw [Finset.mul_sum]    apply Finset.sum_congr rfl    intro n _hn    field_simp [Real.pi_ne_zero]  · field_simp [Real.pi_ne_zero]