Indexed multiplicity under list membership filtering

These statements count positions, so repeated equal lists still contribute separately. They are generalized from the canonical incidence-path occupancy proofs.

Main results

• List.two_le_filter_contains_iff.
• List.exists_other_index_of_two_le_filter_contains.
• List.toFinset_filter_not_mem: filtering C by non-membership in H takes the set difference C.toFinset \ H.toFinset.
• List.countP_le_sum_map: if 1 ≤ f x whenever p x = true on l, then l.countP p ≤ (l.map f).sum.

theorem List.two_le_filter_contains_iff {α : Type u_1} [DecidableEq α] (rs : List (List α)) (p : α) : 2 ≤ (filter (fun (r : List α) => r.contains p) rs).length ↔ ∃ (i : ℕ) (j : ℕ) (hi : i < rs.length) (hj : j < rs.length), i ≠ j ∧ p ∈ rs[i] ∧ p ∈ rs[j]

At least two memberships correspond to distinct indices, even for repeated equal lists.

theorem List.exists_other_index_of_two_le_filter_contains {α : Type u_1} [DecidableEq α] (rs : List (List α)) (p : α) (i : ℕ) (hcount : 2 ≤ (filter (fun (r : List α) => r.contains p) rs).length) : ∃ (j : ℕ) (hj : j < rs.length), j ≠ i ∧ p ∈ rs[j]

Two filtered memberships give an index different from any given natural number.

theorem List.toFinset_filter_not_mem {α : Type u_1} [DecidableEq α] (C H : List α) : (filter (fun (l : α) => !H.any fun (x : α) => x == l) C).toFinset = C.toFinset \ H.toFinset

Filtering C by non-membership in H takes the set difference C.toFinset \ H.toFinset.

theorem List.countP_le_sum_map {α : Type u_1} {p : α → Bool} {f : α → ℕ} {l : List α} (h : ∀ x ∈ l, p x = true → 1 ≤ f x) : countP p l ≤ (map f l).sum

If 1 ≤ f x whenever p x = true on l, then l.countP p ≤ (l.map f).sum.