Documentation

Lean 4 Proof

theorem qLog_eq_of_ne {q : ℝ} (hq : q ≠ 1) (x : ℝ) :
    qLog q x = (x ^ (1 - q) - 1) / (1 - q) := by
  simp [qLog, hq]

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:55

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file