Source indexedlemma · leanprover/lean4:v4.32.0

ArithmeticFunction.two_pow_omega_le_sigma_zero

PrimeNumberTheoremAnd.IwaniecKowalskiCh1 · PrimeNumberTheoremAnd/IwaniecKowalskiCh1.lean:724 to 745

Mathematical statement

Exact Lean statement

@[blueprint
  "two_pow_omega_le_sigma_zero"
  (title := "two-pow-omega-le-sigma-zero")
  (statement := /--
    We have the inequality $2^{\omega(n)}\leq\sigma_0(n)$ when $n\neq 0$.
  -/)
  (proof := /--
    Recall that $\omega(n)$ is the number of distinct prime factors of $n$. Thus,
    $$2^{\omega(n)}=\prod_{p|n}2.$$
    Likewise, $\sigma_0(n)$ is the number of divisors of $n$. We can write this as
    $$\prod_{p|n}(1+v_p(n))=\sigma_0(n)$$
    where $v_p(n)$ denotes the $p$-adic valuation of $n$. For $p|n$ we have that $2\leq 1+v_p(n)$.
    Thus the result immediately follows.
  -/)]
lemma two_pow_omega_le_sigma_zero {n : ℕ} (hn : n ≠ 0) :
    2 ^ (ω n) ≤ σ 0 n

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

@[blueprint  "two_pow_omega_le_sigma_zero"  (title := "two-pow-omega-le-sigma-zero")  (statement := /--    We have the inequality $2^{\omega(n)}\leq\sigma_0(n)$ when $n\neq 0$.  -/)  (proof := /--    Recall that $\omega(n)$ is the number of distinct prime factors of $n$. Thus,    $$2^{\omega(n)}=\prod_{p|n}2.$$    Likewise, $\sigma_0(n)$ is the number of divisors of $n$. We can write this as    $$\prod_{p|n}(1+v_p(n))=\sigma_0(n)$$    where $v_p(n)$ denotes the $p$-adic valuation of $n$. For $p|n$ we have that $2\leq 1+v_p(n)$.    Thus the result immediately follows.  -/)]lemma two_pow_omega_le_sigma_zero {n : ℕ} (hn : n ≠ 0) :    2 ^ (ω n) ≤ σ 0 n := by  rw [show ω n = (Nat.primeFactors n).card from rfl, ArithmeticFunction.sigma_zero_apply, Nat.card_divisors hn, ← Finset.prod_const]  apply Finset.prod_le_prod'  intro p hp  simpa [two_mul] using  (Nat.Prime.dvd_iff_one_le_factorization (prime_of_mem_primeFactors hp) hn).mp    (dvd_of_mem_primeFactors hp)