ZetaAppendix.tendsto_sine_series_unit_interval

lemma tendsto_sine_series_unit_interval {x : ℝ} (hx0 : 0 < x) (hx1 : x < 1) :    Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) / (n + 1 : ℝ))      atTop (𝓝 (Real.pi * (1 / 2 - x))) := by  have hx_not_int : ¬ ∃ k : ℤ, x = k := not_exists_int_eq_of_mem_Ioo hx0 hx1  have hcomplex := tendsto_exp_over_nat_eq_neg_log_of_not_int hx_not_int  have him : Tendsto      (fun N : ℕ ↦        (∑ n ∈ range N,          ((1 : ℝ) / (n + 1 : ℝ)) •            (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1)).im)      atTop (𝓝 ((-Complex.log (1 - expPhase x)).im)) := by    exact (Complex.continuous_im.tendsto _).comp hcomplex  have hlimit : (-Complex.log (1 - expPhase x)).im = Real.pi * (1 / 2 - x) := by    rw [neg_im, Complex.log_im, arg_one_sub_expPhase_of_mem_Ioo hx0 hx1]    ring_nf  have hleft : Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) / (n + 1 : ℝ))      atTop (𝓝 ((-Complex.log (1 - expPhase x)).im)) := by    refine him.congr' ?_    filter_upwards with N    change Complex.imCLM        (∑ n ∈ range N,          ((1 : ℝ) / (n + 1 : ℝ)) •            (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1)) =      ∑ n ∈ range N, Real.sin (2 * Real.pi * (n + 1) * x) / (n + 1 : ℝ)    rw [map_sum Complex.imCLM]    apply Finset.sum_congr rfl    intro n _hn    change ((((1 : ℝ) / (n + 1 : ℝ)) • (expPhase x) ^ (n + 1)).im) =      Real.sin (2 * Real.pi * (n + 1) * x) / (n + 1 : ℝ)    rw [one_div_smul_expPhase_pow_im]  simpa [hlimit] using hleft