Exact calibration interfaces

This file contains the probability/calibration interfaces shared by the Vlassis--Thomas theorem and the reduction to Feige's inequality.

def Feige.CalibrationProperty {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) {n : ℕ} (K : (Fin n → ℝ) → ℝ) : Prop

Abstract form of Theorem 2.1: K is super-uniform for every independent family of nonnegative random variables whose coordinate means are at most one.

Equations

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

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

The calibration property, uniformly over all (small-universe) probability spaces.

Equations

• Feige.UniversalCalibration K = ∀ (Ω : Type) (x : MeasurableSpace Ω) (μ : MeasureTheory.Measure Ω), MeasureTheory.IsProbabilityMeasure μ → Feige.CalibrationProperty μ K