Mathlib.Data.List.Count

List.countP_lt_length_iff theorem

{l : List α} {p : α → Bool} : l.countP p < l.length ↔ ∃ a ∈ l, p a = false

Full source

@[simp]
theorem countP_lt_length_iff {l : List α} {p : α → Bool} :
    l.countP p < l.length ↔ ∃ a ∈ l, p a = false := by
  simp [Nat.lt_iff_le_and_ne, countP_le_length]

Count of Satisfying Elements is Less Than List Length if and Only if There Exists a Falsifying Element

Informal description

For a list $l$ of elements of type $\alpha$ and a predicate $p : \alpha \to \text{Bool}$, the count of elements in $l$ satisfying $p$ is less than the length of $l$ if and only if there exists an element $a \in l$ for which $p(a) = \text{false}$.

List.count_lt_length_iff theorem

{a : α} : l.count a < l.length ↔ ∃ b ∈ l, b ≠ a

Full source

@[simp]
theorem count_lt_length_iff {a : α} : l.count a < l.length ↔ ∃ b ∈ l, b ≠ a := by simp [count]

Count Strictly Less Than Length Characterizes Non-Unique Elements in List

Informal description

For any element $a$ in a list $l$, the count of $a$ in $l$ is strictly less than the length of $l$ if and only if there exists an element $b$ in $l$ such that $b \neq a$.

List.countP_erase theorem

(p : α → Bool) (l : List α) (a : α) : countP p (l.erase a) = countP p l - if a ∈ l ∧ p a then 1 else 0

Full source

lemma countP_erase (p : α → Bool) (l : List α) (a : α) :
    countP p (l.erase a) = countP p l - if a ∈ l ∧ p a then 1 else 0 := by
  rw [countP_eq_length_filter, countP_eq_length_filter, ← erase_filter, length_erase]
  aesop

Count of Predicate in List After Removal of an Element

Informal description

For any predicate $p : \alpha \to \text{Bool}$, list $l : \text{List } \alpha$, and element $a : \alpha$, the count of elements satisfying $p$ in the list obtained by removing $a$ from $l$ is equal to the count of elements satisfying $p$ in $l$ minus $1$ if $a$ is in $l$ and satisfies $p$, and $0$ otherwise. In mathematical notation: $$ \text{countP } p (l.\text{erase } a) = \text{countP } p l - \begin{cases} 1 & \text{if } a \in l \text{ and } p a = \text{true}, \\ 0 & \text{otherwise.} \end{cases} $$

List.count_diff theorem

(a : α) (l₁ : List α) : ∀ l₂, count a (l₁.diff l₂) = count a l₁ - count a l₂

Full source

lemma count_diff (a : α) (l₁ : List α) :
    ∀ l₂, count a (l₁.diff l₂) = count a l₁ - count a l₂
  | [] => rfl
  | b :: l₂ => by
    simp only [diff_cons, count_diff, count_erase, beq_iff_eq, Nat.sub_right_comm, count_cons,
      Nat.sub_add_eq]

Count of Element in List Difference: $\text{count}(a, l_1 \setminus l_2) = \text{count}(a, l_1) - \text{count}(a, l_2)$

Informal description

For any element $a$ of type $\alpha$ and any list $l_1$ of elements of type $\alpha$, the count of $a$ in the difference $l_1 \setminus l_2$ is equal to the count of $a$ in $l_1$ minus the count of $a$ in $l_2$, for any list $l_2$ of elements of type $\alpha$. In other words: $$ \text{count}(a, l_1 \setminus l_2) = \text{count}(a, l_1) - \text{count}(a, l_2). $$

List.countP_diff theorem

(hl : l₂ <+~ l₁) (p : α → Bool) : countP p (l₁.diff l₂) = countP p l₁ - countP p l₂

Full source

lemma countP_diff (hl : l₂ <+~ l₁) (p : α → Bool) :
    countP p (l₁.diff l₂) = countP p l₁ - countP p l₂ := by
  refine (Nat.sub_eq_of_eq_add ?_).symm
  rw [← countP_append]
  exact ((subperm_append_diff_self_of_count_le <| subperm_ext_iff.1 hl).symm.trans
    perm_append_comm).countP_eq _

Count of Predicate-Satisfying Elements in List Difference

Informal description

Let $l_1$ and $l_2$ be lists of type $\alpha$ such that $l_2$ is a sublist of $l_1$ (denoted by $l_2 <+~ l_1$). For any predicate $p : \alpha \to \text{Bool}$, the count of elements satisfying $p$ in the difference list $l_1 \setminus l_2$ is equal to the count of elements satisfying $p$ in $l_1$ minus the count of elements satisfying $p$ in $l_2$. In other words, $\text{countP}\, p\, (l_1 \setminus l_2) = \text{countP}\, p\, l_1 - \text{countP}\, p\, l_2$.

List.count_map_of_injective theorem

[DecidableEq β] (l : List α) (f : α → β) (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l

Full source

@[simp]
theorem count_map_of_injective [DecidableEq β] (l : List α) (f : α → β)
    (hf : Function.Injective f) (x : α) : count (f x) (map f l) = count x l := by
  simp only [count, countP_map]
  unfold Function.comp
  simp only [hf.beq_eq]

Count Preservation under Injective Mapping: $\text{count}(f(x), \text{map}\,f\,l) = \text{count}(x, l)$

Informal description

Let $\alpha$ and $\beta$ be types with decidable equality on $\beta$. For any list $l$ of elements of type $\alpha$, any injective function $f : \alpha \to \beta$, and any element $x \in \alpha$, the count of $f(x)$ in the mapped list $\text{map}\,f\,l$ is equal to the count of $x$ in $l$. In other words, $\text{count}(f(x), \text{map}\,f\,l) = \text{count}(x, l)$.