Documentation

Lean 4 Proof

def qLog (q x : ℝ) : ℝ :=
  if q = 1 then Real.log x
  else (x ^ (1 - q) - 1) / (1 - q)

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:26

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file