ArithmeticFunction.two_pow_omega_tsum_prime_pow

@[blueprint  "two_pow_omega_tsum_prime_pow"  (title := "two-pow-omega-tsum-prime-pow")  (statement := /--    For $1<\Re(s)$ and $p$ prime, we have that    $$\sum_{0\leq k}2^{\omega(p^k)}p^{-ks}=\frac{1+p^{-s}}{1-p^{-s}}.$$  -/)  (proof := /--    Note that $\omega(p^0)=0$ and $\omega(p^k)=1$ whenever $0<k$. Thus,    $$\sum_{0\leq k}2^{\omega(p^k)}p^{-ks}=1+2p^{-s}+2p^{-2s}+\ldots.$$    Now apply a geometric sum to the non-constant terms and simplify. We have the necessary    convergence as $1<\Re(s)$.  -/)]lemma two_pow_omega_tsum_prime_pow {s : ℂ} (hs : 1 < s.re)    (p : Primes) : sumOnPrimePows (LSeries.term (fun n ↦ 2 ^ (ω n)) s) p = (1 + (p : ℂ) ^ (-s)) / (1 - (p : ℂ) ^ (-s)) := by  have h_rw : sumOnPrimePows (LSeries.term (fun n ↦ 2 ^ (ω n)) s) p = 1 + ∑' e : ℕ, LSeries.term (fun n : ℕ => 2 ^ (ω n)) s (p.val ^ (e + 1)) := by    rw [sumOnPrimePows_apply, Summable.tsum_eq_zero_add];    · unfold LSeries.term      simp [Nat.Prime.ne_zero p.prop]    · have := LSeriesSummable_two_pow_omega hs;      convert! this.comp_injective (show Function.Injective (fun e : ℕ => p.val ^ e) from fun a b h => Nat.pow_right_injective p.prop.one_lt h) using 1  have h_term_eval : ∀ e : ℕ, LSeries.term (fun n : ℕ => 2 ^ ω n) s (p.val ^ (e + 1)) = 2 * (p.val : ℂ) ^ (-(e + 1) * s) := by    intro e    simp only [neg_mul, LSeries.term, Nat.pow_eq_zero, ne_eq, cast_pow, Nat.Prime.ne_zero p.prop, false_and, ↓reduceIte]    rw [ArithmeticFunction.cardDistinctFactors_apply_prime_pow p.prop, pow_one]    · simp only [Complex.cpow_neg, div_eq_mul_inv, ← Complex.natCast_cpow_natCast_mul, cast_add, cast_one]    · linarith  have geo_series_rw : ∑' e : ℕ, (p.val : ℂ) ^ (-(e + 1) * s) = (p.val : ℂ) ^ (-s) / (1 - (p.val : ℂ) ^ (-s)) := by    rw [div_eq_mul_inv, ← tsum_geometric_of_norm_lt_one]    · rw [← tsum_mul_left]; congr; ext n; rw [← Complex.cpow_nat_mul]; ring_nf      rw [← Complex.cpow_add _ _ (Nat.cast_ne_zero.mpr p.prop.ne_zero)]; ring_nf    · rw [Complex.norm_cpow_of_ne_zero] <;> norm_num [p.2.ne_zero]      exact lt_of_lt_of_le (Real.rpow_lt_rpow_of_exponent_lt (mod_cast p.2.one_lt) (neg_lt_zero.mpr (by linarith))) (by norm_num)  simp only [h_rw, h_term_eval, geo_series_rw, tsum_mul_left]  rw [eq_div_iff, add_mul, one_mul, ← mul_div_assoc, div_mul_cancel₀]  · ring_nf  all_goals (exact Complex.one_sub_prime_cpow_ne_zero p.2 hs)