Documentation

Lean 4 Proof

def shannonEntropy (p : Fin J → ℝ) : ℝ :=
  -∑ j : Fin J, p j * Real.log (p j)

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:131

Module Section

### The Thermodynamic Decomposition of Value

In the same file