Documentation

Lean 4 Proof

theorem cesPotential_uniform_equal (hJ : 0 < J) (q T ε₀ : ℝ) :
    cesPotential J q T (fun _ => (1 : ℝ) / ↑J) (fun _ => ε₀) =
    ε₀ - T * tsallisEntropy J q (fun _ => (1 : ℝ) / ↑J) := by
  simp only [cesPotential]
  congr 1
  rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:222

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file