Documentation

Lean 4 Proof

theorem boltzmann_eq_escort [NeZero J] {x : Fin J → ℝ}
    (hx : ∀ j, 0 < x j) (ρ : ℝ) (j : Fin J) :
    Real.exp (-ρ * negEnergy x j) /
      ∑ k : Fin J, Real.exp (-ρ * negEnergy x k) =
    escortProbability x ρ j := by
  unfold escortProbability escortPartitionZ
  congr 1
  · exact boltzmann_eq_rpow hx ρ j
  · exact Finset.sum_congr rfl (fun k _ => boltzmann_eq_rpow hx ρ k)

Dependency Graph

Location

thesis/CESProofs/Foundations/TripleCorrespondence.lean:65

Module Section

### The Boltzmann-Escort Identification

In the same file