Inclusion-exclusion principle

This file proves several variants of the inclusion-exclusion principle.

The inclusion-exclusion principle says that the sum/integral of a function over a finite union of sets can be calculated as the alternating sum over n > 0 of the sum/integral of the function over the intersection of n of the sets.

By taking complements, it also says that the sum/integral of a function over a finite intersection of complements of sets can be calculated as the alternating sum over n ≥ 0 of the sum/integral of the function over the intersection of n of the sets.

By taking the function to be constant 1, we instead get a result about the cardinality/measure of the sets.

Main declarations

Per the above explanation, this file contains the following variants of inclusion-exclusion:

• Finset.inclusion_exclusion_sum_biUnion: Sum of a function over a finite union of sets
• Finset.inclusion_exclusion_card_biUnion: Cardinality of a finite union of sets
• Finset.inclusion_exclusion_sum_inf_compl: Sum of a function over a finite intersection of complements of sets
• Finset.inclusion_exclusion_card_inf_compl: Cardinality of a finite intersection of complements of sets

See also MeasureTheory.integral_biUnion_eq_sum_powerset for the version with integrals, and MeasureTheory.measureReal_biUnion_eq_sum_powerset for the version with measures.

TODO

• Prove that truncating the series alternatively gives an upper/lower bound to the true value.

theorem Finset.prod_indicator_biUnion_sub_indicator {ι : Type u_1} {α : Type u_2} {s : Finset ι} (hs : s.Nonempty) (S : ι → Set α) (a : α) : ∏ i ∈ s, ((⋃ i ∈ s, S i).indicator 1 a - (S i).indicator 1 a) = 0

theorem Finset.indicator_biUnion_eq_sum_powerset {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddCommGroup G] (s : Finset ι) (S : ι → Set α) (f : α → G) (a : α) : (⋃ i ∈ s, S i).indicator f a = ∑ t ∈ s.powerset with t.Nonempty, (-1) ^ (t.card + 1) • (⋂ i ∈ t, S i).indicator f a

Inclusion-exclusion principle, indicator version over a finite union of sets.

theorem Finset.prod_indicator_biUnion_finset_sub_indicator {ι : Type u_1} {α : Type u_2} {s : Finset ι} [DecidableEq α] (hs : s.Nonempty) (S : ι → Finset α) (a : α) : ∏ i ∈ s, ((↑(s.biUnion S)).indicator 1 a - (↑(S i)).indicator 1 a) = 0

theorem Finset.inclusion_exclusion_sum_biUnion {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddCommGroup G] [DecidableEq α] (s : Finset ι) (S : ι → Finset α) (f : α → G) : ∑ a ∈ s.biUnion S, f a = ∑ t : ↥({x ∈ s.powerset | x.Nonempty}), (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a

Inclusion-exclusion principle for the sum of a function over a union.

The sum of a function f over the union of the S i over i ∈ s is the alternating sum of the sums of f over the intersections of the S i.

theorem Finset.inclusion_exclusion_card_biUnion {ι : Type u_1} {α : Type u_2} [DecidableEq α] (s : Finset ι) (S : ι → Finset α) : ↑(s.biUnion S).card = ∑ t : ↥({x ∈ s.powerset | x.Nonempty}), (-1) ^ ((↑t).card + 1) * ↑((↑t).inf' ⋯ S).card

Inclusion-exclusion principle for the cardinality of a union.

The cardinality of the union of the S i over i ∈ s is the alternating sum of the cardinalities of the intersections of the S i.

theorem Finset.inclusion_exclusion_sum_inf_compl {ι : Type u_1} {α : Type u_2} {G : Type u_3} [AddCommGroup G] [DecidableEq α] [Fintype α] (s : Finset ι) (S : ι → Finset α) (f : α → G) : ∑ a ∈ s.inf fun (i : ι) => (S i)ᶜ, f a = ∑ t ∈ s.powerset, (-1) ^ t.card • ∑ a ∈ t.inf S, f a

Inclusion-exclusion principle for the sum of a function over an intersection of complements.

The sum of a function f over the intersection of the complements of the S i over i ∈ s is the alternating sum of the sums of f over the intersections of the S i.

theorem Finset.inclusion_exclusion_card_inf_compl {ι : Type u_1} {α : Type u_2} [DecidableEq α] [Fintype α] (s : Finset ι) (S : ι → Finset α) : ↑(s.inf fun (i : ι) => (S i)ᶜ).card = ∑ t ∈ s.powerset, (-1) ^ t.card * ↑(t.inf S).card

Inclusion-exclusion principle for the cardinality of an intersection of complements.

The cardinality of the intersection of the complements of the S i over i ∈ s is the alternating sum of the cardinalities of the intersections of the S i.