Documentation

Lean 4 Proof

theorem boltzmann_eq_rpow {x : Fin J → ℝ} (hx : ∀ j, 0 < x j)
    (ρ : ℝ) (j : Fin J) :
    Real.exp (-ρ * negEnergy x j) = x j ^ ρ := by
  unfold negEnergy
  rw [show -ρ * -Real.log (x j) = Real.log (x j) * ρ from by ring]
  exact (rpow_def_of_pos (hx j) ρ).symm

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:48

Module Section

### The Boltzmann-Escort Identification

In the same file