ZetaAppendix.tendsto_exp_over_nat_eq_neg_log_of_not_int

lemma tendsto_exp_over_nat_eq_neg_log_of_not_int {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :    Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N,          ((1 : ℝ) / (n + 1 : ℝ)) •            (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ (n + 1))      atTop (𝓝 (-Complex.log (1 - expPhase x))) := by  obtain ⟨L, hL⟩ := exists_tendsto_exp_over_nat_of_not_int hx  have hL_div : Tendsto      (fun N : ℕ ↦        ∑ n ∈ range N, (expPhase x) ^ (n + 1) / (n + 1 : ℂ))      atTop (𝓝 L) := by    refine hL.congr' (Eventually.of_forall fun N ↦ ?_)    apply Finset.sum_congr rfl    intro n _hn    exact one_div_nat_smul_eq_div n ((expPhase x) ^ (n + 1))  have hAbel := Complex.tendsto_tsum_powerSeries_nhdsWithin_lt hL_div  rw [tendsto_map'_iff] at hAbel  have h_ofReal : Tendsto (fun r : ℝ ↦ (r : ℂ)) (𝓝[<] (1 : ℝ)) (𝓝 (1 : ℂ)) :=    tendsto_nhdsWithin_of_tendsto_nhds (Complex.continuous_ofReal.tendsto 1)  have h_arg : Tendsto (fun r : ℝ ↦ 1 - (r : ℂ) * expPhase x) (𝓝[<] (1 : ℝ))      (𝓝 (1 - expPhase x)) := by    simpa using tendsto_const_nhds.sub (h_ofReal.mul tendsto_const_nhds)  have h_log : Tendsto (fun r : ℝ ↦ -Complex.log (1 - (r : ℂ) * expPhase x) / (r : ℂ))      (𝓝[<] (1 : ℝ)) (𝓝 (-Complex.log (1 - expPhase x))) := by    simpa using! ((continuousAt_clog (one_sub_expPhase_mem_slitPlane hx)).tendsto.comp      h_arg).neg.div h_ofReal (by norm_num : (1 : ℂ) ≠ 0)  have h_power_log : Tendsto      (fun r : ℝ ↦ ∑' n : ℕ,        (expPhase x) ^ (n + 1) / (n + 1 : ℂ) * (r : ℂ) ^ n)      (𝓝[<] (1 : ℝ)) (𝓝 (-Complex.log (1 - expPhase x))) := by    refine h_log.congr' ?_    filter_upwards [Ioo_mem_nhdsLT (show (0 : ℝ) < 1 by norm_num)] with r hr    symm    have hr0 : (r : ℂ) ≠ 0 := by exact_mod_cast (ne_of_gt hr.1)    have hnorm : ‖(r : ℂ) * expPhase x‖ < 1 := by      calc        ‖(r : ℂ) * expPhase x‖ = ‖(r : ℂ)‖ * ‖expPhase x‖ := norm_mul _ _        _ = |r| * 1 := by rw [Complex.norm_real, Real.norm_eq_abs, norm_exp_two_pi_mul_I]        _ = r := by rw [abs_of_pos hr.1]; ring        _ < 1 := hr.2    exact tsum_expPhase_power_eq_neg_log_div (x := x) (r := r) hr0 hnorm  have hL_eq : L = -Complex.log (1 - expPhase x) :=    tendsto_nhds_unique hAbel h_power_log  simpa [expPhase, hL_eq] using hL