Documentation

Lean 4 Proof

theorem qSum_assoc (q a b c : ℝ) :
    qSum q (qSum q a b) c = qSum q a (qSum q b c) := by
  simp [qSum]; ring

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:102

Module Section

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

In the same file