The four functions theorem and corollaries #

This file proves the four functions theorem. The statement is that if f₁ a * f₂ b ≤ f₃ (a ⊓ b) * f₄ (a ⊔ b) for all a, b in a finite distributive lattice, then (∑ x ∈ s, f₁ x) * (∑ x ∈ t, f₂ x) ≤ (∑ x ∈ s ⊼ t, f₃ x) * (∑ x ∈ s ⊻ t, f₄ x) where s ⊼ t = {a ⊓ b | a ∈ s, b ∈ t}, s ⊻ t = {a ⊔ b | a ∈ s, b ∈ t}.

The proof uses Birkhoff's representation theorem to restrict to the case where the finite distributive lattice is in fact a finite powerset algebra, namely Finset α for some finite α. Then it proves this new statement by induction on the size of α.

Main declarations #

The two versions of the four functions theorem are

• Finset.four_functions_theorem for finite powerset algebras.
• four_functions_theorem for any finite distributive lattices.

We deduce a number of corollaries:

• Finset.le_card_infs_mul_card_sups: Daykin inequality. |s| |t| ≤ |s ⊼ t| |s ⊻ t|
• holley: Holley inequality.
• fkg: Fortuin-Kastelyn-Ginibre inequality.
• Finset.card_le_card_diffs: Marica-Schönheim inequality. |s| ≤ |{a \ b | a, b ∈ s}|

TODO #

Prove that lattices in which Finset.le_card_infs_mul_card_sups holds are distributive. See Daykin, A lattice is distributive iff |A| |B| <= |A ∨ B| |A ∧ B|

Prove the Fishburn-Shepp inequality.

Is collapse a construct generally useful for set family inductions? If so, we should move it to an earlier file and give it a proper API.

References #

Applications of the FKG Inequality and Its Relatives, Graham

theorem collapse_eq {α : Type u_1} {β : Type u_2} [] {a : α} {s : } (ha : as) (𝒜 : Finset (Finset α)) (f : β) :
collapse 𝒜 a f s = (if s 𝒜 then f s else 0) + if insert a s 𝒜 then f (insert a s) else 0
theorem collapse_of_mem {α : Type u_1} {β : Type u_2} [] {𝒜 : Finset (Finset α)} {a : α} {f : β} {s : } {t : } {u : } (ha : as) (ht : t 𝒜) (hu : u 𝒜) (hts : t = s) (hus : u = insert a s) :
collapse 𝒜 a f s = f t + f u
theorem le_collapse_of_mem {α : Type u_1} {β : Type u_2} [] {𝒜 : Finset (Finset α)} {a : α} {f : β} {s : } {t : } (ha : as) (hf : 0 f) (hts : t = s) (ht : t 𝒜) :
f t collapse 𝒜 a f s
theorem le_collapse_of_insert_mem {α : Type u_1} {β : Type u_2} [] {𝒜 : Finset (Finset α)} {a : α} {f : β} {s : } {t : } (ha : as) (hf : 0 f) (hts : t = insert a s) (ht : t 𝒜) :
f t collapse 𝒜 a f s
theorem collapse_nonneg {α : Type u_1} {β : Type u_2} [] {𝒜 : Finset (Finset α)} {a : α} {f : β} (hf : 0 f) :
0 collapse 𝒜 a f
theorem collapse_modular {α : Type u_1} {β : Type u_2} [] {a : α} {f₁ : β} {f₂ : β} {f₃ : β} {f₄ : β} {u : } [] (hu : au) (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ ⦃s : ⦄, s insert a u∀ ⦃t : ⦄, t insert a uf₁ s * f₂ t f₃ (s t) * f₄ (s t)) (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) ⦃s : :
s u∀ ⦃t : ⦄, t ucollapse 𝒜 a f₁ s * collapse a f₂ t collapse (𝒜 ) a f₃ (s t) * collapse (𝒜 ) a f₄ (s t)
theorem sum_collapse {α : Type u_1} {β : Type u_2} [] {𝒜 : Finset (Finset α)} {a : α} {f : β} {u : } (h𝒜 : 𝒜 (insert a u).powerset) (hu : au) :
su.powerset, collapse 𝒜 a f s = s𝒜, f s
theorem Finset.four_functions_theorem {α : Type u_1} {β : Type u_2} [] {f₁ : β} {f₂ : β} {f₃ : β} {f₄ : β} [] (u : ) (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ ⦃s : ⦄, s u∀ ⦃t : ⦄, t uf₁ s * f₂ t f₃ (s t) * f₄ (s t)) {𝒜 : Finset (Finset α)} {ℬ : Finset (Finset α)} (h𝒜 : 𝒜 u.powerset) (hℬ : u.powerset) :
(∑ s𝒜, f₁ s) * s, f₂ s (∑ s𝒜 , f₃ s) * s𝒜 , f₄ s

The Four Functions Theorem on a powerset algebra. See four_functions_theorem for the finite distributive lattice generalisation.

theorem four_functions_theorem {α : Type u_1} {β : Type u_2} [] [] (f₁ : αβ) (f₂ : αβ) (f₃ : αβ) (f₄ : αβ) [] (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ (a b : α), f₁ a * f₂ b f₃ (a b) * f₄ (a b)) (s : ) (t : ) :
(∑ as, f₁ a) * at, f₂ a (∑ as t, f₃ a) * as t, f₄ a

The Four Functions Theorem, aka Ahlswede-Daykin Inequality.

theorem Finset.le_card_infs_mul_card_sups {α : Type u_1} [] [] (s : ) (t : ) :
s.card * t.card (s t).card * (s t).card

An inequality of Daykin. Interestingly, any lattice in which this inequality holds is distributive.

theorem four_functions_theorem_univ {α : Type u_1} {β : Type u_2} [] [] (f₁ : αβ) (f₂ : αβ) (f₃ : αβ) (f₄ : αβ) [] (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ (a b : α), f₁ a * f₂ b f₃ (a b) * f₄ (a b)) :
(∑ a : α, f₁ a) * a : α, f₂ a (∑ a : α, f₃ a) * a : α, f₄ a

Special case of the Four Functions Theorem when s = t = univ.

theorem holley {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (g : αβ) (μ : αβ) [] (hμ₀ : 0 μ) (hf : 0 f) (hg : 0 g) (hμ : ) (hfg : a : α, f a = a : α, g a) (h : ∀ (a b : α), f a * g b f (a b) * g (a b)) :
a : α, μ a * f a a : α, μ a * g a

The Holley Inequality.

theorem fkg {α : Type u_1} {β : Type u_2} [] [] (f : αβ) (g : αβ) (μ : αβ) [] (hμ₀ : 0 μ) (hf₀ : 0 f) (hg₀ : 0 g) (hf : ) (hg : ) (hμ : ∀ (a b : α), μ a * μ b μ (a b) * μ (a b)) :
(∑ a : α, μ a * f a) * a : α, μ a * g a (∑ a : α, μ a) * a : α, μ a * (f a * g a)

The Fortuin-Kastelyn-Ginibre Inequality.

theorem Finset.le_card_diffs_mul_card_diffs {α : Type u_1} [] (s : ) (t : ) :
s.card * t.card (s.diffs t).card * (t.diffs s).card

A slight generalisation of the Marica-Schönheim Inequality.

theorem Finset.card_le_card_diffs {α : Type u_1} [] (s : ) :
s.card (s.diffs s).card

The Marica-Schönheim Inequality.