Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.two_pow_omega_LSeries_eulerProduct_tprod

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:938 to 961

Mathematical statement

Exact Lean statement

@[blueprint
  "two_pow_omega_LSeries_eulerProduct_tprod"
  (title := "two-pow-omega-LSeries-eulerProduct-tprod")
  (statement := /--
    For $1<\Re(s)$ we have that
    $$\sum_{1\leq n}2^{\omega(n)}n^{-s}=\prod_p\frac{1+p^{-s}}{1-p^{-s}}.$$
    The naming convention here is designed to match
    \begin{verbatim}
      riemannZeta_eulerProduct_tprod
    \end{verbatim}
  -/)
  (proof := /--
    Immediately follows from Lemmas \ref{two-pow-omega-LSeries.term-IsMultiplicative} and \ref{two-pow-omega-tsum-prime-pow}.
  -/)]
lemma two_pow_omega_LSeries_eulerProduct_tprod (s : ℂ) (hs : 1 < s.re) :
    LSeries (fun n ↦ 2 ^ (ω n)) s = ∏' (p : Primes), (1 + (p : ℂ) ^ (-s)) / (1 - (p : ℂ) ^ (-s))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "two_pow_omega_LSeries_eulerProduct_tprod"  (title := "two-pow-omega-LSeries-eulerProduct-tprod")  (statement := /--    For $1<\Re(s)$ we have that    $$\sum_{1\leq n}2^{\omega(n)}n^{-s}=\prod_p\frac{1+p^{-s}}{1-p^{-s}}.$$    The naming convention here is designed to match    \begin{verbatim}      riemannZeta_eulerProduct_tprod    \end{verbatim}  -/)  (proof := /--    Immediately follows from Lemmas \ref{two-pow-omega-LSeries.term-IsMultiplicative} and \ref{two-pow-omega-tsum-prime-pow}.  -/)]lemma two_pow_omega_LSeries_eulerProduct_tprod (s : ℂ) (hs : 1 < s.re) :    LSeries (fun n ↦ 2 ^ (ω n)) s = ∏' (p : Primes), (1 + (p : ℂ) ^ (-s)) / (1 - (p : ℂ) ^ (-s)) := by  convert! HasProd.tprod_eq ( EulerProduct.eulerProduct_hasProd (R := ℂ) ?_ ?_ _ _ ) |> Eq.symm using 1  · apply tprod_congr    simp only [← two_pow_omega_tsum_prime_pow hs, sumOnPrimePows_apply, implies_true]  · simp only [ne_eq, one_ne_zero, not_false_eq_true, LSeries.term_of_ne_zero,      cardDistinctFactors_one, pow_zero, cast_one, Complex.one_cpow, div_self]  · intro m n mCn; exact two_pow_omega_LSeries.term_isMultiplicative s mCn  · convert! (LSeriesSummable_two_pow_omega hs).norm using 1  · unfold LSeries.term; simp only [↓reduceIte]