Mixtures of couplings #
Let Λ be a law, A a set of coordinates to keep, and W a finite set of coordinates
outside A to choose. A coupling chooses the signs on W as a function of the signs on
a finite set U ⊆ A. If every nonnegative combination of finitely many costs, each a
function of the coordinates in U ∪ W, has expected optimal value at most the same
combination of the bounds c i, then the finite minimax lemma gives a mixture of
couplings meeting every bound at once. The mixture keeps the marginals of Λ on A.
theorem
Erdos111.exists_mixture
{V : Type u_1}
{r : ℕ}
(Λ : MeasureTheory.Measure (V → Bool))
[MeasureTheory.IsProbabilityMeasure Λ]
(A : Set V)
(U W : Finset V)
(hW : ∀ w ∈ W, w ∉ A)
(f : Fin r → (V → Bool) → ℕ)
(hf : ∀ (i : Fin r), DependsOn (f i) (↑U ∪ ↑W))
(c : Fin r → NNReal)
(hkey :
∀ (ρ : Fin r → NNReal),
∫⁻ (τ : V → Bool), ⨅ (η : V → Bool), ∑ i : Fin r, ↑(ρ i) * ↑(f i (W.piecewise η τ)) ∂Λ ≤ ∑ i : Fin r, ↑(ρ i) * ↑(c i))
:
A mixture of couplings that choose the signs on W meets finitely many expected-cost
bounds at once, if every nonnegative combination of them is met by optimal choices.