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

TODO

• Use (a slight variant of) Finset.prod_indicator_biUnion_sub_indicator to prove the integral version of inclusion-exclusion.
• 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} [DecidableEq α] {s : Finset ι} (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} [DecidableEq α] [AddCommGroup G] (s : Finset ι) (S : ι → Finset α) (f : α → G) : ∑ a ∈ s.biUnion S, f a = ∑ t : { x : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-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 : Finset ι // x ∈ Finset.filter (fun (x : Finset ι) => x.Nonempty) s.powerset }, (-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} [DecidableEq α] [AddCommGroup G] [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.