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

theorem collapse_eq {α : Type u_1} {β : Type u_2} [DecidableEq α] [LinearOrderedCommSemiring β] {a : α} {s : Finset α} (ha : a ∉ s) (𝒜 : 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 : a ∉ s) (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 : a ∉ s) (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 : a ∉ s) (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 β] {a : α} {f₁ : Finset α → β} {f₂ : Finset α → β} {f₃ : Finset α → β} {f₄ : Finset α → β} {u : Finset α} [ExistsAddOfLE β] (hu : a ∉ u) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄) (h : ∀ ⦃s : Finset α⦄, s ⊆ insert a u → ∀ ⦃t : Finset α⦄, t ⊆ insert a u → f₁ s * f₂ t ≤ f₃ (s ∩ t) * f₄ (s ∪ t)) (𝒜 : Finset (Finset α)) (ℬ : Finset (Finset α)) ⦃s : Finset α⦄ : s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → collapse 𝒜 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 : a ∉ u) : ∑ s ∈ u.powerset, collapse 𝒜 a f s = ∑ s ∈ 𝒜, f s

theorem Finset.four_functions_theorem {α : Type u_1} {β : Type u_2} [DecidableEq α] [LinearOrderedCommSemiring β] {f₁ : Finset α → β} {f₂ : Finset α → β} {f₃ : Finset α → β} {f₄ : Finset α → β} [ExistsAddOfLE β] (u : Finset α) (h₁ : 0 ≤ f₁) (h₂ : 0 ≤ f₂) (h₃ : 0 ≤ f₃) (h₄ : 0 ≤ f₄) (h : ∀ ⦃s : Finset α⦄, s ⊆ u → ∀ ⦃t : Finset α⦄, t ⊆ u → f₁ 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 α) : (∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ 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.