Probability normalization for independent unit exponentials

This module supplies the product-density normalization needed to turn the normalized-exponential integral identity into a probability-law statement.

theorem Feige.integrable_unitExponentialDensity : MeasureTheory.Integrable unitExponentialDensity MeasureTheory.volume

theorem Feige.integrable_pi_unitExponentialDensity {n : ℕ} : MeasureTheory.Integrable (fun (x : Fin n → ℝ) => ∏ i : Fin n, unitExponentialDensity (x i)) MeasureTheory.volume

The product density of n independent unit exponentials is integrable on the coordinate function space.

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

Real-valued joint density on ℝ × (Fin n → ℝ).

Equations

• Feige.jointUnitExponentialDensity e = Feige.unitExponentialDensity e.1 * ∏ i : Fin n, Feige.unitExponentialDensity (e.2 i)

theorem Feige.integrable_jointUnitExponentialDensity {n : ℕ} : MeasureTheory.Integrable jointUnitExponentialDensity MeasureTheory.volume

theorem Feige.integral_jointUnitExponentialDensity {n : ℕ} : ∫ (e : ℝ × (Fin n → ℝ)), jointUnitExponentialDensity e = 1

theorem Feige.jointUnitExponentialDensity_nonneg {n : ℕ} (e : ℝ × (Fin n → ℝ)) : 0 ≤ jointUnitExponentialDensity e

theorem Feige.lintegral_ofReal_jointUnitExponentialDensity {n : ℕ} : ∫⁻ (e : ℝ × (Fin n → ℝ)), ENNReal.ofReal (jointUnitExponentialDensity e) = 1

ENNReal form of normalization of the full independent exponential product density.

theorem Feige.volume_singleton_zeroExponentialVector {n : ℕ} : MeasureTheory.volume {(0, fun (x : Fin n) => 0)} = 0

The sole point removed when passing from the closed nonnegative orthant to positiveExponentialOrthant is Lebesgue-null.

theorem Feige.nonnegative_nonzero_exponentialTotal_pos {n : ℕ} {e : ℝ × (Fin n → ℝ)} (h0 : 0 ≤ e.1) (hi : ∀ (i : Fin n), 0 ≤ e.2 i) (hne : e ≠ (0, fun (x : Fin n) => 0)) : 0 < exponentialTotal e

theorem Feige.jointUnitExponentialDensity_eq_exp_neg_total {n : ℕ} (e : ℝ × (Fin n → ℝ)) (h0 : 0 ≤ e.1) (hi : ∀ (i : Fin n), 0 ≤ e.2 i) : jointUnitExponentialDensity e = Real.exp (-exponentialTotal e)

theorem Feige.jointUnitExponentialDensity_eq_zero_of_neg {n : ℕ} (e : ℝ × (Fin n → ℝ)) (hneg : e.1 < 0 ∨ ∃ (i : Fin n), e.2 i < 0) : jointUnitExponentialDensity e = 0

theorem Feige.lintegral_positiveExponentialOrthant_exp_neg_total {n : ℕ} : ∫⁻ (e : ℝ × (Fin n → ℝ)) in positiveExponentialOrthant, ENNReal.ofReal (Real.exp (-exponentialTotal e)) = 1

theorem Feige.factorial_mul_volume_fullSimplex {n : ℕ} : ↑n.factorial * MeasureTheory.volume (fullSimplex (Fin n)) = 1

theorem Feige.volume_fullSimplex_eq_factorial_inv {n : ℕ} : MeasureTheory.volume (fullSimplex (Fin n)) = (↑n.factorial)⁻¹

Exact Lebesgue volume of the standard full simplex.

instance Feige.instIsProbabilityMeasureNormalizedExponentialSimplexMeasure {n : ℕ} : MeasureTheory.IsProbabilityMeasure normalizedExponentialSimplexMeasure