Mathlib.Combinatorics
Finite combinatorial and spectral infrastructure for uniform subset slices and their linear operators.
BooleanCubeMobius 3 core · 3 supporting This file proves a baseline-zero, real-valued specialization of the inclusion-exclusion expansion on a finite Boolean cube. ★ mobius_expansion
Normalized Boolean-Cube Möbius Expansion
This file proves a baseline-zero, real-valued specialization of the
inclusion-exclusion expansion on a finite Boolean cube. The definition
indicator builds Boolean vectors from finite subsets, delta gives the
coefficient for a subset, and mobius_expansion recovers a function normalized
to zero at the all-zero vector as a sum of its nonempty-subset terms. The full
Möbius expansion, without the normalization, additionally contains the
empty-set coefficient.
def indicator reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.BooleanCubeMobius
For a coordinate type with decidable equality and a finite subset of coordinates, the subset-indicator Boolean vector assigns one to coordinates in the subset and zero to all other coordinates.
def delta reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.BooleanCubeMobius
For a coordinate type with decidable equality, a real-valued function on its Boolean cube, and a finite subset of coordinates, the subset Möbius coefficient is the alternating sum over the indicator vectors of all its subsets, with sign determined by the difference in subset sizes.
theorem mobius_expansion reviewed
⚑ flagged
Causalean.Mathlib.Combinatorics.BooleanCubeMobius
For a real-valued function τ on a finite Boolean cube that is normalized to zero at the all-zero vector, its value at a Boolean vector h is recovered from its nonempty-subset Möbius coefficients. A coefficient contributes only when every coordinate in its subset is one.
Formal statement
Proof (Lean source)
theorem mobius_expansion
[Fintype ι]
(τ : (ι → Fin 2) → ℝ)
(hτ0 : τ (fun _ => 0) = 0)
(h : ι → Fin 2) :
τ h =
∑ S ∈ (((Finset.univ : Finset ι).powerset.filter (·.Nonempty)) :
Finset (Finset ι)),
delta τ S * prod S (fun k => ((h k).val : ℝ)) := by
classical
let B : Finset ι := Finset.univ.filter (fun k => h k = 1)
have hBmem : ∀ k, k ∈ B ↔ h k = 1 := by
intro k
simp [B, mem_filter]
have hh_indB : h = indicator B := by
funext k
by_cases hk : k ∈ B
· have hk' := (hBmem k).1 hk
simp [indicator, hk, hk']
· have h0 : h k ≠ 1 := by
intro hh
exact hk ((hBmem k).2 hh)
have h2 : h k = 0 := by
apply Fin.ext
have hval_ne : (h k).val ≠ 1 := by
intro hv
apply h0
apply Fin.ext
simpa using hv
omega
simp [indicator, hk, h2]
let u : Finset (Finset ι) :=
(Finset.univ : Finset ι).powerset.filter (·.Nonempty)
let s : Finset (Finset ι) := B.powerset.filter (·.Nonempty)
change τ h = ∑ S ∈ u, delta τ S * prod S (fun k => ((h k).val : ℝ))
have hstep1 :
(∑ S ∈ u, delta τ S * prod S (fun k => ((h k).val : ℝ)))
= ∑ S ∈ s, delta τ S := by
have hmul :
∀ S ∈ u,
delta τ S * prod S (fun k => ((h k).val : ℝ)) =
if S ⊆ B then delta τ S else 0 := by
intro S hS
rw [prod_indicator_eq h B hBmem S]
by_cases hSB : S ⊆ B <;> simp [hSB]
rw [Finset.sum_congr rfl hmul]
have hfilter :
u.filter (fun S => S ⊆ B) = s := by
ext S
simp [u, s, and_comm]
rw [← Finset.sum_filter]
rw [hfilter]
have hstep2 :
(∑ S ∈ s, delta τ S)
= ∑ A ∈ B.powerset,
(∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0)
* τ (indicator A) := by
rw [show s = B.powerset.filter (·.Nonempty) by rfl]
calc
(∑ S ∈ B.powerset.filter (·.Nonempty), delta τ S)
= ∑ S ∈ B.powerset.filter (·.Nonempty),
∑ A ∈ B.powerset,
if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A) else 0 := by
refine Finset.sum_congr rfl ?_
intro S hS
rw [delta]
have hSsub : S ⊆ B := Finset.mem_powerset.mp (Finset.mem_filter.mp hS).1
have hcard :
(∑ A ∈ S.powerset, (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A))
= ∑ A ∈ B.powerset,
if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) * τ (indicator A) else 0 := by
rw [← Finset.sum_filter]
have hPowEq : S.powerset = B.powerset.filter (fun A => A ⊆ S) := by
ext A
constructor
· intro hAS
exact Finset.mem_filter.mpr
⟨Finset.mem_powerset.mpr ((Finset.mem_powerset.mp hAS).trans hSsub),
Finset.mem_powerset.mp hAS⟩
· intro hAS
exact Finset.mem_powerset.mpr (Finset.mem_filter.mp hAS).2
simp [hPowEq]
simp [hcard]
_ = ∑ S ∈ B.powerset.filter (·.Nonempty),
∑ A ∈ B.powerset,
(if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by
simp [ite_mul]
_ = ∑ A ∈ B.powerset,
∑ S ∈ B.powerset.filter (·.Nonempty),
(if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by
rw [Finset.sum_comm]
_ = ∑ A ∈ B.powerset,
(∑ S ∈ B.powerset.filter (·.Nonempty),
if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A) := by
simp [Finset.sum_mul]
have hstep3 :
(∑ A ∈ B.powerset,
(∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A))
= τ (indicator B) := by
have hterms :
∀ A ∈ B.powerset,
(∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) *
τ (indicator A)
= if A = B then τ (indicator B) else 0 := by
intro A hA
by_cases hA0 : A = ∅
· subst hA0
by_cases hB0 : B = ∅
· rw [hB0]
simp [hτ0]
· have hne : (∅ : Finset ι) ≠ B := by
intro h
exact hB0 h.symm
simp [hτ0, hne]
· have hAne : A.Nonempty := Finset.nonempty_iff_ne_empty.mpr hA0
have hAS : A ⊆ B := Finset.mem_powerset.mp hA
have hfilter :
s.filter (fun S => A ⊆ S) = B.powerset.filter (A ⊆ ·) := by
ext S
constructor
· intro hS
rcases Finset.mem_filter.mp hS with ⟨hSs, hSA⟩
exact Finset.mem_filter.mpr ⟨(Finset.mem_filter.mp hSs).1, hSA⟩
· intro hS
rcases Finset.mem_filter.mp hS with ⟨hSsub, hSA⟩
exact Finset.mem_filter.mpr
⟨Finset.mem_filter.mpr ⟨hSsub, hAne.mono hSA⟩, hSA⟩
have hinner :
(∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0)
= ∑ S ∈ B.powerset.filter (A ⊆ ·), (-1 : ℝ) ^ (S.card - A.card) := by
rw [← Finset.sum_filter]
have hEq : s.filter (fun S => A ⊆ S) = B.powerset.filter (A ⊆ ·) := hfilter
simp [hEq]
rw [hinner]
have hcoeff := coeff_sum A B hAS
by_cases hABeq : A = B
· subst hABeq
simp [hcoeff]
· simp [hcoeff, hABeq]
calc
(∑ A ∈ B.powerset,
(∑ S ∈ s, if A ⊆ S then (-1 : ℝ) ^ (S.card - A.card) else 0) * τ (indicator A))
= ∑ A ∈ B.powerset, if A = B then τ (indicator B) else 0 := by
exact Finset.sum_congr rfl hterms
_ = τ (indicator B) := by
rw [Finset.sum_eq_single B]
· simp
· intro A hA hAB
simp [hAB]
· intro hB
simp at hB
rw [hstep1, hstep2, hstep3]
simp [hh_indB]
3 supporting declarations (lemmas, instances)
-
prod_indicator_eqlemma — Indicator product: ∏ k ∈ S, ((h k).val : ℝ) equals 1 if S ⊆ B and 0 otherwise, where B = {k : h k = 1}.hypothesesconclusionprod S (fun k => ((h k).val : ℝ)) = if S ⊆ B then 1 else 0Proof (Lean source)
lemma prod_indicator_eq (h : ι → Fin 2) (B : Finset ι) (hB : ∀ k, k ∈ B ↔ h k = 1) (S : Finset ι) : prod S (fun k => ((h k).val : ℝ)) = if S ⊆ B then 1 else 0 := by classical by_cases hSB : S ⊆ B · rw [if_pos hSB] apply Finset.prod_eq_one intro k hk have hk1 : h k = 1 := (hB k).mp (hSB hk) rw [hk1]; simp · rw [if_neg hSB] rw [Finset.not_subset] at hSB obtain ⟨k, hkS, hkB⟩ := hSB apply Finset.prod_eq_zero hkS have h0 : h k ≠ 1 := fun hh => hkB ((hB k).mpr hh) have h2 : h k = 0 := by apply Fin.ext have hval_ne : (h k).val ≠ 1 := by intro hv apply h0 apply Fin.ext simpa using hv omega rw [h2]; simp -
coeff_sumlemma — Coefficient sum: for A ⊆ B, ∑ S, A ⊆ S ⊆ B, (-1)^(|S|-|A|) = if A = B then 1 else 0.hypothesesconclusion(∑ S ∈ B.powerset.filter (A ⊆ ·), (-1 : ℝ) ^ (S.card - A.card)) = if A = B then 1 else 0Proof (Lean source)
lemma coeff_sum (A B : Finset ι) (hAB : A ⊆ B) : (∑ S ∈ B.powerset.filter (A ⊆ ·), (-1 : ℝ) ^ (S.card - A.card)) = if A = B then 1 else 0 := by classical set C := B \ A with hCdef have hAdisj : Disjoint A C := Finset.disjoint_sdiff -- Reindex S = A ∪ T with T ⊆ C. have hreindex : (∑ S ∈ B.powerset.filter (A ⊆ ·), (-1 : ℝ) ^ (S.card - A.card)) = ∑ T ∈ C.powerset, (-1 : ℝ) ^ T.card := by refine Finset.sum_nbij' (fun S => S \ A) (fun T => A ∪ T) ?_ ?_ ?_ ?_ ?_ · intro S hS simp only [mem_filter, Finset.mem_powerset] at hS obtain ⟨hSB, _⟩ := hS exact (Finset.mem_powerset.mpr <| by intro x hx simp only [hCdef, mem_sdiff] at hx ⊢ exact ⟨hSB hx.1, hx.2⟩) · intro T hT simp only [Finset.mem_powerset] at hT simp only [mem_filter, Finset.mem_powerset] have hTC : T ⊆ C := hT have hTB : T ⊆ B := hTC.trans sdiff_subset exact ⟨Finset.union_subset hAB hTB, Finset.subset_union_left⟩ · intro S hS simp only [mem_filter, Finset.mem_powerset] at hS obtain ⟨_, hAS⟩ := hS ext x simp only [mem_union, mem_sdiff] constructor · rintro (hxA | ⟨hxS, _⟩) · exact hAS hxA · exact hxS · intro hxS by_cases hxA : x ∈ A · exact inl hxA · exact inr ⟨hxS, hxA⟩ · intro T hT simp only [Finset.mem_powerset] at hT have hTC : T ⊆ C := hT have hTA : Disjoint A T := Finset.disjoint_of_subset_right hTC hAdisj ext x simp only [mem_sdiff, mem_union] constructor · rintro ⟨hxA | hxT, hxnA⟩ · exact (hxnA hxA).elim · exact hxT · intro hxT refine ⟨Or.inr hxT, ?_⟩ intro hxA exact (Finset.disjoint_left.mp hTA hxA) hxT · intro S hS simp only [mem_filter, Finset.mem_powerset] at hS obtain ⟨_, hAS⟩ := hS rw [Finset.card_sdiff_of_subset hAS] rw [hreindex] by_cases hAB' : A = B · subst hAB' have hC0 : C = ∅ := by simp [hCdef] simp [hC0] · have hCne : C ≠ ∅ := by intro hC0 apply hAB' refine le_antisymm hAB ?_ intro x hxB by_contra hxA have hxC : x ∈ C := by simp [hCdef, hxB, hxA] rw [hC0] at hxC exact Finset.notMem_empty _ hxC have hCne' : C.Nonempty := Finset.nonempty_iff_ne_empty.mpr hCne have hint : (∑ T ∈ C.powerset, (-1 : ℤ) ^ T.card) = 0 := Finset.sum_powerset_neg_one_pow_card_of_nonempty (x := C) hCne' have hreal : (∑ T ∈ C.powerset, (-1 : ℝ) ^ T.card) = 0 := by exact_mod_cast hint simpa [hAB'] using hreal