Documentation

Lean 4 Proof

theorem free_energy_decomposition [NeZero J] {ρ : ℝ} (hρ : ρ ≠ 0)
    (x : Fin J → ℝ) (hx : ∀ j, 0 < x j) :
    ρ * Real.log (powerMean J ρ hρ x) =
    ρ * efficiencyTerm x ρ + escortEntropy x ρ - Real.log ↑J := by
  rw [logCES_eq_logPartition hρ x hx, logZ_eq_rho_eff_plus_entropy x hx ρ]

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:219

Module Section

### The Thermodynamic Decomposition of Value

In the same file