feat(number_theory/prime_counting): The prime counting function (#9080)

With an eye to implementing [this proof](https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238002/near/251178921), I am adding a file to define the prime counting function and prove a simple upper bound on it.



Co-authored-by: Vladimir Goryachev <gor050299@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: YaelDillies <yael.dillies@gmail.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Eric <ericrboidi@gmail.com>

src/data/nat/totient.lean

@@ -7,6 +7,7 @@ import algebra.big_operators.basic
 import data.nat.prime
 import data.zmod.basic
 import ring_theory.multiplicity
+import data.nat.periodic
 import algebra.char_p.two
 
 /-!
@@ -26,7 +27,7 @@ namespace nat
 
 /-- Euler's totient function. This counts the number of naturals strictly less than `n` which are
 coprime with `n`. -/
-def totient (n : ℕ) : ℕ := ((range n).filter (nat.coprime n)).card
+def totient (n : ℕ) : ℕ := ((range n).filter n.coprime).card
 
 localized "notation `φ` := nat.totient" in nat
 
@@ -35,7 +36,7 @@ localized "notation `φ` := nat.totient" in nat
 @[simp] theorem totient_one : φ 1 = 1 :=
 by simp [totient]
 
-lemma totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter (nat.coprime n)).card := rfl
+lemma totient_eq_card_coprime (n : ℕ) : φ n = ((range n).filter n.coprime).card := rfl
 
 lemma totient_le (n : ℕ) : φ n ≤ n :=
 calc totient n ≤ (range n).card : card_filter_le _ _
@@ -57,6 +58,44 @@ lemma totient_pos : ∀ {n : ℕ}, 0 < n → 0 < φ n
 | 1 := by simp [totient]
 | (n+2) := λ h, card_pos.2 ⟨1, mem_filter.2 ⟨mem_range.2 dec_trivial, coprime_one_right _⟩⟩
 
+lemma filter_coprime_Ico_eq_totient (a n : ℕ) :
+  ((Ico n (n+a)).filter (coprime a)).card = totient a :=
+begin
+  rw [totient, filter_Ico_card_eq_of_periodic, count_eq_card_filter_range],
+  exact periodic_coprime a,
+end
+
+lemma Ico_filter_coprime_le {a : ℕ} (k n : ℕ) (a_pos : 0 < a) :
+  ((Ico k (k + n)).filter (coprime a)).card ≤ totient a * (n / a + 1) :=
+begin
+  conv_lhs { rw ←nat.mod_add_div n a },
+  induction n / a with i ih,
+  { rw ←filter_coprime_Ico_eq_totient a k,
+    simp only [add_zero, mul_one, mul_zero, le_of_lt (mod_lt n a_pos)],
+    mono,
+    refine monotone_filter_left a.coprime _,
+    simp only [finset.le_eq_subset],
+    exact Ico_subset_Ico rfl.le (add_le_add_left (le_of_lt (mod_lt n a_pos)) k), },
+  simp only [mul_succ],
+  simp_rw ←add_assoc at ih ⊢,
+  calc (filter a.coprime (Ico k (k + n % a + a * i + a))).card
+      = (filter a.coprime (Ico k (k + n % a + a * i)
+                            ∪ Ico (k + n % a + a * i) (k + n % a + a * i + a))).card :
+        begin
+          congr,
+          rw Ico_union_Ico_eq_Ico,
+          rw add_assoc,
+          exact le_self_add,
+          exact le_self_add,
+        end
+  ... ≤ (filter a.coprime (Ico k (k + n % a + a * i))).card + a.totient :
+        begin
+          rw [filter_union, ←filter_coprime_Ico_eq_totient a (k + n % a + a * i)],
+          apply card_union_le,
+        end
+  ... ≤ a.totient * i + a.totient + a.totient : add_le_add_right ih (totient a),
+end
+
 open zmod
 
 /-- Note this takes an explicit `fintype ((zmod n)ˣ)` argument to avoid trouble with instance

src/number_theory/prime_counting.lean

@@ -0,0 +1,87 @@
+/-
+Copyright (c) 2021 Bolton Bailey. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Bolton Bailey
+-/
+
+import data.nat.prime
+import data.nat.totient
+import algebra.periodic
+import data.finset.locally_finite
+import data.nat.count
+
+
+/-!
+# The Prime Counting Function
+
+In this file we define the prime counting function: the function on natural numbers that returns
+the number of primes less than or equal to its input.
+
+## Main Results
+
+The main definitions for this file are
+
+- `nat.prime_counting`: The prime counting function π
+- `nat.prime_counting'`: π(n - 1)
+
+We then prove that these are monotone in `nat.monotone_prime_counting` and
+`nat.monotone_prime_counting'`. The last main theorem `nat.prime_counting'_add_le` is an upper
+bound on `π'` which arises by observing that all numbers greater than `k` and not coprime to `k`
+are not prime, and so only at most `φ(k)/k` fraction of the numbers from `k` to `n` are prime.
+
+## Notation
+
+We use the standard notation `π` to represent the prime counting function (and `π'` to represent
+the reindexed version).
+
+-/
+
+namespace nat
+open finset
+
+/--
+A variant of the traditional prime counting function which gives the number of primes
+*strictly* less than the input. More convenient for avoiding off-by-one errors.
+-/
+def prime_counting' : ℕ → ℕ := nat.count prime
+
+/-- The prime counting function: Returns the number of primes less than or equal to the input. -/
+def prime_counting (n : ℕ) : ℕ := prime_counting' (n + 1)
+
+localized "notation `π` := nat.prime_counting" in nat
+localized "notation `π'` := nat.prime_counting'" in nat
+
+lemma monotone_prime_counting' : monotone prime_counting' := count_monotone prime
+
+lemma monotone_prime_counting : monotone prime_counting :=
+λ a b a_le_b, monotone_prime_counting' (add_le_add_right a_le_b 1)
+
+/-- A linear upper bound on the size of the `prime_counting'` function -/
+lemma prime_counting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
+  π' (k + n) ≤ π' k + nat.totient a * (n / a + 1) :=
+calc π' (k + n)
+    ≤ ((range k).filter (prime)).card + ((Ico k (k + n)).filter (prime)).card :
+        begin
+          rw [prime_counting', count_eq_card_filter_range, range_eq_Ico,
+              ←Ico_union_Ico_eq_Ico (zero_le k) (le_self_add), filter_union],
+          apply card_union_le,
+        end
+... ≤ π' k + ((Ico k (k + n)).filter (prime)).card :
+        by rw [prime_counting', count_eq_card_filter_range]
+... ≤ π' k + ((Ico k (k + n)).filter (coprime a)).card :
+        begin
+          refine add_le_add_left (card_le_of_subset _) k.prime_counting',
+          simp only [subset_iff, and_imp, mem_filter, mem_Ico],
+          intros p succ_k_le_p p_lt_n p_prime,
+          split,
+          { exact ⟨succ_k_le_p, p_lt_n⟩, },
+          { rw coprime_comm,
+            exact coprime_of_lt_prime h0 (gt_of_ge_of_gt succ_k_le_p h1) p_prime, },
+        end
+... ≤ π' k + totient a * (n / a + 1) :
+        begin
+          rw [add_le_add_iff_left],
+          exact Ico_filter_coprime_le k n h0,
+        end
+
+end nat

src/set_theory/fincard.lean

@@ -26,13 +26,13 @@ namespace nat
 
 /-- `nat.card α` is the cardinality of `α` as a natural number.
   If `α` is infinite, `nat.card α = 0`. -/
-def card (α : Type*) : ℕ := (mk α).to_nat
+protected def card (α : Type*) : ℕ := (mk α).to_nat
 
 @[simp]
-lemma card_eq_fintype_card [fintype α] : card α = fintype.card α := mk_to_nat_eq_card
+lemma card_eq_fintype_card [fintype α] : nat.card α = fintype.card α := mk_to_nat_eq_card
 
 @[simp]
-lemma card_eq_zero_of_infinite [infinite α] : card α = 0 := mk_to_nat_of_infinite
+lemma card_eq_zero_of_infinite [infinite α] : nat.card α = 0 := mk_to_nat_of_infinite
 
 end nat