Boolean Möbius Inversion

This file formalizes the Boolean Möbius inversion formula, also known as the Möbius inversion formula for the Boolean lattice.

Main Results

• booleanMobiusInversion: Given functions a and b on subsets of a finite set S where b I = ∑ J ⊆ I, a J for all I ⊆ S, we have a I = ∑ J ⊆ I, (-1)^|I \ J| * b J

• alternatingSum_superset_eq_iverson_a: For P ⊆ Q, we have ∑_{I : P ⊆ I ⊆ Q} (-1)^|I| = (-1)^|P| * [P = Q]

• alternatingSum_superset_eq_iverson_b: For P ⊆ Q, we have ∑_{I : P ⊆ I ⊆ Q} (-1)^|Q \ I| = [P = Q]

References

• Source: AlgebraicCombinatorics/tex/SignedCounting/InclusionExclusion2.tex
  • Section: subsec.sign.pie.moeb-bool
  • Theorem thm.pie.moeb
  • Lemma lem.pie.two-sets-altsum

Tags

inclusion-exclusion, Möbius inversion, Boolean lattice, alternating sum

Alternating Sums over Supersets

These lemmas establish the key combinatorial identities needed for the Boolean Möbius inversion formula.

The key insight is that for P ⊆ Q, the sum ∑_{I : P ⊆ I ⊆ Q} (-1)^|I| equals (-1)^|P| when P = Q and 0 otherwise. The proof uses the bijection from (Q \ P).powerset to Icc P Q (via Icc_eq_image_powerset) and then applies Mathlib's sum_powerset_neg_one_pow_card.

theorem BooleanMobius.alternatingSum_superset_eq_iverson_a {α : Type u_1} [DecidableEq α] {P Q : Finset α} (hPQ : P ⊆ Q) : ∑ I ∈ Q.powerset with P ⊆ I, (-1) ^ I.card = (-1) ^ P.card * if P = Q then 1 else 0

Lemma lem.pie.two-sets-altsum (a): For P ⊆ Q finite sets, ∑_{I : P ⊆ I ⊆ Q} (-1)^|I| = (-1)^|P| * [P = Q]

When P ≠ Q, the sum is 0. When P = Q, the only term is (-1)^|Q|.

The proof uses the bijection I ↦ I ∩ (Q \ P) from {I : P ⊆ I ⊆ Q} to (Q \ P).powerset, and then applies sum_powerset_neg_one_pow_card.

Label: eq.lem.pie.two-sets-altsum.a

theorem BooleanMobius.alternatingSum_superset_eq_iverson_b {α : Type u_1} [DecidableEq α] {P Q : Finset α} (hPQ : P ⊆ Q) : ∑ I ∈ Q.powerset with P ⊆ I, (-1) ^ (Q \ I).card = if P = Q then 1 else 0

Lemma lem.pie.two-sets-altsum (b): For P ⊆ Q finite sets, ∑_{I : P ⊆ I ⊆ Q} (-1)^|Q \ I| = [P = Q]

This follows from part (a) by the identity |Q \ I| ≡ |Q| + |I| (mod 2).

Label: eq.lem.pie.two-sets-altsum.b

Boolean Möbius Inversion

The main theorem states that if b I = ∑_{J ⊆ I} a J for all I ⊆ S, then we can recover a from b via a I = ∑_{J ⊆ I} (-1)^|I \ J| b J.

This is a fundamental result in combinatorics, generalizing the inclusion-exclusion principle.

theorem BooleanMobius.sum_powerset_powerset_swap {α : Type u_1} [DecidableEq α] {Q : Finset α} {A : Type u_2} [AddCommGroup A] (f : Finset α → Finset α → A) : ∑ J ∈ Q.powerset, ∑ P ∈ J.powerset, f J P = ∑ P ∈ Q.powerset, ∑ J ∈ Q.powerset with P ⊆ J, f J P

A helper lemma for swapping sums over pairs (J, P) with P ⊆ J ⊆ Q to pairs (P, J) with P ⊆ J ⊆ Q.

theorem BooleanMobius.booleanMobiusInversion {α : Type u_1} [DecidableEq α] {S : Finset α} {A : Type u_2} [AddCommGroup A] (a b : Finset α → A) (hab : ∀ I ⊆ S, b I = ∑ J ∈ I.powerset, a J) (I : Finset α) : I ⊆ S → a I = ∑ J ∈ I.powerset, (-1) ^ (I \ J).card • b J

Boolean Möbius inversion formula (Theorem thm.pie.moeb): Let S be a finite set and A an additive abelian group. For each subset I of S, let a_I and b_I be elements of A.

If b I = ∑_{J ⊆ I} a J for all I ⊆ S, then a I = ∑_{J ⊆ I} (-1)^|I \ J| b J for all I ⊆ S.

Label: thm.pie.moeb, eq.thm.pie.moeb.ass, eq.thm.pie.moeb.claim

theorem BooleanMobius.booleanMobiusInversion' {α : Type u_1} [DecidableEq α] {S : Finset α} {A : Type u_2} [AddCommGroup A] [Module ℤ A] (a b : Finset α → A) (hab : ∀ I ⊆ S, b I = ∑ J ∈ I.powerset, a J) (I : Finset α) : I ⊆ S → a I = ∑ J ∈ I.powerset, (-1) ^ (I \ J).card • b J

Alternative formulation of Boolean Möbius inversion using (-1)^|I \ J| as an integer. This is sometimes more convenient for computation.