Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.moebius_sq_LSeries_eulerProduct_tprod

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1126 to 1150

Mathematical statement

Exact Lean statement

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

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "moebius_sq_LSeries_eulerProduct_tprod"  (title := "moebius-sq-LSeries-eulerProduct-tprod")  (statement := /--    For $1<\Re(s)$ we have that    $$\sum_{1\leq n}\mu^2(n)n^{-s}=\prod_p(1+p^{-s}).$$    The naming convention here is designed to match    \begin{verbatim}      riemannZeta_eulerProduct_tprod    \end{verbatim}  -/)  (proof := /--    Immediately follows from Lemmas \ref{moebius-sq-LSeries.term-IsMultiplicative} and \ref{moebius-sq-tsum-prime-pow}.  -/)]lemma moebius_sq_LSeries_eulerProduct_tprod (s : ℂ) (hs : 1 < s.re) :    LSeries (fun n ↦ (μ n) ^ 2) s = ∏' (p : Primes), (1 + (p : ℂ) ^ (-s)) := by  convert! (EulerProduct.eulerProduct_hasProd (R := ℂ) ?_ ?_ _ _).tprod_eq.symm using 1  · apply tprod_congr    simp only [← moebius_sq_tsum_prime_pow, sumOnPrimePows_apply, implies_true]  · simp only [ne_eq, one_ne_zero, not_false_eq_true, LSeries.term_of_ne_zero, isUnit_iff_eq_one,      IsUnit.squarefree, moebius_apply_of_squarefree, Int.reduceNeg, cardFactors_one, pow_zero,      Int.cast_one, one_pow, cast_one, Complex.one_cpow, div_self]  · intro m n mCn; exact moebius_sq_LSeries.term_isMultiplicative s mCn  · convert! (LSeriesSummable_moebius_sq hs).norm using 1  · unfold LSeries.term; simp only [↓reduceIte]