Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.moebius_sq_eq

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1364 to 1377

Source documentation

I-K (1.33): μ^2(n) = ∑ d^2|n μ(d).

Exact Lean statement

@[blueprint
  "moebius_sq_eq"
  (title := "moebius-sq-eq")
  (statement := /-- I-K (1.33): $\mu^2(n) = \sum_{d^2|n} \mu(d)$. -/)
  (proof := /-- Apply the previous two lemmas. -/)]
lemma moebius_sq_eq (n : ℕ) : (μ n) ^ 2 = ∑ d ∈ n.divisors.filter (fun x => x ^ 2 ∣ n), μ d

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "moebius_sq_eq"  (title := "moebius-sq-eq")  (statement := /-- I-K (1.33): $\mu^2(n) = \sum_{d^2|n} \mu(d)$. -/)  (proof := /-- Apply the previous two lemmas. -/)]lemma moebius_sq_eq (n : ℕ) : (μ n) ^ 2 = ∑ d ∈ n.divisors.filter (fun x => x ^ 2 ∣ n), μ d := by  by_cases n_zero : n = 0  · simp [n_zero]  · rw[← sum_moebius_sq_divisors_apply, IsMultiplicative.multiplicative_factorization sum_moebius_sq_divisors sum_moebius_sq_divisors_IsMultiplicative n_zero]    have hpf : ∀ p ∈ n.factorization.support, Nat.Prime p :=      fun p hp => Nat.prime_of_mem_primeFactors (Nat.support_factorization n ▸ hp)    simp only [Finset.prod_pow, Finsupp.prod, Nat.support_factorization, Finset.prod_congr rfl (fun x hx =>      sum_moebius_sq_divisors_apply_prime_pow ((Nat.support_factorization n ▸ hpf) x hx))]    congr; exact IsMultiplicative.multiplicative_factorization μ isMultiplicative_moebius n_zero