Documentation

Lean 4 Proof

def qSum (q a b : ℝ) : ℝ := a + b + (1 - q) * a * b

Dependency Graph

Location

thesis/CESProofs/Potential/TsallisUniqueness.lean:91

Module Section

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

In the same file