Documentation

Lean 4 Proof

def efficiencyTerm (x : Fin J → ℝ) (ρ : ℝ) : ℝ :=
  escortExpectation x ρ (fun j => Real.log (x j))

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:141

Module Section

### The Thermodynamic Decomposition of Value

In the same file