# Counting on ℕ #

This file defines the `count` function, which gives, for any predicate on the natural numbers, "how many numbers under `k` satisfy this predicate?". We then prove several expected lemmas about `count`, relating it to the cardinality of other objects, and helping to evaluate it for specific `k`.

source
def Nat.count (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
ℕ

Count the number of naturals `k < n` satisfying `p k`.

Equations

- Nat.count p n = List.countP (fun (b : ℕ) => decide (p b)) (List.range n)

Instances For

source
@[simp]
theorem Nat.count_zero (p : ℕ → Prop) [DecidablePred p] :
count p 0 = 0
source
def Nat.CountSet.fintype (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
Fintype { i : ℕ // i < n ∧ p i }

A fintype instance for the set relevant to `Nat.count`. Locally an instance in scope `count`

Equations

- Nat.CountSet.fintype p n = Fintype.ofFinset ({x ∈ Finset.range n | p x}) ⋯

Instances For

source
theorem Nat.count_eq_card_filter_range (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
count p n = {x ∈ Finset.range n | p x}.card
source
theorem Nat.count_eq_card_fintype (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
count p n = Fintype.card { k : ℕ // k < n ∧ p k }

`count p n` can be expressed as the cardinality of `{k // k < n ∧ p k}`.

source
theorem Nat.count_le (p : ℕ → Prop) [DecidablePred p] {n : ℕ} :
count p n ≤ n
source
theorem Nat.count_succ (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
count p (n + 1) = count p n + if p n then 1 else 0
source
theorem Nat.count_monotone (p : ℕ → Prop) [DecidablePred p] :
Monotone (count p)
source
theorem Nat.count_add (p : ℕ → Prop) [DecidablePred p] (a b : ℕ) :
count p (a + b) = count p a + count (fun (k : ℕ) => p (a + k)) b
source
theorem Nat.count_add' (p : ℕ → Prop) [DecidablePred p] (a b : ℕ) :
count p (a + b) = count (fun (k : ℕ) => p (k + b)) a + count p b
source
theorem Nat.count_one (p : ℕ → Prop) [DecidablePred p] :
count p 1 = if p 0 then 1 else 0
source
theorem Nat.count_succ' (p : ℕ → Prop) [DecidablePred p] (n : ℕ) :
count p (n + 1) = count (fun (k : ℕ) => p (k + 1)) n + if p 0 then 1 else 0
source
@[simp]
theorem Nat.count_lt_count_succ_iff {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p n < count p (n + 1) ↔ p n
source
theorem Nat.count_succ_eq_succ_count_iff {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p (n + 1) = count p n + 1 ↔ p n
source
theorem Nat.count_succ_eq_count_iff {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p (n + 1) = count p n ↔ ¬p n
source
theorem Nat.count_succ_eq_succ_count {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
p n → count p (n + 1) = count p n + 1

Alias of the reverse direction of `Nat.count_succ_eq_succ_count_iff`.

source
theorem Nat.count_succ_eq_count {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
¬p n → count p (n + 1) = count p n

Alias of the reverse direction of `Nat.count_succ_eq_count_iff`.

source
theorem Nat.lt_of_count_lt_count {p : ℕ → Prop} [DecidablePred p] {a b : ℕ} (h : count p a < count p b) :
a < b
source
theorem Nat.count_strict_mono {p : ℕ → Prop} [DecidablePred p] {m n : ℕ} (hm : p m) (hmn : m < n) :
count p m < count p n
source
theorem Nat.count_injective {p : ℕ → Prop} [DecidablePred p] {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) :
m = n
source
theorem Nat.count_le_card {p : ℕ → Prop} [DecidablePred p] (hp : (setOf p).Finite) (n : ℕ) :
count p n ≤ hp.toFinset.card
source
theorem Nat.count_lt_card {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hp : (setOf p).Finite) (hpn : p n) :
count p n < hp.toFinset.card
source
theorem Nat.count_iff_forall {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p n = n ↔ ∀ n' < n, p n'
source
theorem Nat.count_of_forall {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
(∀ n' < n, p n') → count p n = n

Alias of the reverse direction of `Nat.count_iff_forall`.

source
@[simp]
theorem Nat.count_true (n : ℕ) :
count (fun (x : ℕ) => True) n = n
source
theorem Nat.count_iff_forall_not {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p n = 0 ↔ ∀ m < n, ¬p m
source
theorem Nat.count_of_forall_not {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
(∀ m < n, ¬p m) → count p n = 0

Alias of the reverse direction of `Nat.count_iff_forall_not`.

source
theorem Nat.count_ne_iff_exists {p : ℕ → Prop} [DecidablePred p] {n : ℕ} :
count p n ≠ 0 ↔ ∃ m < n, p m
source
@[simp]
theorem Nat.count_false (n : ℕ) :
count (fun (x : ℕ) => False) n = 0
source
theorem Nat.exists_of_count_lt_count {p : ℕ → Prop} [DecidablePred p] {a b : ℕ} (h : count p a < count p b) :
∃ x ∈ Set.Ico a b, p x
source
theorem Nat.count_mono_left {p : ℕ → Prop} [DecidablePred p] {q : ℕ → Prop} [DecidablePred q] {n : ℕ} (hpq : ∀ k < n, p k → q k) :
count p n ≤ count q n