Documentation

Lean 4 Proof

def negEnergy (x : Fin J → ℝ) (j : Fin J) : ℝ := -Real.log (x j)

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:42

Module Section

### The Boltzmann-Escort Identification

In the same file