theorem
proved
primeCounting_twenty
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.Primes.ArithmeticFunctions on GitHub at line 394.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
391 native_decide
392
393/-- π(20) = 8. -/
394theorem primeCounting_twenty : primeCounting 20 = 8 := by
395 native_decide
396
397/-- π(100) = 25. -/
398theorem primeCounting_hundred : primeCounting 100 = 25 := by
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)