Source indexedtheorem · leanprover/lean4:v4.32.0

ArithmeticFunction.sum_moebius_pmul_eq_prod_one_sub

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:99 to 145

Source documentation

If g is a multiplicative arithmetic function, then for any $n \neq 0$ , $\sum_{d | n} \mu(d) \cdot g(d) = \prod_{p | n} (1 - g(p))$ .

Exact Lean statement

@[blueprint
  "sum_moebius_pmul_eq_prod_one_sub"
  (title := "sum moebius pmul eq prod one sub")
  (statement := /-- If $g$ is a multiplicative arithmetic function, then for any $n \neq 0$,
    $\sum_{d | n} \mu(d) \cdot g(d) = \prod_{p | n} (1 - g(p))$.
      \begin{verbatim}
  Upstream issue has been created #1240.
  \end{verbatim}

    -/)
  (proof := /--
  Multiply out and collect terms.
  -/)]
theorem sum_moebius_pmul_eq_prod_one_sub {R : Type*} [CommRing R]
    {g : ArithmeticFunction R} (hg : g.IsMultiplicative) (n : ℕ) : n ≠ 0 →
    ∑ d ∈ n.divisors, (moebius d : R) * g d = ∏ p ∈ n.primeFactors, (1 - g p)

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "sum_moebius_pmul_eq_prod_one_sub"  (title := "sum moebius pmul eq prod one sub")  (statement := /-- If $g$ is a multiplicative arithmetic function, then for any $n \neq 0$,    $\sum_{d | n} \mu(d) \cdot g(d) = \prod_{p | n} (1 - g(p))$.      \begin{verbatim}  Upstream issue has been created #1240.  \end{verbatim}     -/)  (proof := /--  Multiply out and collect terms.  -/)]theorem sum_moebius_pmul_eq_prod_one_sub {R : Type*} [CommRing R]    {g : ArithmeticFunction R} (hg : g.IsMultiplicative) (n : ℕ) : n ≠ 0 →    ∑ d ∈ n.divisors, (moebius d : R) * g d = ∏ p ∈ n.primeFactors, (1 - g p) := by  induction n using Nat.recOnPosPrimePosCoprime with  | zero => intro h; exact absurd rfl h  | one => exact fun _ ↦ by simp [hg.map_one]  | prime_pow p k hp hk =>    refine fun _ ↦ ?_    rw [Nat.primeFactors_prime_pow hk.ne' hp, Finset.prod_singleton, sum_divisors_prime_pow hp,      Finset.sum_range_succ']    simp only [pow_zero, moebius_apply_one, Int.cast_one, hg.map_one, mul_one]    rw [Finset.sum_eq_single_of_mem 0 (Finset.mem_range.mpr hk)]    · simp only [zero_add, pow_one, moebius_apply_prime hp, Int.reduceNeg, Int.cast_neg,        Int.cast_one, neg_mul, one_mul]; ring    · intro i _ hi      have hnsq : ¬Squarefree (p ^ (i + 1)) := by        rw [Nat.squarefree_pow_iff hp.ne_one (by omega : i + 1 ≠ 0)]        omega      rw [moebius_eq_zero_of_not_squarefree hnsq]      simp  | coprime a b ha hb hab iha ihb =>    intro hn    rw [hab.primeFactors_mul, Finset.prod_union hab.disjoint_primeFactors,        ← iha (by omega), ← ihb (by omega)]    let h : ArithmeticFunction R := ⟨fun n ↦ ↑(moebius n) * g n, by simp⟩    have h_mul : h.IsMultiplicative := by      refine ⟨?_, ?_⟩      · simp [h, ArithmeticFunction.coe_mk, hg.left]      · intro m n hmn        simp only [h, ArithmeticFunction.coe_mk]        rw [ArithmeticFunction.isMultiplicative_moebius.right hmn, hg.right hmn]        push_cast        ring    exact sum_divisors_mul_of_coprime h_mul hab (by omega) (by omega)