Documentation

Lean 4 Proof

theorem qLog_one (q : ℝ) : qLog q 1 = 0 := by
  simp only [qLog]
  split_ifs with h
  · exact Real.log_one
  · simp [rpow_def_of_pos one_pos]

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:41

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file