Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.moebius_sq_LSeries_eulerProduct_hasProd

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1152 to 1174

Mathematical statement

Exact Lean statement

@[blueprint
  "moebius_sq_LSeries_eulerProduct_hasProd"
  (title := "moebius-sq-LSeries-eulerProduct-hasProd")
  (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_hasProd
    \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_hasProd (s : ℂ) (hs : 1 < s.re) :
    HasProd (fun (p : Primes) ↦ (1 + ↑↑p ^ (-s))) (L (fun n ↦ (μ n) ^ 2) s)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "moebius_sq_LSeries_eulerProduct_hasProd"  (title := "moebius-sq-LSeries-eulerProduct-hasProd")  (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_hasProd    \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_hasProd (s : ℂ) (hs : 1 < s.re) :    HasProd (fun (p : Primes) ↦ (1 + ↑↑p ^ (-s))) (L (fun n ↦ (μ n) ^ 2) s) := by  convert! EulerProduct.eulerProduct_hasProd _ _ _ (LSeries.term_zero (fun n ↦ (μ n) ^ 2) s) using 1;  · funext p; exact Eq.symm (moebius_sq_tsum_prime_pow p)  · 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 _ _ mCn; exact moebius_sq_LSeries.term_isMultiplicative s mCn  · convert! (LSeriesSummable_moebius_sq hs).norm using 1