Constructing a dominating chain for ordered two-point systems

This is the finite induction used to prove the two-point case of Theorem 2.1. Its sole input is the local insertion theorem. The product law is split at the last coordinate, the induction hypothesis constructs a chain on the old coordinates, and one insertion of the new coordinate completes the step.

def Feige.StrictOrderedLocalInsertion : Prop

The uniform local conclusion needed at every induction stage, restricted to the strict ordered systems to which the analytic insertion proof applies.

Equations

• One or more equations did not get rendered due to their size.

theorem Feige.monotone_revealedLastPayoff {n : ℕ} {p : ℝ} (hp0 : 0 ≤ p) (hp1 : p ≤ 1) {g : Finset (Fin (n + 1)) → ℝ} (hg : Monotone g) : Monotone (revealedLastPayoff p g)

Revealing one independent Bernoulli coordinate preserves monotonicity of a payoff on the Boolean lattice.

theorem Feige.productHighSetExpectation_zero_eq_chain (γ β : Fin 0 → ℝ) (g : Finset (Fin 0) → ℝ) : productHighSetExpectation (twoPointHighProbability γ β) g = booleanChainExpectation γ β (Equiv.refl (Fin 0)) ⋯ ⋯ g

The unique zero-dimensional Boolean chain has the same expectation as the zero-dimensional product law.

theorem Feige.exists_chain_dominating_product_of_localInsertion (hlocal : StrictOrderedLocalInsertion) {m : ℕ} (γ β : Fin m → ℝ) (hγpos : ∀ (i : Fin m), 0 < γ i) (hγle : ∀ (i : Fin m), γ i ≤ 1) (hβpos : ∀ (i : Fin m), 0 < β i) (hγord : Antitone γ) (g : Finset (Fin m) → ℝ) (hg : Monotone g) : ∃ (σ : Equiv.Perm (Fin m)), productHighSetExpectation (twoPointHighProbability γ β) g ≤ booleanChainExpectation γ β σ ⋯ ⋯ g

The finite chain construction for strictly positive parameters already arranged in nonincreasing γ order.

theorem Feige.orderedStrictTwoPoint_rejection_le_of_localInsertion (hlocal : StrictOrderedLocalInsertion) {m : ℕ} (γ β : Fin m → ℝ) (hγpos : ∀ (i : Fin m), 0 < γ i) (hγle : ∀ (i : Fin m), γ i ≤ 1) (hβpos : ∀ (i : Fin m), 0 < β i) (hγord : Antitone γ) {α : ℝ} (hα : 0 ≤ α) : twoPointRejectionMass γ β α ≤ α

Ordered strict two-point calibration follows immediately once the local insertion theorem has been discharged.