Event bridge for the exponential and simplex statistics

This file records the deterministic normalization identity between the simplex statistic in (2.1) and the internal exponential representation, in the NNReal coordinate model used by expProductMeasure.

theorem Feige.expMeasure_one_eq_withDensity_unitExponentialDensity : ProbabilityTheory.expMeasure 1 = MeasureTheory.volume.withDensity fun (x : ℝ) => ENNReal.ofReal (unitExponentialDensity x)

theorem Feige.prod_withDensity_eq_volume_withDensity {α : Type u_1} {β : Type u_2} [MeasureTheory.MeasureSpace α] [MeasureTheory.MeasureSpace β] [MeasureTheory.SFinite MeasureTheory.volume] {f : α → ENNReal} {g : β → ENNReal} (hf : Measurable f) (hg : Measurable g) : (MeasureTheory.volume.withDensity f).prod (MeasureTheory.volume.withDensity g) = (MeasureTheory.volume.prod MeasureTheory.volume).withDensity fun (z : α × β) => f z.1 * g z.2

Binary density-product bridge used in the finite-dimensional induction.

theorem Feige.MeasurePreserving.map_withDensity_equiv {α : Type u_1} {β : Type u_2} [MeasurableSpace α] [MeasurableSpace β] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} (T : α ≃ᵐ β) (hT : MeasureTheory.MeasurePreserving (⇑T) μ ν) {f : β → ENNReal} (hf : Measurable f) : MeasureTheory.Measure.map (⇑T) (μ.withDensity (f ∘ ⇑T)) = ν.withDensity f

Transporting a density through a measure-preserving measurable equivalence transports the underlying measure and composes the density with the equivalence.

theorem Feige.expMeasure_prod_withDensity {β : Type u_1} [MeasureTheory.MeasureSpace β] [MeasureTheory.SFinite MeasureTheory.volume] {g : β → ENNReal} (hg : Measurable g) : (ProbabilityTheory.expMeasure 1).prod (MeasureTheory.volume.withDensity g) = (MeasureTheory.volume.prod MeasureTheory.volume).withDensity fun (z : ℝ × β) => ENNReal.ofReal (unitExponentialDensity z.1) * g z.2

One induction step: adjoining an independent unit exponential to a finite-dimensional density multiplies the joint density.

noncomputable def Feige.finExponentialDensity (n : ℕ) : (Fin n → ℝ) → ENNReal

The joint unit-exponential density on Fin n → ℝ.

Equations

• Feige.finExponentialDensity n x = ∏ i : Fin n, ENNReal.ofReal (Feige.unitExponentialDensity (x i))

theorem Feige.measurable_finExponentialDensity (n : ℕ) : Measurable (finExponentialDensity n)

theorem Feige.pi_expMeasure_eq_withDensity (n : ℕ) : (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.expMeasure 1) = MeasureTheory.volume.withDensity (finExponentialDensity n)

The finite product of unit exponential laws has the product of the one-dimensional exponential densities with respect to Lebesgue volume.

theorem Feige.productExponentialDensity_eq_ofReal_joint {n : ℕ} (e : ℝ × (Fin n → ℝ)) : ENNReal.ofReal (unitExponentialDensity e.1) * finExponentialDensity n e.2 = ENNReal.ofReal (jointUnitExponentialDensity e)

theorem Feige.expMeasure_prod_pi_eq_realExponentialProductMeasure {n : ℕ} : (ProbabilityTheory.expMeasure 1).prod (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.expMeasure 1) = realExponentialProductMeasure

def Feige.nnrealOptionToRealOption {n : ℕ} (e : Option (Fin n) → NNReal) : Option (Fin n) → ℝ

Coerce every coordinate of an NNReal vector to a real number.

Equations

• Feige.nnrealOptionToRealOption e i = ↑(e i)

theorem Feige.measurable_nnrealOptionToRealOption {n : ℕ} : Measurable nnrealOptionToRealOption

theorem Feige.map_expProductMeasure_to_realOption {n : ℕ} : MeasureTheory.Measure.map nnrealOptionToRealOption (expProductMeasure (Fin n)) = MeasureTheory.Measure.pi fun (x : Option (Fin n)) => ProbabilityTheory.expMeasure 1

theorem Feige.map_realOptionProductMeasure {n : ℕ} : MeasureTheory.Measure.map optionVectorToProduct (MeasureTheory.Measure.pi fun (x : Option (Fin n)) => ProbabilityTheory.expMeasure 1) = (ProbabilityTheory.expMeasure 1).prod (MeasureTheory.Measure.pi fun (x : Fin n) => ProbabilityTheory.expMeasure 1)

theorem Feige.map_expProductMeasure_to_realProduct {n : ℕ} : MeasureTheory.Measure.map (optionVectorToProduct ∘ nnrealOptionToRealOption) (expProductMeasure (Fin n)) = realExponentialProductMeasure

def Feige.nnrealExponentialTotal {n : ℕ} (e : Option (Fin n) → NNReal) : ℝ

The total mass of an optional-indexed nonnegative vector.

Equations

• Feige.nnrealExponentialTotal e = ↑(e none) + ∑ i : Fin n, ↑(e (some i))

noncomputable def Feige.nnrealNormalizedCoordinates {n : ℕ} (e : Option (Fin n) → NNReal) : Fin n → ℝ

Normalize the finite coordinates by the total exponential mass.

Equations

• Feige.nnrealNormalizedCoordinates e i = ↑(e (some i)) / Feige.nnrealExponentialTotal e

theorem Feige.measurable_nnrealExponentialTotal {n : ℕ} : Measurable nnrealExponentialTotal

theorem Feige.measurable_nnrealNormalizedCoordinates {n : ℕ} : Measurable nnrealNormalizedCoordinates

theorem Feige.nnrealNormalizedCoordinates_mem_fullSimplex {n : ℕ} {e : Option (Fin n) → NNReal} (ht : 0 < nnrealExponentialTotal e) : nnrealNormalizedCoordinates e ∈ fullSimplex (Fin n)

theorem Feige.mem_kEvent_iff_normalized_simplex_event {n : ℕ} (y : Fin n → ℝ) {e : Option (Fin n) → NNReal} (ht : 0 < nnrealExponentialTotal e) : e ∈ kEvent y ↔ simplexLinearForm y (nnrealNormalizedCoordinates e) ≤ 1

On every nonzero exponential vector, the event defining dirichletK is exactly the simplex halfspace event after normalization.

theorem Feige.normalizedCoordinates_realProduct_comp {n : ℕ} (e : Option (Fin n) → NNReal) : normalizedExponentialCoordinates (optionVectorToProduct (nnrealOptionToRealOption e)) = nnrealNormalizedCoordinates e

theorem Feige.mem_kEvent_iff_normalized_simplex_event' {n : ℕ} (y : Fin n → ℝ) (e : Option (Fin n) → NNReal) : e ∈ kEvent y ↔ simplexLinearForm y (nnrealNormalizedCoordinates e) ≤ 1

theorem Feige.map_expProductMeasure_normalizedCoordinates {n : ℕ} : MeasureTheory.Measure.map nnrealNormalizedCoordinates (expProductMeasure (Fin n)) = simplexUniformMeasure (Fin n)

theorem Feige.simplexExponentialIdentification (n : ℕ) : SimplexExponentialIdentification n