norm_dirichletApproxAux_le_of_re_nonneg

lemma norm_dirichletApproxAux_le_of_re_nonneg {n : ℕ} {x r : ℝ} (hx : exp (I * x) ≠ 1)    (h'x : 0 ≤ re (exp (I * x))) (hn : r⁻¹ ≤ n) (hr : 0 < r) :    ‖dirichletApproxAux n x‖ ≤ 2 * (1 + r / ‖1 - exp (I * x)‖ ^ 2) := by  have A (k : ℕ) : exp (I * 2 * k * x) = (exp (I * (2 * x : ℝ))) ^ k := by    rw [← exp_nat_mul]    simp [mul_assoc]    ring_nf  have B : ‖1 - exp (I * x)‖ ≤ ‖exp (I * (2 * x : ℝ)) - 1‖ := by    have : exp (I * (2 * x : ℝ)) - 1 =          - ((1 - exp (I * x)) * (exp (I * x) + 1)) := by      rw [show I * (2 * x : ℝ) = I * x + I * x by simp; ring, exp_add]      ring    rw [this, norm_neg, norm_mul]    apply le_mul_of_one_le_right (norm_nonneg _)    apply le_trans _ (re_le_norm _)    simpa using h'x  have C : exp (I * (2 * x : ℝ)) ≠ 1 := by    intro h    simp only [h, sub_self, norm_zero, norm_le_zero_iff, sub_eq_zero] at B    exact hx B.symm  calc  ‖dirichletApproxAux n x‖  _ = (n : ℝ)⁻¹ * ‖1 - exp (I * x)‖⁻¹ * ‖∑ k ∈ Finset.range n, exp (I * (2 * x : ℝ)) ^ k‖ := by    simp only [dirichletApproxAux, neg_mul, A, Nat.Ico_zero_eq_range, Complex.norm_mul,      Complex.norm_div, norm_inv, norm_natCast, norm_pow, norm_exp_I_mul_ofReal,      norm_one_sub_exp_neg_I_mul_ofReal]    simp only [one_pow, mul_one, ofReal_mul, ofReal_ofNat, div_eq_mul_inv]  _ = (n : ℝ)⁻¹ * ‖1 - exp (I * x)‖⁻¹ *      ‖(exp (I * (2 * x : ℝ)) ^ n - 1) / (exp (I * (2 * x : ℝ)) - 1)‖ := by    rw [geom_sum_eq C]  _ ≤ (n : ℝ)⁻¹ * ‖1 - exp (I * x)‖⁻¹ * (2 * ‖(exp (I * (2 * x : ℝ)) - 1)‖⁻¹) := by    rw [div_eq_mul_inv, norm_mul, norm_inv]    gcongr    apply (norm_sub_le _ _).trans_eq    rw [norm_pow, norm_exp_I_mul_ofReal]    simpa using by norm_num  _ ≤ r * ‖1 - exp (I * x)‖⁻¹ * (2 * ‖1 - exp (I * x)‖⁻¹) := by    gcongr    · exact inv_le_of_inv_le₀ hr hn    · simpa [sub_eq_zero] using hx.symm  _ = 2 * (0 + r / ‖1 - exp (I * x)‖ ^ 2) := by    rw [pow_two, div_eq_inv_mul, mul_inv]    ring  _ ≤ 2 * (1 + r / ‖1 - exp (I * x)‖ ^ 2) := by    gcongr    norm_num