Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.sum_moebius_sq_divisors_apply_prime_pow

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:1325 to 1361

Mathematical statement

Exact Lean statement

@[blueprint
  "sum_moebius_sq_divisors_apply_prime_pow"
  (title := "sum-moebius-sq-divisors-apply-prime-pow")
  (statement := /-- Applied at prime powers, sum-moebius-sq-divisors coincides with $\mu^2$. -/)
  (proof := /--
    For a prime power $p^k$, note that if $k\leq 1$ then the only square divisor is $1$, so the sum
    evaluates as $\mu(1)=1$. If $k\geq 2$, then $1$ and $p^2$ are square divisors of $p^k$. Thus,
    the sum evaluates as $\mu(1)+\mu(p)+\ldots$ where the remaining terms are moebius of higher
    powers (if necessary). Since $\mu(p)=-1$ and $\mu$ of higher powers of $p$ is zero, this is
    $0$. This agrees with $\mu(p^k)^2$, which is simply an indicator function for $k\leq 1$ (i.e.
    $p^k$ is squarefree).
  -/)]
lemma sum_moebius_sq_divisors_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) :
  sum_moebius_sq_divisors (p ^ k) = (μ (p ^ k)) ^ 2

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "sum_moebius_sq_divisors_apply_prime_pow"  (title := "sum-moebius-sq-divisors-apply-prime-pow")  (statement := /-- Applied at prime powers, sum-moebius-sq-divisors coincides with $\mu^2$. -/)  (proof := /--    For a prime power $p^k$, note that if $k\leq 1$ then the only square divisor is $1$, so the sum    evaluates as $\mu(1)=1$. If $k\geq 2$, then $1$ and $p^2$ are square divisors of $p^k$. Thus,    the sum evaluates as $\mu(1)+\mu(p)+\ldots$ where the remaining terms are moebius of higher    powers (if necessary). Since $\mu(p)=-1$ and $\mu$ of higher powers of $p$ is zero, this is    $0$. This agrees with $\mu(p^k)^2$, which is simply an indicator function for $k\leq 1$ (i.e.    $p^k$ is squarefree).  -/)]lemma sum_moebius_sq_divisors_apply_prime_pow {p k : ℕ} (hp : Nat.Prime p) :  sum_moebius_sq_divisors (p ^ k) = (μ (p ^ k)) ^ 2 := by  have h_filter : ((Nat.divisors (p ^ k)).filter (fun x => x ^ 2 ∣ p ^ k)) = Finset.image (fun j => p ^ j) (Finset.range (k / 2 + 1)) := by    ext; simp only [Nat.divisors_prime_pow hp, mem_filter, mem_map, mem_range, Order.lt_add_one_iff, Function.Embedding.coeFn_mk, mem_image]    constructor    · rintro ⟨⟨a, ha, rfl⟩, h⟩      exact ⟨a, Nat.le_div_iff_mul_le zero_lt_two |>.2 <| by        rw [← pow_mul] at h        exact Nat.le_of_not_lt fun ha' => absurd (Nat.le_of_dvd (pow_pos hp.pos _) h)          (not_le_of_gt (pow_lt_pow_right₀ hp.one_lt ha')), rfl⟩    · rintro ⟨a, ha, rfl⟩      exact ⟨⟨a, by omega, rfl⟩, by rw [← pow_mul]; exact pow_dvd_pow _ (by omega)⟩  simp only [moebius_sq, sum_moebius_sq_divisors_apply, h_filter]  rw [Finset.sum_image <| by intros a ha b hb hab; exact Nat.pow_right_injective hp.two_le hab, Finset.sum_range_succ']  split_ifs with h  · have hk : k / 2 = 0 := by      rw [Nat.div_eq_zero_iff, or_iff_right (two_ne_zero)]      by_contra hk      exact absurd h (by rw [Nat.squarefree_pow_iff hp.ne_one (by omega)]; exact not_and_of_not_right _ (by linarith))    simp [hk]  · simp only [pow_zero, isUnit_iff_eq_one, IsUnit.squarefree, moebius_apply_of_squarefree, Int.reduceNeg, cardFactors_one]    rcases k with _ | _ | _    · simp at ⊢ h    · simp [hp.squarefree] at ⊢ h    · simp_all +decide [ArithmeticFunction.moebius_apply_prime_pow]