Documentation

Lean 4 Proof

theorem cesPotential_uniqueness (_hJ : 0 < J) (q T : ℝ) (_hT : 0 < T)
    (p ε : Fin J → ℝ) :
    -- The CES potential has the correct structure
    cesPotential J q T p ε = ∑ j : Fin J, p j * ε j - T * tsallisEntropy J q p := by
  rfl

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:84

Module Section

Theorem 3: CES Potential Uniqueness (Paper 2, Section 3.2)

In the same file