Occurrence counts in finite families

occCount f y counts the indices at which a family f takes the value y. For an infinite fiber its value is zero, following the convention of Nat.card. Occurrence counts regroup sums over a finite family by fibers: each value in a finite set covering the range is weighted by its occurrence count.

Main results

• Function.occCount_pos: for a finite fiber, the count is positive exactly when it is nonempty.
• Function.occCount_of_injective: an injective function has count one on its range and zero outside.
• Function.occCount_le_of_comp, Function.occCount_lt_of_comp: comparison along embeddings.
• Function.occCount_eq_card_preimage: the count as the cardinality of a singleton preimage.
• Function.prod_occCount_pow and its additive form Function.sum_occCount_nsmul: regroup a product or sum by counting the occurrences of each value.
• Function.occCount_castSucc, Function.occCount_succ: split off the last or first position.
• Function.sum_occCount_eq_card: the total occurrence count is the cardinality of the index type.
• Function.exists_perm_of_occCount_eq: equal counts on finite families give a permutation.

noncomputable def Function.occCount {X : Type u_1} {S : Type u_2} (f : X → S) (y : S) : ℕ

The cardinality of a fiber, counting occurrences of a value in a family.

Equations

• Function.occCount f y = Nat.card { x : X // f x = y }

theorem Function.occCount_def {X : Type u_1} {S : Type u_2} (f : X → S) (y : S) : occCount f y = Nat.card { x : X // f x = y }

Occurrence counts are natural cardinalities of fibers.

theorem Function.occCount_eq_card_filter {X : Type u_1} {S : Type u_2} [Fintype X] [DecidableEq S] (f : X → S) (y : S) : occCount f y = {x : X | f x = y}.card

The occurrence count is the Finset.card of the indices taking the given value.

theorem Function.occCount_eq_sum {X : Type u_1} {S : Type u_2} [Fintype X] [DecidableEq S] (w : X → S) (a : S) : occCount w a = ∑ i : X, if w i = a then 1 else 0

The occurrence count as a sum of indicators over the positions.

theorem Function.occCount_le_of_comp {X : Type u_1} {S : Type u_2} {Y : Type u_3} {u : X → S} {v : Y → S} (e : X ↪ Y) (he : ∀ (i : X), v (e i) = u i) (a : S) [Finite { y : Y // v y = a }] : occCount u a ≤ occCount v a

When the target fiber is finite, occurrence counts grow along an embedding preserving the values.

theorem Function.occCount_lt_of_comp {X : Type u_1} {S : Type u_2} {Y : Type u_3} {u : X → S} {v : Y → S} {a : S} [Finite { y : Y // v y = a }] {j : Y} (e : X ↪ Y) (he : ∀ (i : X), v (e i) = u i) (hj : v j = a) (hmiss : ∀ (i : X), e i ≠ j) : occCount u a < occCount v a

When the target fiber is finite, an embedding that misses an occurrence gives a strictly smaller occurrence count.

@[simp]

theorem Function.occCount_pos {X : Type u_1} {S : Type u_2} (f : X → S) (y : S) [Finite { x : X // f x = y }] : 0 < occCount f y ↔ ∃ (x : X), f x = y

For a finite fiber, positive occurrence count is equivalent to the value being attained.

theorem Function.occCount_eq_card_preimage {X : Type u_1} {S : Type u_2} (f : X → S) (y : S) : occCount f y = Nat.card ↑(f ⁻¹' {y})

Occurrence counts are the cardinalities of singleton preimages.

@[simp]

theorem Function.occCount_of_notMem_range {X : Type u_1} {S : Type u_2} (f : X → S) (y : S) (h : y ∉ Set.range f) : occCount f y = 0

A value outside the range has occurrence count zero.

theorem Function.occCount_of_injective {X : Type u_1} {S : Type u_2} (f : X → S) (hinj : Injective f) (y : S) [Decidable (∃ (x : X), f x = y)] : occCount f y = if ∃ (x : X), f x = y then 1 else 0

An injective function gives occurrence count one precisely on its range.

@[simp]

theorem Function.occCount_apply_of_injective {X : Type u_1} {S : Type u_2} (f : X → S) (hinj : Injective f) (x : X) : occCount f (f x) = 1

Every value of an injective function occurs exactly once.

theorem Function.prod_occCount_pow {X : Type u_1} {S : Type u_2} [Fintype X] {K : Type u_3} [CommMonoid K] (f : X → S) {T : Finset S} (hT : ∀ (x : X), f x ∈ T) (weight : S → K) : ∏ y ∈ T, weight y ^ occCount f y = ∏ x : X, weight (f x)

Raising each weight to its occurrence count gives the product over all indices.

theorem Function.sum_occCount_nsmul {X : Type u_1} {S : Type u_2} [Fintype X] {K : Type u_3} [AddCommMonoid K] (f : X → S) {T : Finset S} (hT : ∀ (x : X), f x ∈ T) (weight : S → K) : ∑ y ∈ T, occCount f y • weight y = ∑ x : X, weight (f x)

Weighting each value by its occurrence count gives the sum over all indices.

theorem Function.sum_occCount_eq_card {X : Type u_1} {S : Type u_2} [Finite X] (f : X → S) {T : Finset S} (hT : ∀ (x : X), f x ∈ T) : ∑ y ∈ T, occCount f y = Nat.card X

Occurrence counts over a finite set containing the range sum to the size of the original family.

theorem Function.occCount_castSucc {S : Type u_2} [DecidableEq S] {n : ℕ} (w : Fin (n + 1) → S) (a : S) : (occCount (w ∘ Fin.castSucc) a + if w (Fin.last n) = a then 1 else 0) = occCount w a

Splitting off the last position: the occurrences of a in a word are those in its initial segment together with a possible occurrence at the last position.

theorem Function.occCount_succ {S : Type u_2} [DecidableEq S] {n : ℕ} (w : Fin (n + 1) → S) (a : S) : (occCount (w ∘ Fin.succ) a + if w 0 = a then 1 else 0) = occCount w a

Splitting off the first position: the occurrences of a in a word are those in its final segment together with a possible occurrence at the first position.

theorem Function.exists_perm_of_occCount_eq {X : Type u_1} {S : Type u_2} [Finite X] {u v : X → S} (h : ∀ (a : S), occCount u a = occCount v a) : ∃ (σ : Equiv.Perm X), v ∘ ⇑σ = u

Two families on a finite index type with equal occurrence counts differ by a permutation.