English
Let α be a distributive lattice and β a linearly ordered, strictly ordered semiring with an additive structure; for nonnegative functions f1, f2, f3, f4: α → β satisfying f1(a) f2(b) ≤ f3(a ∧ b) f4(a ∨ b) for all a, b ∈ α, and for any finite subsets s, t of α, we have (sum over s of f1) · (sum over t of f2) ≤ (sum over s ⊼ t of f3) · (sum over s ⊻ t of f4).
Русский
Пусть α — распределительная решётка, β — линейно упорядоченная полугруппа с суммированием; для неотрицательных функций f1, f2, f3, f4: α → β, удовлетворяющих f1(a) f2(b) ≤ f3(a ∧ b) f4(a ∨ b) для всех a, b ∈ α, для любых конечных подмножеств s, t ⊆ α выполняется неравенство (∑_{a∈s} f1(a)) (∑_{a∈t} f2(a)) ≤ (∑_{a∈s ⊼ t} f3(a)) (∑_{a∈s ⊻ t} f4(a)).
LaTeX
$$$$\\text{Let } \\alpha \\text{ be a distributive lattice and } \\beta \\text{ a linearly ordered ring-like semiring. \\\\ \nIf } f_1,f_2,f_3,f_4:\\alpha\\to\\mathbb{R}_{\\ge 0} \\text{ satisfy } f_1(a) f_2(b) \\le f_3(a \\wedge b) f_4(a \\vee b) \\text{ for all } a,b\\in\\alpha, \\\\ \n\\text{then for all finite } s,t\\subseteq\\alpha, \\\\ \n\\left(\\sum_{a\\in s} f_1(a)\\right)\\left(\\sum_{a\\in t} f_2(a)\\right) \\le \\left(\\sum_{a\\in s \\sqcap t} f_3(a)\\right)\\left(\\sum_{a\\in s \\sqcup t} f_4(a)\\right).$$$$
Lean4
/-- The **Four Functions Theorem**, aka **Ahlswede-Daykin Inequality**. -/
theorem four_functions_theorem [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 t : Finset α) :
(∑ a ∈ s, f₁ a) * ∑ a ∈ t, f₂ a ≤ (∑ a ∈ s ⊼ t, f₃ a) * ∑ a ∈ s ⊻ t, f₄ a := by
classical
set L : Sublattice α := ⟨latticeClosure (s ∪ t), isSublattice_latticeClosure.1, isSublattice_latticeClosure.2⟩
have : Finite L := (s.finite_toSet.union t.finite_toSet).latticeClosure.to_subtype
set s' : Finset L := s.preimage (↑) Subtype.coe_injective.injOn
set t' : Finset L := t.preimage (↑) Subtype.coe_injective.injOn
have hs' : s'.map ⟨L.subtype, Subtype.coe_injective⟩ = s := by
simpa [s', map_eq_image, image_preimage, filter_eq_self] using fun a ha ↦
subset_latticeClosure <| Set.subset_union_left ha
have ht' : t'.map ⟨L.subtype, Subtype.coe_injective⟩ = t := by
simpa [t', map_eq_image, image_preimage, filter_eq_self] using fun a ha ↦
subset_latticeClosure <| Set.subset_union_right ha
clear_value s' t'
obtain ⟨β, _, _, g, hg⟩ := exists_birkhoff_representation L
have :=
four_functions_theorem_aux (extend g (f₁ ∘ (↑)) 0) (extend g (f₂ ∘ (↑)) 0) (extend g (f₃ ∘ (↑)) 0)
(extend g (f₄ ∘ (↑)) 0) (extend_nonneg (fun _ ↦ h₁ _) le_rfl) (extend_nonneg (fun _ ↦ h₂ _) le_rfl)
(extend_nonneg (fun _ ↦ h₃ _) le_rfl) (extend_nonneg (fun _ ↦ h₄ _) le_rfl) ?_ (s'.map ⟨g, hg⟩) (t'.map ⟨g, hg⟩)
· simpa only [← hs', ← ht', ← map_sups, ← map_infs, sum_map, Embedding.coeFn_mk, hg.extend_apply] using this
rintro s t
classical
obtain ⟨a, rfl⟩ | hs := em (∃ a, g a = s)
· obtain ⟨b, rfl⟩ | ht := em (∃ b, g b = t)
· simp_rw [← sup_eq_union, ← inf_eq_inter, ← map_sup, ← map_inf, hg.extend_apply]
exact h _ _
·
simpa [extend_apply' _ _ _ ht] using
mul_nonneg (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)
·
simpa [extend_apply' _ _ _ hs] using
mul_nonneg (extend_nonneg (fun a : L ↦ h₃ a) le_rfl _) (extend_nonneg (fun a : L ↦ h₄ a) le_rfl _)
