Mathlib.Data.Nat.Count

Nat.count definition

(n : ℕ) : ℕ

Full source

/-- Count the number of naturals `k < n` satisfying `p k`. -/
def count (n : ℕ) : ℕ :=
  (List.range n).countP p

Count of natural numbers satisfying a predicate up to $n$

Informal description

The function counts the number of natural numbers $k < n$ that satisfy the predicate $p(k)$.

Nat.count_zero theorem

: count p 0 = 0

Full source

@[simp]
theorem count_zero : count p 0 = 0 := by
  rw [count, List.range_zero, List.countP, List.countP.go]

Count at Zero: $\mathrm{count}\,p\,0 = 0$

Informal description

For any predicate $p$ on natural numbers, the count of numbers less than $0$ satisfying $p$ is $0$, i.e., $\mathrm{count}\,p\,0 = 0$.

Nat.CountSet.fintype definition

(n : ℕ) : Fintype { i // i < n ∧ p i }

Full source

/-- A fintype instance for the set relevant to `Nat.count`. Locally an instance in locale `count` -/
def CountSet.fintype (n : ℕ) : Fintype { i // i < n ∧ p i } := by
  apply Fintype.ofFinset {x ∈ range n | p x}
  intro x
  rw [mem_filter, mem_range]
  rfl

Finiteness of the count set for natural numbers

Informal description

For any natural number $ n $ and predicate $ p $ on natural numbers, the set $\{ i \mid i < n \text{ and } p(i) \}$ is finite.

Nat.count_eq_card_filter_range theorem

(n : ℕ) : count p n = #({x ∈ range n | p x})

Full source

theorem count_eq_card_filter_range (n : ℕ) : count p n = #{x ∈ range n | p x} := by
  rw [count, List.countP_eq_length_filter]
  rfl

Count Equals Cardinality of Filtered Range

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n$ satisfying $p$ is equal to the cardinality of the set $\{x \in \mathbb{N} \mid x < n \text{ and } p(x)\}$.

Nat.count_eq_card_fintype theorem

(n : ℕ) : count p n = Fintype.card { k : ℕ // k < n ∧ p k }

Full source

/-- `count p n` can be expressed as the cardinality of `{k // k < n ∧ p k}`. -/
theorem count_eq_card_fintype (n : ℕ) : count p n = Fintype.card { k : ℕ // k < n ∧ p k } := by
  rw [count_eq_card_filter_range, ← Fintype.card_ofFinset, ← CountSet.fintype]
  rfl

Count as Cardinality of Finite Predicate-Satisfying Set

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n$ satisfying $p$ is equal to the cardinality of the finite set $\{k \in \mathbb{N} \mid k < n \text{ and } p(k)\}$.

Nat.count_le theorem

{n : ℕ} : count p n ≤ n

Full source

theorem count_le {n : ℕ} : count p n ≤ n := by
  rw [count_eq_card_filter_range]
  exact (card_filter_le _ _).trans_eq (card_range _)

Upper Bound on Count of Predicate-Satisfying Numbers: $\text{count}(p, n) \leq n$

Informal description

For any natural number $n$ and predicate $p$, the number of natural numbers less than $n$ that satisfy $p$ is at most $n$, i.e., $\text{count}(p, n) \leq n$.

Nat.count_succ theorem

(n : ℕ) : count p (n + 1) = count p n + if p n then 1 else 0

Full source

theorem count_succ (n : ℕ) : count p (n + 1) = count p n + if p n then 1 else 0 := by
  split_ifs with h <;> simp [count, List.range_succ, h]

Recursive Count Formula for Successor Natural Numbers

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n+1$ satisfying $p$ is equal to the count of numbers less than $n$ satisfying $p$ plus $1$ if $p(n)$ holds, and $0$ otherwise. That is, $$\text{count}(p, n+1) = \text{count}(p, n) + \begin{cases} 1 & \text{if } p(n) \\ 0 & \text{otherwise.} \end{cases}$$

Nat.count_monotone theorem

: Monotone (count p)

Full source

@[mono]
theorem count_monotone : Monotone (count p) :=
  monotone_nat_of_le_succ fun n ↦ by by_cases h : p n <;> simp [count_succ, h]

Monotonicity of the Count Function: $\text{count}(p, \cdot)$ is Monotone

Informal description

For any predicate $p$ on natural numbers, the function $\text{count}(p, \cdot)$ is monotone. That is, for any natural numbers $n \leq m$, we have $\text{count}(p, n) \leq \text{count}(p, m)$.

Nat.count_add theorem

(a b : ℕ) : count p (a + b) = count p a + count (fun k ↦ p (a + k)) b

Full source

theorem count_add (a b : ℕ) : count p (a + b) = count p a + count (fun k ↦ p (a + k)) b := by
  have : Disjoint {x ∈ range a | p x} {x ∈ (range b).map <| addLeftEmbedding a | p x} := by
    apply disjoint_filter_filter
    rw [Finset.disjoint_left]
    simp_rw [mem_map, mem_range, addLeftEmbedding_apply]
    rintro x hx ⟨c, _, rfl⟩
    exact (Nat.le_add_right _ _).not_lt hx
  simp_rw [count_eq_card_filter_range, range_add, filter_union, card_union_of_disjoint this,
    filter_map, addLeftEmbedding, card_map]
  rfl

Additive Property of Natural Number Counts: $\text{count}(p, a + b) = \text{count}(p, a) + \text{count}(k \mapsto p(a + k), b)$

Informal description

For any natural numbers $a$ and $b$, and any predicate $p$ on natural numbers, the count of numbers less than $a + b$ satisfying $p$ is equal to the count of numbers less than $a$ satisfying $p$ plus the count of numbers less than $b$ satisfying the shifted predicate $k \mapsto p(a + k)$. That is, $$\text{count}(p, a + b) = \text{count}(p, a) + \text{count}(k \mapsto p(a + k), b).$$

Nat.count_add' theorem

(a b : ℕ) : count p (a + b) = count (fun k ↦ p (k + b)) a + count p b

Full source

theorem count_add' (a b : ℕ) : count p (a + b) = count (fun k ↦ p (k + b)) a + count p b := by
  rw [add_comm, count_add, add_comm]
  simp_rw [add_comm b]

Additive Property of Natural Number Counts (Shifted Version): $\text{count}(p, a + b) = \text{count}(k \mapsto p(k + b), a) + \text{count}(p, b)$

Informal description

For any natural numbers $a$ and $b$, and any predicate $p$ on natural numbers, the count of numbers less than $a + b$ satisfying $p$ is equal to the count of numbers less than $a$ satisfying the shifted predicate $k \mapsto p(k + b)$ plus the count of numbers less than $b$ satisfying $p$. That is, $$\text{count}(p, a + b) = \text{count}(k \mapsto p(k + b), a) + \text{count}(p, b).$$

Nat.count_one theorem

: count p 1 = if p 0 then 1 else 0

Full source

theorem count_one : count p 1 = if p 0 then 1 else 0 := by simp [count_succ]

Count at One: $\text{count}(p, 1) = \mathbb{1}_{p(0)}$

Informal description

For any predicate $p$ on natural numbers, the count of numbers less than $1$ satisfying $p$ is $1$ if $p(0)$ holds and $0$ otherwise, i.e., $$\text{count}(p, 1) = \begin{cases} 1 & \text{if } p(0) \\ 0 & \text{otherwise.} \end{cases}$$

Nat.count_succ' theorem

(n : ℕ) : count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0

Full source

theorem count_succ' (n : ℕ) :
    count p (n + 1) = count (fun k ↦ p (k + 1)) n + if p 0 then 1 else 0 := by
  rw [count_add', count_one]

Count at Successor via Shifted Predicate: $\text{count}(p, n+1) = \text{count}(k \mapsto p(k+1), n) + \mathbb{1}_{p(0)}$

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n+1$ satisfying $p$ is equal to the count of numbers less than $n$ satisfying the shifted predicate $k \mapsto p(k+1)$ plus $1$ if $p(0)$ holds and $0$ otherwise. That is, $$\text{count}(p, n+1) = \text{count}(k \mapsto p(k+1), n) + \begin{cases} 1 & \text{if } p(0) \\ 0 & \text{otherwise.} \end{cases}$$

Nat.count_lt_count_succ_iff theorem

{n : ℕ} : count p n < count p (n + 1) ↔ p n

Full source

@[simp]
theorem count_lt_count_succ_iff {n : ℕ} : countcount p n < count p (n + 1) ↔ p n := by
  by_cases h : p n <;> simp [count_succ, h]

Count Strictly Increases at Successor if and only if Predicate Holds

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n$ satisfying $p$ is strictly less than the count of numbers less than $n+1$ satisfying $p$ if and only if $p(n)$ holds. That is, $$\text{count}(p, n) < \text{count}(p, n+1) \leftrightarrow p(n).$$

Nat.count_succ_eq_succ_count_iff theorem

{n : ℕ} : count p (n + 1) = count p n + 1 ↔ p n

Full source

theorem count_succ_eq_succ_count_iff {n : ℕ} : countcount p (n + 1) = count p n + 1 ↔ p n := by
  by_cases h : p n <;> simp [h, count_succ]

Count Increment Condition for Successor Natural Numbers

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n+1$ satisfying $p$ equals the count of numbers less than $n$ satisfying $p$ plus one if and only if $p(n)$ holds. That is, $$\text{count}(p, n+1) = \text{count}(p, n) + 1 \leftrightarrow p(n).$$

Nat.count_succ_eq_count_iff theorem

{n : ℕ} : count p (n + 1) = count p n ↔ ¬p n

Full source

theorem count_succ_eq_count_iff {n : ℕ} : countcount p (n + 1) = count p n ↔ ¬p n := by
  by_cases h : p n <;> simp [h, count_succ]

Count Invariance Condition for Successor Natural Numbers

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n+1$ satisfying $p$ equals the count of numbers less than $n$ satisfying $p$ if and only if $p(n)$ does not hold. That is, $$\text{count}(p, n+1) = \text{count}(p, n) \leftrightarrow \neg p(n).$$

Nat.lt_of_count_lt_count theorem

{a b : ℕ} (h : count p a < count p b) : a < b

Full source

theorem lt_of_count_lt_count {a b : ℕ} (h : count p a < count p b) : a < b :=
  (count_monotone p).reflect_lt h

Strict Count Comparison Implies Strict Ordering of Natural Numbers

Informal description

For any natural numbers $a$ and $b$, if the count of numbers less than $a$ satisfying predicate $p$ is strictly less than the count of numbers less than $b$ satisfying $p$, then $a < b$. That is, $$\text{count}(p, a) < \text{count}(p, b) \implies a < b.$$

Nat.count_strict_mono theorem

{m n : ℕ} (hm : p m) (hmn : m < n) : count p m < count p n

Full source

theorem count_strict_mono {m n : ℕ} (hm : p m) (hmn : m < n) : count p m < count p n :=
  (count_lt_count_succ_iff.2 hm).trans_le <| count_monotone _ (Nat.succ_le_iff.2 hmn)

Strict Monotonicity of Count Function under Predicate Condition

Informal description

For any natural numbers $m$ and $n$ and predicate $p$, if $p(m)$ holds and $m < n$, then the count of numbers less than $m$ satisfying $p$ is strictly less than the count of numbers less than $n$ satisfying $p$. That is, if $p(m)$ and $m < n$, then $\text{count}(p, m) < \text{count}(p, n)$.

Nat.count_injective theorem

{m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n

Full source

theorem count_injective {m n : ℕ} (hm : p m) (hn : p n) (heq : count p m = count p n) : m = n := by
  by_contra! h : m ≠ n
  wlog hmn : m < n
  · exact this hn hm heq.symm h.symm (h.lt_or_lt.resolve_left hmn)
  · simpa [heq] using count_strict_mono hm hmn

Injectivity of Count Function for Predicate-Satisfying Natural Numbers

Informal description

For any natural numbers $m$ and $n$ and predicate $p$, if $p(m)$ and $p(n)$ hold and the count of numbers less than $m$ satisfying $p$ equals the count of numbers less than $n$ satisfying $p$, then $m = n$. In other words, if $p(m)$, $p(n)$, and $\mathrm{count}(p, m) = \mathrm{count}(p, n)$, then $m = n$.

Nat.count_le_card theorem

(hp : (setOf p).Finite) (n : ℕ) : count p n ≤ #hp.toFinset

Full source

theorem count_le_card (hp : (setOf p).Finite) (n : ℕ) : count p n ≤ #hp.toFinset := by
  rw [count_eq_card_filter_range]
  exact Finset.card_mono fun x hx ↦ hp.mem_toFinset.2 (mem_filter.1 hx).2

Upper Bound on Count of Numbers Satisfying a Finite Predicate

Informal description

For any predicate $p$ on natural numbers such that the set $\{x \mid p(x)\}$ is finite, and for any natural number $n$, the count of numbers less than $n$ satisfying $p$ is at most the cardinality of the finite set $\{x \mid p(x)\}$. In other words, if we let $S = \{x \in \mathbb{N} \mid p(x)\}$ be finite, then for all $n \in \mathbb{N}$ we have $\mathrm{count}(p, n) \leq |S|$.

Nat.count_lt_card theorem

{n : ℕ} (hp : (setOf p).Finite) (hpn : p n) : count p n < #hp.toFinset

Full source

theorem count_lt_card {n : ℕ} (hp : (setOf p).Finite) (hpn : p n) : count p n < #hp.toFinset :=
  (count_lt_count_succ_iff.2 hpn).trans_le (count_le_card hp _)

Count of Numbers Satisfying Predicate is Strictly Less Than Cardinality When Predicate Holds

Informal description

For any natural number $n$ and predicate $p$ such that the set $\{x \mid p(x)\}$ is finite, if $p(n)$ holds, then the count of numbers less than $n$ satisfying $p$ is strictly less than the cardinality of the finite set $\{x \mid p(x)\}$. In other words, if $S = \{x \in \mathbb{N} \mid p(x)\}$ is finite and $n \in S$, then $\mathrm{count}(p, n) < |S|$.

Nat.count_iff_forall theorem

{n : ℕ} : count p n = n ↔ ∀ n' < n, p n'

Full source

theorem count_iff_forall {n : ℕ} : countcount p n = n ↔ ∀ n' < n, p n' := by
  simpa [count_eq_card_filter_range, card_range, mem_range] using
    card_filter_eq_iff (p := p) (s := range n)

Count Equals $n$ iff Predicate Holds for All Numbers Below $n$

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n$ satisfying $p$ equals $n$ if and only if the predicate $p$ holds for all natural numbers $n' < n$.

Nat.count_true theorem

(n : ℕ) : count (fun _ ↦ True) n = n

Full source

@[simp] theorem count_true (n : ℕ) : count (fun _ ↦ True) n = n := count_of_forall fun _ _ ↦ trivial

Count of True Predicate Equals $n$

Informal description

For any natural number $n$, the count of numbers less than $n$ satisfying the always-true predicate is equal to $n$, i.e., $\mathrm{count}(\lambda \_. \mathrm{True}, n) = n$.

Nat.count_iff_forall_not theorem

{n : ℕ} : count p n = 0 ↔ ∀ m < n, ¬p m

Full source

theorem count_iff_forall_not {n : ℕ} : countcount p n = 0 ↔ ∀ m < n, ¬p m := by
  simpa [count_eq_card_filter_range, mem_range] using
    card_filter_eq_zero_iff (p := p) (s := range n)

Count Zero iff Predicate Fails for All Numbers Below $n$

Informal description

For any natural number $n$ and predicate $p$, the count of numbers less than $n$ satisfying $p$ is zero if and only if for all $m < n$, the predicate $p(m)$ does not hold.

Nat.count_false theorem

(n : ℕ) : count (fun _ ↦ False) n = 0

Full source

@[simp] theorem count_false (n : ℕ) : count (fun _ ↦ False) n = 0 :=
  count_of_forall_not fun _ _ ↦ id

Count of False Predicate is Zero

Informal description

For any natural number $n$, the count of numbers less than $n$ satisfying the always-false predicate is zero, i.e., $\mathrm{count}(\lambda \_. \mathrm{False}, n) = 0$.

Nat.count_mono_left theorem

{n : ℕ} (hpq : ∀ k, p k → q k) : count p n ≤ count q n

Full source

theorem count_mono_left {n : ℕ} (hpq : ∀ k, p k → q k) : count p n ≤ count q n := by
  simp only [count_eq_card_filter_range]
  exact card_le_card ((range n).monotone_filter_right hpq)

Monotonicity of Count under Predicate Implication

Informal description

For any natural number $n$ and predicates $p, q$ on natural numbers, if $p(k)$ implies $q(k)$ for all $k$, then the number of natural numbers less than $n$ satisfying $p$ is less than or equal to the number of natural numbers less than $n$ satisfying $q$.