Uniform simplex law from normalized exponentials

This module identifies the factorial-density simplex measure obtained by the normalized-exponential calculation with the project's existing uniform simplex probability measure.

theorem Feige.normalizedExponentialSimplexMeasure_eq_uniform {n : ℕ} : normalizedExponentialSimplexMeasure = simplexUniformMeasure (Fin n)

noncomputable def Feige.normalizedExponentialCoordinates {n : ℕ} (e : ℝ × (Fin n → ℝ)) : Fin n → ℝ

The normalized-coordinate map on real product coordinates.

Equations

• Feige.normalizedExponentialCoordinates e = (Feige.exponentialSimplexInverse e).2

noncomputable def Feige.realExponentialProductMeasure {n : ℕ} : MeasureTheory.Measure (ℝ × (Fin n → ℝ))

Independent unit exponentials on the positive real orthant, written as an absolutely continuous measure in real product coordinates.

Equations

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

theorem Feige.realExponentialProductMeasure_lintegral {n : ℕ} (h : (Fin n → ℝ) → ENNReal) (hh : Measurable h) : ∫⁻ (e : ℝ × (Fin n → ℝ)), h (normalizedExponentialCoordinates e) ∂realExponentialProductMeasure = ∫⁻ (x : Fin n → ℝ), h x ∂simplexUniformMeasure (Fin n)

theorem Feige.measurable_normalizedExponentialCoordinates {n : ℕ} : Measurable normalizedExponentialCoordinates

theorem Feige.map_realExponentialProductMeasure_normalizedCoordinates {n : ℕ} : MeasureTheory.Measure.map normalizedExponentialCoordinates realExponentialProductMeasure = simplexUniformMeasure (Fin n)

Measure-level pushforward form of the normalized exponential law.