Möbius inversion on a finite Boolean lattice

This file pins the upper-transform convention used for graph parameters independently of graphs. For s ⊆ t, the inverse coefficient is (-1) ^ #(t \ s): the exponent counts elements added to the lower set. The small executable examples at the end guard this orientation.

def Finset.booleanUpperZeta {I : Type u_1} [Fintype I] [DecidableEq I] (p : Finset I → ℚ) (s : Finset I) : ℚ

The upper zeta transform on the Boolean lattice of subsets of a finite type.

Equations

• Finset.booleanUpperZeta p s = ∑ t : Finset I, if s ⊆ t then p t else 0

def Finset.booleanUpperMobius {I : Type u_1} [Fintype I] [DecidableEq I] (p : Finset I → ℚ) (s : Finset I) : ℚ

The signed upper Möbius transform. Its sign counts elements added above s.

Equations

• Finset.booleanUpperMobius p s = ∑ t : Finset I, if s ⊆ t then (-1) ^ (t \ s).card * p t else 0

theorem Finset.booleanUpperMobius_booleanUpperZeta {I : Type u_1} [Fintype I] [DecidableEq I] (p : Finset I → ℚ) : booleanUpperMobius (booleanUpperZeta p) = p

The signed upper Möbius transform inverts the upper zeta transform.

Executable convention regressions.