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.

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)

@[simp]

theorem Nat.count_zero (p : ℕ → Prop) [DecidablePred p] : Nat.count p 0 = 0

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 locale count

Equations

• Nat.CountSet.fintype p n = Fintype.ofFinset (Finset.filter p (Finset.range n)) (_ : ∀ (x : ℕ), x ∈ Finset.filter p (Finset.range n) ↔ x ∈ fun x => x < n ∧ p x)

theorem Nat.count_eq_card_filter_range (p : ℕ → Prop) [DecidablePred p] (n : ℕ) : Nat.count p n = Finset.card (Finset.filter p (Finset.range n))

theorem Nat.count_eq_card_fintype (p : ℕ → Prop) [DecidablePred p] (n : ℕ) : Nat.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}.

theorem Nat.count_succ (p : ℕ → Prop) [DecidablePred p] (n : ℕ) : Nat.count p (n + 1) = Nat.count p n + if p n then 1 else 0

theorem Nat.count_monotone (p : ℕ → Prop) [DecidablePred p] : Monotone (Nat.count p)

theorem Nat.count_add (p : ℕ → Prop) [DecidablePred p] (a : ℕ) (b : ℕ) : Nat.count p (a + b) = Nat.count p a + Nat.count (fun k => p (a + k)) b

theorem Nat.count_add' (p : ℕ → Prop) [DecidablePred p] (a : ℕ) (b : ℕ) : Nat.count p (a + b) = Nat.count (fun k => p (k + b)) a + Nat.count p b

theorem Nat.count_one (p : ℕ → Prop) [DecidablePred p] : Nat.count p 1 = if p 0 then 1 else 0

theorem Nat.count_succ' (p : ℕ → Prop) [DecidablePred p] (n : ℕ) : Nat.count p (n + 1) = Nat.count (fun k => p (k + 1)) n + if p 0 then 1 else 0

@[simp]

theorem Nat.count_lt_count_succ_iff {p : ℕ → Prop} [DecidablePred p] {n : ℕ} : Nat.count p n < Nat.count p (n + 1) ↔ p n

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

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

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

Alias of the reverse direction of Nat.count_succ_eq_succ_count_iff.

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

Alias of the reverse direction of Nat.count_succ_eq_count_iff.

theorem Nat.count_le_cardinal {p : ℕ → Prop} [DecidablePred p] (n : ℕ) : ↑(Nat.count p n) ≤ Cardinal.mk ↑{k | p k}

theorem Nat.lt_of_count_lt_count {p : ℕ → Prop} [DecidablePred p] {a : ℕ} {b : ℕ} (h : Nat.count p a < Nat.count p b) : a < b

theorem Nat.count_strict_mono {p : ℕ → Prop} [DecidablePred p] {m : ℕ} {n : ℕ} (hm : p m) (hmn : m < n) : Nat.count p m < Nat.count p n

theorem Nat.count_injective {p : ℕ → Prop} [DecidablePred p] {m : ℕ} {n : ℕ} (hm : p m) (hn : p n) (heq : Nat.count p m = Nat.count p n) : m = n

theorem Nat.count_le_card {p : ℕ → Prop} [DecidablePred p] (hp : Set.Finite (setOf p)) (n : ℕ) : Nat.count p n ≤ Finset.card (Set.Finite.toFinset hp)

theorem Nat.count_lt_card {p : ℕ → Prop} [DecidablePred p] {n : ℕ} (hp : Set.Finite (setOf p)) (hpn : p n) : Nat.count p n < Finset.card (Set.Finite.toFinset hp)

theorem Nat.count_mono_left {p : ℕ → Prop} [DecidablePred p] {q : ℕ → Prop} [DecidablePred q] {n : ℕ} (hpq : (k : ℕ) → p k → q k) : Nat.count p n ≤ Nat.count q n