Documentation

Lean 4 Proof

theorem gibbsProb_is_shareFunction (ε x : Fin J → ℝ)
    (T h : ℝ) (j : Fin J) :
    gibbsProb ε x T h j =
    shareFunction (fun k => gibbsWeight ε x T h k) j := by
  simp only [gibbsProb, gibbsZ, shareFunction]

Dependency Graph

Location

thesis/CESProofs/Foundations/TenWayIdentity.lean:200

Module Section

Ten Views of a Single Object:

In the same file