Documentation

Lean 4 Proof

def specificHeat (x : Fin J → ℝ) (ρ : ℝ) : ℝ :=
  ρ ^ 2 * escortVariance x ρ (fun j => Real.log (x j))

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:148

Module Section

### The Thermodynamic Decomposition of Value

In the same file