Finite expectations in the two-point calibration argument

This file defines the independent product expectation and the rejection payoff used by the ordered insertion proof.

noncomputable def Feige.productHighSetExpectation {m : ℕ} (p : Fin m → ℝ) (g : Finset (Fin m) → ℝ) : ℝ

Expectation under the independent product law on high sets.

Equations

• Feige.productHighSetExpectation p g = ∑ S ∈ Finset.univ.powerset, Feige.highSetMass p S * g S

@[simp]

theorem Feige.productHighSetExpectation_one {m : ℕ} (p : Fin m → ℝ) : (productHighSetExpectation p fun (x : Finset (Fin m)) => 1) = 1

theorem Feige.monotone_booleanRejectionPayoff {m : ℕ} (γ β : Fin m → ℝ) (hγ : ∀ (i : Fin m), 0 ≤ γ i) (hβ : ∀ (i : Fin m), 0 ≤ β i) (α : ℝ) : Monotone (booleanRejectionPayoff γ β α)

Rejection is an increasing payoff because K is antitone on the Boolean lattice.

theorem Feige.productExpectation_rejection_eq {m : ℕ} (γ β : Fin m → ℝ) (α : ℝ) : productHighSetExpectation (twoPointHighProbability γ β) (booleanRejectionPayoff γ β α) = twoPointRejectionMass γ β α