Counting functions by constrained positions

Main results

• Finset.card_pi_places_card: count functions by the positions with a property.
• Finset.card_places_card: binomial count without pointwise constraints.

References

Adapted selectively from Anthropic's pinned formal source. Source pin: 16a5ce41304fcdaea4e0be7c132e1c361dc26da5.

theorem Finset.prod_ite_mem_const {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [CommMonoid M] (S : Finset ι) (a b : M) : (∏ i : ι, if i ∈ S then a else b) = a ^ S.card * b ^ (Fintype.card ι - S.card)

A product that takes the value a on S and b elsewhere.

theorem Finset.prod_ite_ite_subset {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [CommMonoidWithZero M] (Q S : Finset ι) (c : M) : (∏ i : ι, if i ∈ S then if i ∈ Q then 1 else 0 else if i ∈ Q then c else 1) = if S ⊆ Q then c ^ (Q.card - S.card) else 0

A product with the factors 1 on S ∩ Q, 0 on S \ Q, c on Q \ S and 1 elsewhere: it is 0 unless S ⊆ Q.

theorem Finset.prod_ite_ite_superset {ι : Type u_1} [Fintype ι] [DecidableEq ι] {M : Type u_2} [CommMonoidWithZero M] (T S : Finset ι) : (∏ i : ι, if i ∈ S then 1 else if i ∈ T then 0 else 1) = if T ⊆ S then 1 else 0

A product with the factor 0 on T \ S and 1 elsewhere: it is 0 unless T ⊆ S.

theorem Finset.sum_powersetCard_ite_subset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (Q : Finset ι) (k c : ℕ) : (∑ S ∈ powersetCard k univ, if S ⊆ Q then c else 0) = Q.card.choose k * c

The number of sets of k elements inside Q, each counted c times.

theorem Finset.card_powersetCard_superset {ι : Type u_1} [Fintype ι] [DecidableEq ι] (T : Finset ι) {k : ℕ} (hk : k ≤ Fintype.card ι) : {S ∈ powersetCard k univ | T ⊆ S}.card = (Fintype.card ι - T.card).choose (Fintype.card ι - k)

The number of sets of k elements that contain T: choose the complement outside T.

Functions by the set of places with a property

theorem Finset.card_pi_places_eq {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] [DecidableEq α] (A : ι → Finset α) (p : α → Prop) [DecidablePred p] (S : Finset ι) : {f : ι → α | (∀ (i : ι), f i ∈ A i) ∧ {i : ι | p (f i)} = S}.card = ∏ i : ι, if i ∈ S then {a ∈ A i | p a}.card else {a ∈ A i | ¬p a}.card

Count the functions satisfying f i ∈ A i and having property p exactly on S by multiplying the permitted choices at each position.

theorem Finset.card_pi_places_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] [DecidableEq α] (A : ι → Finset α) (p : α → Prop) [DecidablePred p] (k : ℕ) : {f : ι → α | (∀ (i : ι), f i ∈ A i) ∧ {i : ι | p (f i)}.card = k}.card = ∑ S ∈ powersetCard k univ, ∏ i : ι, if i ∈ S then {a ∈ A i | p a}.card else {a ∈ A i | ¬p a}.card

Partition the functions satisfying f i ∈ A i and having property p at exactly k positions by their size-k set of such positions, and sum the corresponding products of choice counts.

theorem Finset.card_places_card {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (p : α → Prop) [DecidablePred p] (k : ℕ) : {f : ι → α | {i : ι | p (f i)}.card = k}.card = (Fintype.card ι).choose k * ({a : α | p a}.card ^ k * {a : α | ¬p a}.card ^ (Fintype.card ι - k))

The number of functions ι → α that have p at exactly k places.