# Documentation

Mathlib.Combinatorics.SetFamily.FourFunctions

# 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 in s, f₁ x) * (∑ x in t, f₂ x) ≤ (∑ x in s ⊼ t, f₃ x) * (∑ x in 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.

theorem collapse_eq {α : Type u_1} {β : Type u_2} [] {a : α} {s : } (ha : as) (𝒜 : 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 ()} {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 ()} {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 ()} {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 ()} {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 ()) ⦃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 ()} {a : α} {f : β} {u : } (h𝒜 : 𝒜 Finset.powerset (insert a u)) (hu : au) :
(Finset.sum () fun (s : ) => collapse 𝒜 a f s) = Finset.sum 𝒜 fun (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 ()} (h𝒜 : ) (hℬ : ) :
((Finset.sum 𝒜 fun (s : ) => f₁ s) * Finset.sum fun (s : ) => f₂ s) (Finset.sum (𝒜 ) fun (s : ) => f₃ s) * Finset.sum (𝒜 ) fun (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 : ) :
((Finset.sum s fun (a : α) => f₁ a) * Finset.sum t fun (a : α) => f₂ a) (Finset.sum (s t) fun (a : α) => f₃ a) * Finset.sum (s t) fun (a : α) => f₄ a

The Four Functions Theorem, aka Ahlswede-Daykin Inequality.

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

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)) :
((Finset.sum Finset.univ fun (a : α) => f₁ a) * Finset.sum Finset.univ fun (a : α) => f₂ a) (Finset.sum Finset.univ fun (a : α) => f₃ a) * Finset.sum Finset.univ fun (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 : (Finset.sum Finset.univ fun (a : α) => f a) = Finset.sum Finset.univ fun (a : α) => g a) (h : ∀ (a b : α), f a * g b f (a b) * g (a b)) :
(Finset.sum Finset.univ fun (a : α) => μ a * f a) Finset.sum Finset.univ fun (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)) :
((Finset.sum Finset.univ fun (a : α) => μ a * f a) * Finset.sum Finset.univ fun (a : α) => μ a * g a) (Finset.sum Finset.univ fun (a : α) => μ a) * Finset.sum Finset.univ fun (a : α) => μ a * (f a * g a)

The Fortuin-Kastelyn-Ginibre Inequality.

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

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

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

The Marica-Schönheim Inequality.