Documentation

Lean 4 Proof

def qExp (q x : ℝ) : ℝ :=
  if q = 1 then Real.exp x
  else (max 0 (1 + (1 - q) * x)) ^ (1 / (1 - q))

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:32

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file