The fixed-dimensional extremal example

This file formalizes the sharpness construction from §1.2 at δ = 1. The sample space is (Fin n → Fin (n + 1)), with its uniform law. Coordinate i is n + 1 when the ith digit is zero, and is zero otherwise. Thus every coordinate has the two-point law used in the proof outline.

@[reducible, inline]

abbrev Feige.ExtremalSpace (n : ℕ) : Type

The finite product sample space for the sharpness example.

Equations

• Feige.ExtremalSpace n = (Fin n → Fin (n + 1))

noncomputable def Feige.extremalMarginal (n : ℕ) : MeasureTheory.Measure (Fin (n + 1))

The uniform probability measure on the extremal sample space.

Equations

• Feige.extremalMarginal n = (PMF.uniformOfFintype (Fin (n + 1))).toMeasure

noncomputable def Feige.extremalMeasure (n : ℕ) : MeasureTheory.Measure (ExtremalSpace n)

The product of the uniform one-coordinate measures.

Equations

• Feige.extremalMeasure n = MeasureTheory.Measure.pi fun (x : Fin n) => Feige.extremalMarginal n

instance Feige.instIsProbabilityMeasureFinHAddNatOfNatExtremalMarginal (n : ℕ) : MeasureTheory.IsProbabilityMeasure (extremalMarginal n)

instance Feige.instIsProbabilityMeasureExtremalSpaceExtremalMeasure (n : ℕ) : MeasureTheory.IsProbabilityMeasure (extremalMeasure n)

noncomputable def Feige.extremalX (n : ℕ) (i : Fin n) (ω : ExtremalSpace n) : ℝ

The ith coordinate of the δ = 1 sharpness construction in §1.2.

Equations

• Feige.extremalX n i ω = if ω i = 0 then ↑n + 1 else 0

noncomputable def Feige.extremalSum (n : ℕ) (ω : ExtremalSpace n) : ℝ

The sum of all coordinates in the sharpness construction.

Equations

• Feige.extremalSum n ω = ∑ i : Fin n, Feige.extremalX n i ω

def Feige.allLowEmbedding (n : ℕ) : (Fin n → Fin n) → ExtremalSpace n

Embed the n nonzero digits into the n + 1 possible digits.

Equations

• Feige.allLowEmbedding n ω i = (ω i).succ

theorem Feige.allLowEmbedding_injective (n : ℕ) : Function.Injective (allLowEmbedding n)

def Feige.extremalGood (n : ℕ) : Set (ExtremalSpace n)

The good event consists precisely of choices with no zero digit.

Equations

• Feige.extremalGood n = Set.range (Feige.allLowEmbedding n)

@[instance_reducible]

instance Feige.instFintypeElemExtremalSpaceExtremalGood (n : ℕ) : Fintype ↑(extremalGood n)

Equations

• Feige.instFintypeElemExtremalSpaceExtremalGood n = Set.fintypeRange (Feige.allLowEmbedding n)

theorem Feige.mem_extremalGood_iff (n : ℕ) (ω : ExtremalSpace n) : ω ∈ extremalGood n ↔ ∀ (i : Fin n), ω i ≠ 0

@[simp]

theorem Feige.extremalX_eq_zero_iff (n : ℕ) (i : Fin n) (ω : ExtremalSpace n) : extremalX n i ω = 0 ↔ ω i ≠ 0

theorem Feige.extremalX_nonneg (n : ℕ) (i : Fin n) (ω : ExtremalSpace n) : 0 ≤ extremalX n i ω

theorem Feige.extremalX_measurable (n : ℕ) (i : Fin n) : Measurable (extremalX n i)

theorem Feige.extremalX_integrable (n : ℕ) (i : Fin n) : MeasureTheory.Integrable (extremalX n i) (extremalMeasure n)

theorem Feige.extremalMarginal_mean (n : ℕ) : ∫ (x : Fin (n + 1)), if x = 0 then ↑n + 1 else 0 ∂extremalMarginal n = 1

theorem Feige.extremalX_mean (n : ℕ) (i : Fin n) : ∫ (ω : ExtremalSpace n), extremalX n i ω ∂extremalMeasure n = 1

theorem Feige.extremalX_iIndepFun (n : ℕ) : ProbabilityTheory.iIndepFun (extremalX n) (extremalMeasure n)

theorem Feige.extremalSum_lt_iff (n : ℕ) (ω : ExtremalSpace n) : extremalSum n ω < ↑n + 1 ↔ ω ∈ extremalGood n

Because the threshold is strict, the good event occurs exactly when all coordinates vanish.

theorem Feige.card_extremalGood (n : ℕ) : Fintype.card ↑(extremalGood n) = n ^ n

theorem Feige.card_extremalSpace (n : ℕ) : Fintype.card (ExtremalSpace n) = (n + 1) ^ n

theorem Feige.extremalGood_probability (n : ℕ) : (extremalMeasure n).real (extremalGood n) = sharpConstant n

The probability of the strict good event in the extremal construction is exactly the fixed-dimensional constant cₙ.

theorem Feige.extremal_strict_event_probability (n : ℕ) : (extremalMeasure n).real {ω : ExtremalSpace n | extremalSum n ω < ↑n + 1} = sharpConstant n

Under the uniform product model from the sharpness paragraph in §1.2, the strict threshold event has probability exactly bₙ,₁.

theorem Feige.extremalSum_mean (n : ℕ) : ∫ (ω : ExtremalSpace n), extremalSum n ω ∂extremalMeasure n = ↑n

The threshold in the sharpness example is exactly E Sₙ + 1 = n + 1.

theorem Feige.extremal_mean_threshold_probability (n : ℕ) : (extremalMeasure n).real {ω : ExtremalSpace n | extremalSum n ω < ∫ (ω' : ExtremalSpace n), extremalSum n ω' ∂extremalMeasure n + 1} = sharpConstant n

The full sharpness statement, with the threshold written in the form used in Feige's inequality.

theorem Feige.fixedDimensionalLowerBound_le_sharpConstant {n : ℕ} {c : ℝ} (h : FixedDimensionalFeigeLowerBound n c) : c ≤ sharpConstant n

The sharpness construction in §1.2 proves that no fixed-dimensional unit-slack lower bound can exceed sharpConstant n.

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

A lower bound is optimal when every other valid lower bound is no larger.

Equations

• Feige.IsOptimalFixedDimensionalFeigeBound n c = (Feige.FixedDimensionalFeigeLowerBound n c ∧ ∀ (d : ℝ), Feige.FixedDimensionalFeigeLowerBound n d → d ≤ c)

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

Conditional on exact calibration and the deterministic bridge, the paper's unit-slack constant is not only valid but optimal; the sharpness construction in §1.2 supplies the reverse extremal statement.