Documentation

Lean 4 Proof

def escortEntropy (x : Fin J → ℝ) (ρ : ℝ) : ℝ :=
  shannonEntropy (escortProbability x ρ)

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:136

Module Section

### The Thermodynamic Decomposition of Value

In the same file