primeCounting_mono

formal source

 399  native_decide
 400
 401/-- π is monotone: m ≤ n → π(m) ≤ π(n). -/
 402theorem primeCounting_mono {m n : ℕ} (h : m ≤ n) : primeCounting m ≤ primeCounting n := by
 403  simp only [primeCounting]
 404  exact Nat.monotone_primeCounting h
 405
 406/-! ### Liouville-squarefree connection -/
 407
 408/-- For squarefree n, λ(n) = μ(n). -/
 409theorem liouville_eq_mobius_of_squarefree {n : ℕ} (hn : n ≠ 0) (hsq : Squarefree n) :
 410    liouville n = mobius n := by
 411  rw [liouville_eq hn, mobius_apply_of_squarefree hsq, bigOmega_eq_omega_of_squarefree hn hsq]
 412
 413/-- μ(n)² = 1 iff n is squarefree. -/
 414theorem mobius_sq_eq_one_iff_squarefree {n : ℕ} : mobius n ^ 2 = 1 ↔ Squarefree n := by
 415  constructor
 416  · intro h
 417    by_contra hnsq
 418    have hμ : mobius n = 0 := mobius_eq_zero_of_not_squarefree hnsq
 419    simp [hμ] at h
 420  · intro hsq
 421    -- μ(n) ∈ {-1, 1} for squarefree n, so μ(n)² = 1
 422    have h_val := mobius_apply_of_squarefree hsq
 423    rw [h_val, ← pow_mul, mul_comm]
 424    have h_even : Even (2 * bigOmega n) := even_two_mul (bigOmega n)
 425    exact Even.neg_one_pow h_even
 426
 427/-! ### Values at 1 -/
 428
 429/-- μ(1) = 1. -/
 430theorem mobius_one : mobius 1 = 1 := by
 431  simp [mobius]
 432