English
Over a finite index set, the indicator of a union equals an alternating sum of indicators of intersections, with signs given by the subset cardinalities.
Русский
Индикатор объединения равен чередующейся сумме индикаторов пересечений с знаками по мощности подмножеств.
LaTeX
$$$ \mathbf{1}_{\bigcup_{i\in s} S_i}(a) = \sum_{t \subseteq s, t.Nonempty} (-1)^{|t|} \mathbf{1}_{\bigcap_{i\in t} S_i}(a) $$$
Lean4
/-- **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 inclusion_exclusion_sum_biUnion (s : Finset ι) (S : ι → Finset α) (f : α → G) :
∑ a ∈ s.biUnion S, f a =
∑ t : s.powerset.filter (·.Nonempty), (-1) ^ (#t.1 + 1) • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a :=
by
classical
rw [← sub_eq_zero]
calc
∑ a ∈ s.biUnion S, f a -
∑ t : s.powerset.filter (·.Nonempty), (-1) ^ (#t.1 + 1) • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a =
∑ t : s.powerset.filter (·.Nonempty), (-1) ^ #t.1 • ∑ a ∈ t.1.inf' (mem_filter.1 t.2).2 S, f a +
∑ t ∈ s.powerset.filter (¬·.Nonempty), (-1) ^ #t • ∑ a ∈ s.biUnion S, f a :=
by simp [sub_eq_neg_add, ← sum_neg_distrib, filter_eq', pow_succ]
_ = ∑ t ∈ s.powerset, (-1) ^ #t • if ht : t.Nonempty then ∑ a ∈ t.inf' ht S, f a else ∑ a ∈ s.biUnion S, f a := by
rw [← sum_attach (filter ..)]; simp [sum_dite]
_ = ∑ a ∈ s.biUnion S, (∏ i ∈ s, (1 - Set.indicator (S i) 1 a : ℤ)) • f a :=
by
simp only [Int.reduceNeg, prod_sub, sum_comm (s := s.biUnion S), sum_smul, mul_assoc]
congr! with t
split_ifs with ht
· obtain ⟨i, hi⟩ := ht
simp only [prod_const_one, prod_indicator_apply]
simp only [smul_sum, Set.indicator, Set.mem_iInter, mem_coe, Pi.one_apply, mul_ite, mul_one, mul_zero, ite_smul,
zero_smul, sum_ite, not_forall, sum_const_zero, add_zero]
congr
aesop
· obtain rfl := not_nonempty_iff_eq_empty.1 ht
simp
_ = ∑ a ∈ s.biUnion S, (∏ i ∈ s, (Set.indicator (s.biUnion S) 1 a - Set.indicator (S i) 1 a) : ℤ) • f a := by
congr! with t; rw [Set.indicator_of_mem ‹_›, Pi.one_apply]
_ = 0 := by
obtain rfl | hs := s.eq_empty_or_nonempty <;> simp [-coe_biUnion, prod_indicator_biUnion_finset_sub_indicator, *]
