ZetaAppendix.exp_geometric_partial_sums_bounded

lemma exp_geometric_partial_sums_bounded {x : ℝ} (hx : ¬ ∃ k : ℤ, x = k) :    ∃ C : ℝ, 0 ≤ C ∧      ∀ N : ℕ,        ‖∑ n ∈ range N, (Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)) ^ n‖ ≤ C := by  let z : ℂ := Complex.exp ((2 * Real.pi * x : ℝ) * Complex.I)  have hz_ne_one : z ≠ 1 := exp_two_pi_mul_I_ne_one_of_not_int hx  have hz_norm : ‖z‖ = 1 := norm_exp_two_pi_mul_I x  refine ⟨2 / ‖z - 1‖, ?_, fun N ↦ ?_⟩  · positivity  calc    ‖∑ n ∈ range N, z ^ n‖        = ‖(z ^ N - 1) / (z - 1)‖ := by rw [geom_sum_eq hz_ne_one]    _ = ‖z ^ N - 1‖ / ‖z - 1‖ := norm_div _ _    _ ≤ (‖z ^ N‖ + ‖(1 : ℂ)‖) / ‖z - 1‖ := by      gcongr      exact norm_sub_le _ _    _ = 2 / ‖z - 1‖ := by norm_num [norm_pow, hz_norm]