---
tag: 4085B8A528
kind: statement
role: theorem
name: Ahlswede–Daykin inequality
msc: [05D05, 06D99, "60E15"]
uses: [0HM0HQCK6N]
about: [0HM0HQCK6N]
sources:
  - url: https://en.wikipedia.org/wiki/Ahlswede–Daykin_inequality
same_as:
  wikidata: Q4695203
  wikipedia: Ahlswede–Daykin inequality
---

## Statement

Let $L$ be a finite [[distributive lattice|0HM0HQCK6N]] with join $\vee$ and meet $\wedge$.
Let $f_1, f_2, f_3, f_4 \colon L \to [0, \infty)$ be functions such that
$$f_1(x) \, f_2(y) \le f_3(x \vee y) \, f_4(x \wedge y) \quad \text{for all } x, y \in L.$$
For $A, B \subseteq L$, let $A \vee B = \set{a \vee b : a \in A, b \in B}$, let $A \wedge B = \set{a \wedge b : a \in A, b \in B}$, and let $f(A) = \sum_{a \in A} f(a)$.
Then
$$f_1(A) \, f_2(B) \le f_3(A \vee B) \, f_4(A \wedge B) \quad \text{for all } A, B \subseteq L.$$

## Remarks

It is also called the four functions theorem.
Every finite distributive lattice embeds in the lattice of subsets of a finite set, so it suffices to treat the power set of $\set{1, \ldots, n}$.
The proof is by induction on $n$; the case $n = 1$ is a direct check of an inequality between four products of nonnegative numbers.

Example: with all four functions equal to $1$, the hypothesis holds and the conclusion is $|A| \, |B| \le |A \vee B| \, |A \wedge B|$ for any subsets $A, B$ of $L$.
Taking $f_1 = f_2 = f_3 = f_4 = \mu$ for a function $\mu$ with $\mu(x)\mu(y) \le \mu(x \vee y)\mu(x \wedge y)$ gives the FKG inequality and, as a special case, the [[Harris inequality|W1YH3YD3S4]].

## Explanations

### L1 human

The theorem turns an inequality between single elements into the same inequality between whole sets of elements.
Suppose the weights of any $x$ and $y$ are controlled by the weights of their join and meet.
Then the total weights of two sets are controlled by the total weights of all their joins and meets.

### L2 human

The four functions theorem is the common source of the correlation inequalities of combinatorics.
It contains the FKG inequality, the [[Harris inequality|W1YH3YD3S4]] and Kleitman's lemma on monotone families of sets.
These are used for random graphs, percolation and the statistical mechanics of spin systems, where increasing events tend to occur together.