Documentation

Lean 4 Proof

theorem qExp_eq_of_ne {q : ℝ} (hq : q ≠ 1) (x : ℝ) :
    qExp q x = (max 0 (1 + (1 - q) * x)) ^ (1 / (1 - q)) := by
  simp [qExp, hq]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/Defs.lean:60

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file