noncomputable def log_sum_exp_function {n : ℕ} : (Fin n → ℝ) → EReal

The log-sum-exp function x ↦ log (∑ j, exp (x_j)) on ℝ^n, regarded as an EReal-valued function so that its Fenchel conjugate is expressed by conjugate_function.

@[simp]

theorem log_sum_exp_function_apply {n : ℕ} (x : Fin n → ℝ) : log_sum_exp_function x = ↑(Real.log (∑ j : Fin n, Real.exp (x j)))

Evaluating log_sum_exp_function at x gives log (∑ j, exp (x_j)), viewed in EReal.

theorem log_sum_exp_function_conjugate {n : ℕ} [NeZero n] : (fun (y : Fin n → ℝ) => conjugate_function log_sum_exp_function ((dotProductEquiv ℝ (Fin n)) y)) = negative_entropy_on_stdSimplex n

Proposition 4.17: the Fenchel conjugate of the log-sum-exp function on ℝ^n, evaluated via the Euclidean pairing dotProductEquiv, is the simplex-constrained negative entropy negative_entropy_on_stdSimplex n. Equivalently, this is the entropy expression ∑ i, y_i log y_i on the standard simplex Δ_n = stdSimplex ℝ (Fin n) and ∞ outside the simplex.

theorem log_sum_exp_function_conjugate_eq {n : ℕ} [NeZero n] (y : Fin n → ℝ) : conjugate_function log_sum_exp_function ((dotProductEquiv ℝ (Fin n)) y) = negative_entropy_on_stdSimplex n y

Pointwise form of Proposition 4.17.

@[simp]

theorem log_sum_exp_function_conjugate_of_mem {n : ℕ} [NeZero n] {y : Fin n → ℝ} (hy : y ∈ stdSimplex ℝ (Fin n)) : conjugate_function log_sum_exp_function ((dotProductEquiv ℝ (Fin n)) y) = ↑(∑ i : Fin n, y i * Real.log (y i))

On stdSimplex ℝ (Fin n), the conjugate of log_sum_exp_function is the entropy sum ∑ i, y i * log (y i).

@[simp]

theorem log_sum_exp_function_conjugate_of_not_mem {n : ℕ} [NeZero n] {y : Fin n → ℝ} (hy : y ∉ stdSimplex ℝ (Fin n)) : conjugate_function log_sum_exp_function ((dotProductEquiv ℝ (Fin n)) y) = ⊤

Outside stdSimplex ℝ (Fin n), the conjugate of log_sum_exp_function is ∞.