Documentation

Lean 4 Proof

theorem tsallis_shannon_limit (J : ℕ) (p : Fin J → ℝ) (_hp : OnOpenSimplex J p) :
    tsallisEntropy J 1 p = -∑ j : Fin J, p j * Real.log (p j) := by
  simp [tsallisEntropy]

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:85

Module Section

Theorem 2: Tsallis Uniqueness (Paper 2, Section 3.1)

In the same file