Documentation

Lean 4 Proof

def qLogSumExp (J : ℕ) (q T : ℝ) (ε : Fin J → ℝ) : ℝ :=
  T * qLog q (∑ j : Fin J, qExp q (ε j / T))

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/QDynamics.lean:170

Module Section

Theorems 5-7, Corollaries 2-4, Propositions 8-11:

In the same file