Documentation

Lean 4 Proof

theorem qLogSumExp_at_one (T : ℝ) (ε : Fin J → ℝ) :
    qLogSumExp J 1 T ε = T * Real.log (∑ j : Fin J, Real.exp (ε j / T)) := by
  simp [qLogSumExp, qLog, qExp]

Dependency Graph

Location

thesis/CESProofs/Potential/QDynamics.lean:174

Module Section

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

In the same file