An exponential representation of the Dirichlet statistic

Equation (2.1) defines Kₙ using a uniform point of the standard simplex. For the formal proof of Theorem 2.1, this file uses the equivalent independent-rate-one-exponential representation. Its identification with the simplex statistic in (2.1) is isolated in a later geometry module.

The coordinate indexed by none is E₀; some i is Eᵢ. We put the exponentials on ℝ≥0, so their nonnegativity is encoded by the type and the coordinatewise antitonicity of K is a pointwise set inclusion.

noncomputable def Feige.nnexpMeasure : MeasureTheory.Measure NNReal

The rate-one exponential law, pushed to ℝ≥0.

The source exponential law is already supported on the nonnegative reals. Using the push-forward makes nonnegativity definitional in all later finite sum arguments.

Equations

• Feige.nnexpMeasure = MeasureTheory.Measure.map Real.toNNReal (ProbabilityTheory.expMeasure 1)

instance Feige.nnexpMeasure.isProbabilityMeasure : MeasureTheory.IsProbabilityMeasure nnexpMeasure

noncomputable def Feige.expProductMeasure (ι : Type u_1) [Fintype ι] : MeasureTheory.Measure (Option ι → NNReal)

The joint law of E₀ and an ι-indexed family of independent rate-one exponentials.

Equations

• Feige.expProductMeasure ι = MeasureTheory.Measure.pi fun (x : Option ι) => Feige.nnexpMeasure

instance Feige.expProductMeasure.isProbabilityMeasure (ι : Type u_1) [Fintype ι] : MeasureTheory.IsProbabilityMeasure (expProductMeasure ι)

def Feige.kEvent {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : Set (Option ι → NNReal)

The exponential event corresponding to the simplex event in (2.1).

Equations

• Feige.kEvent y = {e : Option ι → NNReal | ∑ i : ι, (y i - 1) * ↑(e (some i)) ≤ ↑(e none)}

theorem Feige.measurableSet_kEvent {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : MeasurableSet (kEvent y)

noncomputable def Feige.dirichletK {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : ℝ

The Dirichlet statistic from (2.1), represented internally by independent rate-one exponentials.

Equations

• Feige.dirichletK y = (Feige.expProductMeasure ι).real (Feige.kEvent y)

theorem Feige.dirichletK_nonneg {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : 0 ≤ dirichletK y

theorem Feige.dirichletK_le_one {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : dirichletK y ≤ 1

theorem Feige.dirichletK_mem_unitInterval {ι : Type u_1} [Fintype ι] (y : ι → ℝ) : dirichletK y ∈ Set.Icc 0 1

theorem Feige.dirichletK_eq_one_of_le_one {ι : Type u_1} [Fintype ι] {y : ι → ℝ} (hy : ∀ (i : ι), y i ≤ 1) : dirichletK y = 1

If every coordinate is at most one, the event defining K is certain.

theorem Feige.kEvent_antitone {ι : Type u_1} [Fintype ι] {y z : ι → ℝ} (hyz : y ≤ z) : kEvent z ⊆ kEvent y

theorem Feige.dirichletK_antitone {ι : Type u_1} [Fintype ι] : Antitone dirichletK

K is coordinatewise nonincreasing.