Reduction from exact calibration to Feige's inequality

This file formalizes the reduction in §2.2 at δ = 1. The calibration theorem and the deterministic simplex bridge are exposed as separate hypotheses. The result here is the shift, bad-event inclusion, and complement argument in the proof of Theorem 1.1.

def Feige.LargeSumBridge {n : ℕ} (K : (Fin n → ℝ) → ℝ) : Prop

Abstract form of the δ = 1 geometric estimate in §2.2: a nonnegative vector with ordinary sum at least n + 1 has Dirichlet statistic at most 1 - bₙ,₁.

Equations

• Feige.LargeSumBridge K = ∀ (y : Fin n → ℝ), (∀ (i : Fin n), 0 ≤ y i) → ↑n + 1 ≤ ∑ i : Fin n, y i → K y ≤ 1 - Feige.sharpConstant n

def Feige.FixedDimensionalFeigeLowerBound (n : ℕ) (c : ℝ) : Prop

A candidate lower bound for the fixed-dimensional unit-slack Feige inequality, quantified over all admissible probability spaces and random variables.

Equations

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

noncomputable def Feige.shifted {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {n : ℕ} (X : Fin n → Ω → ℝ) (i : Fin n) (ω : Ω) : ℝ

The shifted variables Yᵢ = Xᵢ + 1 - E Xᵢ used in the proof of Theorem 1.1 in §2.2.

Equations

• Feige.shifted μ X i ω = X i ω + 1 - ∫ (ω' : Ω), X i ω' ∂μ

theorem Feige.sharp_feige_of_calibration_and_largeSumBridge {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) [MeasureTheory.IsProbabilityMeasure μ] {n : ℕ} (K : (Fin n → ℝ) → ℝ) (hcal : CalibrationProperty μ K) (hbridge : LargeSumBridge K) (X : Fin n → Ω → ℝ) (hX_meas : ∀ (i : Fin n), Measurable (X i)) (hX_int : ∀ (i : Fin n), MeasureTheory.Integrable (X i) μ) (hX_indep : ProbabilityTheory.iIndepFun X μ) (hX_nonneg : ∀ (i : Fin n) (ω : Ω), 0 ≤ X i ω) (hX_mean : ∀ (i : Fin n), ∫ (ω : Ω), X i ω ∂μ ≤ 1) : sharpConstant n ≤ μ.real {ω : Ω | ∑ i : Fin n, X i ω < ∫ (ω' : Ω), ∑ i : Fin n, X i ω' ∂μ + 1}

The δ = 1 reduction in §2.2: exact calibration and the deterministic bridge imply the sharp fixed-dimensional bound for the strict event ∑ Xᵢ < E(∑ Xᵢ) + 1.

theorem Feige.sharpConstant_is_lowerBound_of_structural_inputs {n : ℕ} (K : (Fin n → ℝ) → ℝ) (hcal : UniversalCalibration K) (hbridge : LargeSumBridge K) : FixedDimensionalFeigeLowerBound n (sharpConstant n)

The two structural inputs imply that sharpConstant n is a valid fixed-dimensional lower bound.