ZetaAppendix.lemma_abadsumas_summable_alternating_theta

lemma lemma_abadsumas_summable_alternating_theta (θ : ℝ) (hθ : |θ| < 1) :    Summable (fun n : ℕ ↦ ((-1) ^ (n + 2) * 2 * θ / ((n + 1) ^ 2 - θ ^ 2) : ℂ)) := by  have hθ_sq_lt : θ ^ 2 < 1 := by nlinarith [sq_abs θ, abs_nonneg θ]  apply Summable.of_norm_bounded (g := fun n : ℕ => 2 * |θ| / ((1 - θ ^ 2) * ((n : ℝ) + 1) ^ 2))  · apply Summable.mul_left    have hpos : (0 : ℝ) < 1 - θ ^ 2 := by nlinarith [sq_abs θ, abs_nonneg θ]    simp_rw [mul_inv]    apply Summable.mul_left    have hbase : Summable (fun n : ℕ => (n ^ 2 : ℝ)⁻¹) := by      simp_rw [inv_eq_one_div]      norm_cast      simp_rw [Nat.cast_pow] at ⊢      apply Real.summable_one_div_nat_pow.mpr (by norm_num)    exact (summable_nat_add_iff 1).mpr hbase |>.congr      (fun n => by push_cast; ring_nf)  · intro n    have hdenom_pos : (0 : ℝ) < (n + 1) ^ 2 - θ ^ 2 := by      have : (0 : ℝ) ≤ (↑n : ℝ) := Nat.cast_nonneg n      nlinarith [sq_nonneg (n : ℝ)]    rw [show ‖(-1 : ℂ) ^ (n + 2) * 2 * θ / ((n + 1) ^ 2 - θ ^ 2)‖ = 2 * |θ| / (((n : ℝ) + 1) ^ 2 - θ ^ 2) by      have h2 : ‖(2 : ℂ)‖ = 2 := by norm_num      rw [norm_div, norm_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, h2,          one_mul, Complex.norm_real, norm_eq_abs]      congr 1      rw [show (↑n + 1 : ℂ) ^ 2 - (↑θ : ℂ) ^ 2 = ↑((↑n + 1 : ℝ) ^ 2 - θ ^ 2) by norm_cast,          Complex.norm_real, Real.norm_eq_abs, abs_of_pos hdenom_pos]]    have hdenom_ineq : (1 - θ ^ 2) * (n + 1) ^ 2 ≤ (n + 1) ^ 2 - θ ^ 2 := by      have h_cast : (0 : ℝ) ≤ (↑n : ℝ) := Nat.cast_nonneg n      have h_ge_one : (1 : ℝ) ≤ ↑n + 1 := by linarith      have h_sq_ge : (1 : ℝ) ≤ (↑n + 1) ^ 2 := by nlinarith      nlinarith [sq_nonneg θ]    have h2 : (0 : ℝ) < 1 - θ ^ 2 := by linarith    gcongr