Documentation

Lean 4 Proof

theorem qSum_at_one (a b : ℝ) : qSum 1 a b = a + b := by
  simp [qSum]

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:94

Module Section

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

In the same file