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 ∈ 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

We deduce a number of corollaries:

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][Graham1983]

theorem collapse_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] [LinearOrderedCommSemiring β] {a : α} {s : Finset α} (ha : as) (𝒜 : Finset (Finset α)) (f : Finset αβ) :
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} [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset αβ} {s : Finset α} {t : Finset α} {u : Finset α} (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} [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset αβ} {s : Finset α} {t : Finset α} (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} [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset αβ} {s : Finset α} {t : Finset α} (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} [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset αβ} (hf : 0 f) :
0 collapse 𝒜 a f
theorem collapse_modular {α : Type u_1} {β : Type u_2} [DecidableEq α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] {a : α} {f₁ : Finset αβ} {f₂ : Finset αβ} {f₃ : Finset αβ} {f₄ : Finset αβ} {u : Finset α} (hu : au) (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ ⦃s : Finset α⦄, s insert a u∀ ⦃t : Finset α⦄, t insert a uf₁ s * f₂ t f₃ (s t) * f₄ (s t)) (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) ⦃s : Finset α :
s u∀ ⦃t : Finset α⦄, 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} [DecidableEq α] [LinearOrderedCommSemiring β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset αβ} {u : Finset α} (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} [DecidableEq α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] {f₁ : Finset αβ} {f₂ : Finset αβ} {f₃ : Finset αβ} {f₄ : Finset αβ} (u : Finset α) (h₁ : 0 f₁) (h₂ : 0 f₂) (h₃ : 0 f₃) (h₄ : 0 f₄) (h : ∀ ⦃s : Finset α⦄, s u∀ ⦃t : Finset α⦄, 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} [DistribLattice α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f₁ : αβ) (f₂ : αβ) (f₃ : αβ) (f₄ : αβ) [DecidableEq α] (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 : Finset α) (t : Finset α) :
(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} [DistribLattice α] [DecidableEq α] (s : Finset α) (t : Finset α) :
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} [DistribLattice α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f₁ : αβ) (f₂ : αβ) (f₃ : αβ) (f₄ : αβ) [Fintype α] (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} [DistribLattice α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f : αβ) (g : αβ) (μ : αβ) [Fintype α] (hμ₀ : 0 μ) (hf : 0 f) (hg : 0 g) (hμ : Monotone μ) (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} [DistribLattice α] [LinearOrderedCommSemiring β] [ExistsAddOfLE β] (f : αβ) (g : αβ) (μ : αβ) [Fintype α] (hμ₀ : 0 μ) (hf₀ : 0 f) (hg₀ : 0 g) (hf : Monotone f) (hg : Monotone g) (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} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) (t : Finset α) :
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} [DecidableEq α] [GeneralizedBooleanAlgebra α] (s : Finset α) :
s.card (s.diffs s).card

The Marica-Schönheim Inequality.