Documentation

Lean 4 Proof

theorem cesPotential_eq_effectiveCESPotential (q T : ℝ) (p ε : Fin J → ℝ) :
    cesPotential J q T p ε = effectiveCESPotential J q T p ε := by
  simp only [cesPotential, effectiveCESPotential, tsallisEntropy]

Dependency Graph

Location

thesis/CESProofs/Potential/CESPotential.lean:116

Module Section

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

In the same file