Normalized exponentials and simplex coordinates

This file begins the change of variables behind the identification of normalized independent exponentials with the uniform simplex law. We use the product model ℝ × (Fin n → ℝ): the first target coordinate is E₀, and the remaining coordinates are Eᵢ.

The forward map is

(t,x) ↦ (t(1-∑xᵢ), fun i ↦ t xᵢ),

and its inverse divides all nonzero-total vectors by their total mass.

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

Total mass of an E₀,E₁,...,Eₙ vector in product coordinates.

Equations

• Feige.exponentialTotal e = e.1 + ∑ i : Fin n, e.2 i

def Feige.exponentialSimplexForward {n : ℕ} (z : ℝ × (Fin n → ℝ)) : ℝ × (Fin n → ℝ)

Polar/simplex coordinate map used for normalized exponentials.

Equations

• Feige.exponentialSimplexForward z = (z.1 * (1 - ∑ i : Fin n, z.2 i), fun (i : Fin n) => z.1 * z.2 i)

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

Inverse normalized-coordinate map. It is used only on the domain where the total is positive.

Equations

• Feige.exponentialSimplexInverse e = (Feige.exponentialTotal e, fun (i : Fin n) => e.2 i / Feige.exponentialTotal e)

def Feige.exponentialSimplexSource {n : ℕ} : Set (ℝ × (Fin n → ℝ))

Natural source domain for the change of variables.

Equations

• Feige.exponentialSimplexSource = {z : ℝ × (Fin n → ℝ) | 0 < z.1 ∧ z.2 ∈ Feige.fullSimplex (Fin n)}

def Feige.positiveExponentialOrthant {n : ℕ} : Set (ℝ × (Fin n → ℝ))

Nonnegative exponential vectors with nonzero total mass.

Equations

• Feige.positiveExponentialOrthant = {e : ℝ × (Fin n → ℝ) | 0 ≤ e.1 ∧ (∀ (i : Fin n), 0 ≤ e.2 i) ∧ 0 < Feige.exponentialTotal e}

theorem Feige.continuous_exponentialTotal {n : ℕ} : Continuous exponentialTotal

theorem Feige.continuous_exponentialSimplexForward {n : ℕ} : Continuous exponentialSimplexForward

theorem Feige.measurable_exponentialSimplexForward {n : ℕ} : Measurable exponentialSimplexForward

theorem Feige.measurable_exponentialSimplexInverse {n : ℕ} : Measurable exponentialSimplexInverse

theorem Feige.isMeasurableSet_exponentialSimplexSource {n : ℕ} : MeasurableSet exponentialSimplexSource

theorem Feige.isMeasurableSet_positiveExponentialOrthant {n : ℕ} : MeasurableSet positiveExponentialOrthant

theorem Feige.exponentialTotal_forward {n : ℕ} (z : ℝ × (Fin n → ℝ)) : exponentialTotal (exponentialSimplexForward z) = z.1

theorem Feige.exponentialSimplexForward_mem {n : ℕ} {z : ℝ × (Fin n → ℝ)} (hz : z ∈ exponentialSimplexSource) : exponentialSimplexForward z ∈ positiveExponentialOrthant

theorem Feige.exponentialSimplexInverse_mem {n : ℕ} {e : ℝ × (Fin n → ℝ)} (he : e ∈ positiveExponentialOrthant) : exponentialSimplexInverse e ∈ exponentialSimplexSource

theorem Feige.exponentialSimplexInverse_forward {n : ℕ} {z : ℝ × (Fin n → ℝ)} (hz : z ∈ exponentialSimplexSource) : exponentialSimplexInverse (exponentialSimplexForward z) = z

theorem Feige.exponentialSimplexForward_inverse {n : ℕ} {e : ℝ × (Fin n → ℝ)} (he : e ∈ positiveExponentialOrthant) : exponentialSimplexForward (exponentialSimplexInverse e) = e

theorem Feige.exponentialSimplex_bijOn {n : ℕ} : Set.BijOn exponentialSimplexForward exponentialSimplexSource positiveExponentialOrthant

The coordinate change is a bijection between its natural source and target domains.

Fréchet derivative of the coordinate change

noncomputable def Feige.simplexCoordinateSumDerivative {n : ℕ} : ℝ × (Fin n → ℝ) →L[ℝ] ℝ

Differential of the total simplex-coordinate sum.

Equations

• Feige.simplexCoordinateSumDerivative = ∑ i : Fin n, ContinuousLinearMap.proj i ∘SL ContinuousLinearMap.snd ℝ ℝ (Fin n → ℝ)

noncomputable def Feige.exponentialSimplexForwardDerivative {n : ℕ} (z : ℝ × (Fin n → ℝ)) : ℝ × (Fin n → ℝ) →L[ℝ] ℝ × (Fin n → ℝ)

The explicit Fréchet derivative of exponentialSimplexForward.

Applied to an increment (dt,dx), it is

(dt(1-∑x)-t∑dx, fun i ↦ dt*xᵢ+t*dxᵢ).

Equations

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

@[simp]

theorem Feige.simplexCoordinateSumDerivative_apply {n : ℕ} (h : ℝ × (Fin n → ℝ)) : simplexCoordinateSumDerivative h = ∑ i : Fin n, h.2 i

theorem Feige.exponentialSimplexForwardDerivative_apply {n : ℕ} (z h : ℝ × (Fin n → ℝ)) : (exponentialSimplexForwardDerivative z) h = (h.1 * (1 - ∑ i : Fin n, z.2 i) - z.1 * ∑ i : Fin n, h.2 i, fun (i : Fin n) => h.1 * z.2 i + z.1 * h.2 i)

theorem Feige.hasFDerivAt_exponentialSimplexForward {n : ℕ} (z : ℝ × (Fin n → ℝ)) : HasFDerivAt exponentialSimplexForward (exponentialSimplexForwardDerivative z) z

theorem Feige.fderiv_exponentialSimplexForward {n : ℕ} (z : ℝ × (Fin n → ℝ)) : fderiv ℝ exponentialSimplexForward z = exponentialSimplexForwardDerivative z

Matrix of the derivative

def Feige.optionVectorToProduct {n : ℕ} (v : Option (Fin n) → ℝ) : ℝ × (Fin n → ℝ)

Identify an Option (Fin n) coordinate vector with radial/product coordinates.

Equations

• Feige.optionVectorToProduct v = (v none, fun (i : Fin n) => v (some i))

theorem Feige.measurable_optionVectorToProduct {n : ℕ} : Measurable optionVectorToProduct

The optional-coordinate identification is measurable.

def Feige.productToOptionVector {n : ℕ} (z : ℝ × (Fin n → ℝ)) : Option (Fin n) → ℝ

The inverse coordinate identification.

Equations

• Feige.productToOptionVector z none = z.1
• Feige.productToOptionVector z (some i) = z.2 i

@[simp]

theorem Feige.productToOptionVector_optionVectorToProduct {n : ℕ} (v : Option (Fin n) → ℝ) : productToOptionVector (optionVectorToProduct v) = v

@[simp]

theorem Feige.optionVectorToProduct_productToOptionVector {n : ℕ} (z : ℝ × (Fin n → ℝ)) : optionVectorToProduct (productToOptionVector z) = z

noncomputable def Feige.exponentialSimplexJacobianMatrix {n : ℕ} (z : ℝ × (Fin n → ℝ)) : Matrix (Option (Fin n)) (Option (Fin n)) ℝ

Jacobian matrix of exponentialSimplexForward in the basis indexed by none, some 0, ..., some (n-1).

Equations

• Feige.exponentialSimplexJacobianMatrix z none none = 1 - ∑ i : Fin n, z.2 i
• Feige.exponentialSimplexJacobianMatrix z none (some val) = -z.1
• Feige.exponentialSimplexJacobianMatrix z (some i) none = z.2 i
• Feige.exponentialSimplexJacobianMatrix z (some i) (some j) = if i = j then z.1 else 0

@[simp]

theorem Feige.exponentialSimplexJacobianMatrix_none_none {n : ℕ} (z : ℝ × (Fin n → ℝ)) : exponentialSimplexJacobianMatrix z none none = 1 - ∑ i : Fin n, z.2 i

@[simp]

theorem Feige.exponentialSimplexJacobianMatrix_none_some {n : ℕ} (z : ℝ × (Fin n → ℝ)) (j : Fin n) : exponentialSimplexJacobianMatrix z none (some j) = -z.1

@[simp]

theorem Feige.exponentialSimplexJacobianMatrix_some_none {n : ℕ} (z : ℝ × (Fin n → ℝ)) (i : Fin n) : exponentialSimplexJacobianMatrix z (some i) none = z.2 i

@[simp]

theorem Feige.exponentialSimplexJacobianMatrix_some_some {n : ℕ} (z : ℝ × (Fin n → ℝ)) (i j : Fin n) : exponentialSimplexJacobianMatrix z (some i) (some j) = if i = j then z.1 else 0

theorem Feige.exponentialSimplexJacobianMatrix_mulVec_none {n : ℕ} (z : ℝ × (Fin n → ℝ)) (v : Option (Fin n) → ℝ) : (exponentialSimplexJacobianMatrix z).mulVec v none = v none * (1 - ∑ i : Fin n, z.2 i) - z.1 * ∑ i : Fin n, v (some i)

theorem Feige.exponentialSimplexJacobianMatrix_mulVec_some {n : ℕ} (z : ℝ × (Fin n → ℝ)) (v : Option (Fin n) → ℝ) (i : Fin n) : (exponentialSimplexJacobianMatrix z).mulVec v (some i) = v none * z.2 i + z.1 * v (some i)

theorem Feige.productToOptionVector_derivative_eq_mulVec {n : ℕ} (z : ℝ × (Fin n → ℝ)) (v : Option (Fin n) → ℝ) : productToOptionVector ((exponentialSimplexForwardDerivative z) (optionVectorToProduct v)) = (exponentialSimplexJacobianMatrix z).mulVec v

The explicit Jacobian matrix represents the Fréchet derivative proved above.

Determinant of the Jacobian

noncomputable def Feige.reducedExponentialSimplexJacobianMatrix {n : ℕ} (z : ℝ × (Fin n → ℝ)) : Matrix (Option (Fin n)) (Option (Fin n)) ℝ

Add all rows of the Jacobian to its none row. This elementary row operation leaves the determinant unchanged and makes the matrix triangular.

Equations

• Feige.reducedExponentialSimplexJacobianMatrix z = (Feige.exponentialSimplexJacobianMatrix z).updateRow none (∑ k : Option (Fin n), 1 • Feige.exponentialSimplexJacobianMatrix z k)

theorem Feige.det_reducedExponentialSimplexJacobianMatrix {n : ℕ} (z : ℝ × (Fin n → ℝ)) : (reducedExponentialSimplexJacobianMatrix z).det = (exponentialSimplexJacobianMatrix z).det

@[simp]

theorem Feige.reducedExponentialSimplexJacobianMatrix_none_none {n : ℕ} (z : ℝ × (Fin n → ℝ)) : reducedExponentialSimplexJacobianMatrix z none none = 1

@[simp]

theorem Feige.reducedExponentialSimplexJacobianMatrix_none_some {n : ℕ} (z : ℝ × (Fin n → ℝ)) (j : Fin n) : reducedExponentialSimplexJacobianMatrix z none (some j) = 0

@[simp]

theorem Feige.reducedExponentialSimplexJacobianMatrix_some_none {n : ℕ} (z : ℝ × (Fin n → ℝ)) (i : Fin n) : reducedExponentialSimplexJacobianMatrix z (some i) none = z.2 i

@[simp]

theorem Feige.reducedExponentialSimplexJacobianMatrix_some_some {n : ℕ} (z : ℝ × (Fin n → ℝ)) (i j : Fin n) : reducedExponentialSimplexJacobianMatrix z (some i) (some j) = if i = j then z.1 else 0

theorem Feige.det_reducedExponentialSimplexJacobianMatrix_eq_pow {n : ℕ} (z : ℝ × (Fin n → ℝ)) : (reducedExponentialSimplexJacobianMatrix z).det = z.1 ^ n

theorem Feige.det_exponentialSimplexJacobianMatrix {n : ℕ} (z : ℝ × (Fin n → ℝ)) : (exponentialSimplexJacobianMatrix z).det = z.1 ^ n

The Jacobian determinant of the radial--simplex coordinate map is t ^ n.

Change of variables

noncomputable def Feige.exponentialCoordinateBasis {n : ℕ} : Module.Basis (Option (Fin n)) ℝ (ℝ × (Fin n → ℝ))

The coordinate basis whose none coordinate is the radial coordinate and whose some i coordinates are the simplex coordinates.

Equations

• Feige.exponentialCoordinateBasis = (Pi.basisFun ℝ (Option (Fin n))).map (LinearEquiv.piOptionEquivProd ℝ)

theorem Feige.det_exponentialSimplexForwardDerivative {n : ℕ} (z : ℝ × (Fin n → ℝ)) : (exponentialSimplexForwardDerivative z).det = z.1 ^ n

The determinant of the Fréchet derivative, in the intrinsic finite-dimensional determinant used by Mathlib's change-of-variables theorem.

theorem Feige.exponentialCoordinateBasis_addHaar_eq_volume {n : ℕ} : exponentialCoordinateBasis.addHaar = MeasureTheory.volume

The coordinate Haar measure is exactly the default product Lebesgue measure, not merely a nonzero scalar multiple of it.

theorem Feige.lintegral_positiveExponentialOrthant_eq {n : ℕ} (g : ℝ × (Fin n → ℝ) → ENNReal) : ∫⁻ (e : ℝ × (Fin n → ℝ)) in positiveExponentialOrthant, g e = ∫⁻ (z : ℝ × (Fin n → ℝ)) in exponentialSimplexSource, ENNReal.ofReal (z.1 ^ n) * g (exponentialSimplexForward z)

Restricted change of variables from radial--simplex coordinates to the positive exponential orthant. This is the nonnegative integral formula directly supplied by Mathlib's finite-dimensional Jacobian theorem, with all geometric and differentiability hypotheses discharged here.

The radial Gamma integral

theorem Feige.integral_exp_neg_mul_pow_Ioi (n : ℕ) : ∫ (t : ℝ) in Set.Ioi 0, Real.exp (-t) * t ^ n = ↑n.factorial

The elementary radial integral appearing after the normalized exponential change of variables.

theorem Feige.lintegral_ofReal_exp_neg_mul_pow_Ioi (n : ℕ) : ∫⁻ (t : ℝ) in Set.Ioi 0, ENNReal.ofReal (Real.exp (-t) * t ^ n) = ↑n.factorial

ENNReal/Tonelli form of the radial Gamma integral.

Normalized exponential coordinates

theorem Feige.exponentialSimplexSource_eq_prod {n : ℕ} : exponentialSimplexSource = Set.Ioi 0 ×ˢ fullSimplex (Fin n)

theorem Feige.lintegral_exponentialRadial_mul_test {n : ℕ} (h : (Fin n → ℝ) → ENNReal) (hh : Measurable h) : ∫⁻ (z : ℝ × (Fin n → ℝ)) in exponentialSimplexSource, ENNReal.ofReal (Real.exp (-z.1) * z.1 ^ n) * h z.2 = ↑n.factorial * ∫⁻ (x : Fin n → ℝ) in fullSimplex (Fin n), h x

Tonelli separation of the radial factor from an arbitrary measurable nonnegative test function on the simplex.

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

The measure on simplex coordinates obtained from independent unit-rate exponentials: factorial times Lebesgue measure restricted to the full simplex.

Equations

• Feige.normalizedExponentialSimplexMeasure = ↑n.factorial • MeasureTheory.volume.restrict (Feige.fullSimplex (Fin n))

theorem Feige.lintegral_normalizedExponential_eq_simplex {n : ℕ} (h : (Fin n → ℝ) → ENNReal) (hh : Measurable h) : ∫⁻ (e : ℝ × (Fin n → ℝ)) in positiveExponentialOrthant, ENNReal.ofReal (Real.exp (-exponentialTotal e)) * h (exponentialSimplexInverse e).2 = ∫⁻ (x : Fin n → ℝ), h x ∂normalizedExponentialSimplexMeasure

Identification of normalized independent exponentials with the factorial-density uniform simplex measure, formulated against arbitrary measurable nonnegative test functions.

noncomputable def Feige.unitExponentialDensity (t : ℝ) : ℝ

The unit-rate exponential density, extended by zero to the negative half-line.

Equations

• Feige.unitExponentialDensity t = (Set.Ici 0).indicator (fun (t : ℝ) => Real.exp (-t)) t

theorem Feige.integral_unitExponentialDensity : ∫ (t : ℝ), unitExponentialDensity t = 1

theorem Feige.integral_pi_unitExponentialDensity {n : ℕ} : ∫ (x : Fin n → ℝ), ∏ i : Fin n, unitExponentialDensity (x i) = 1

A finite product of unit exponential densities has total mass one.