Documentation

Lean 4 Proof

theorem tsallisEntropy_uniform (hJ : 0 < J) (q : ℝ) :
    tsallisEntropy J q (fun _ => (1 : ℝ) / ↑J) =
    if q = 1 then Real.log ↑J
    else (1 - (↑J : ℝ) ^ (1 - q)) / (q - 1) := by
  simp only [tsallisEntropy]
  have hJpos : (0 : ℝ) < ↑J := Nat.cast_pos.mpr hJ
  have hJne : (↑J : ℝ) ≠ 0 := ne_of_gt hJpos
  split_ifs with h
  · -- q = 1 case: -J · (1/J · log(1/J)) = log J
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    rw [Real.log_div one_ne_zero hJne, Real.log_one, zero_sub]
    field_simp
  · -- q ≠ 1 case: (1 - J · (1/J)^q) / (q-1) = (1 - J^{1-q}) / (q-1)
    congr 1; congr 1
    rw [Finset.sum_const, Finset.card_univ, Fintype.card_fin, nsmul_eq_mul]
    rw [one_div, inv_rpow (le_of_lt hJpos)]
    -- Goal: J * (J^q)⁻¹ = J^(1-q)
    rw [← rpow_neg (le_of_lt hJpos)]
    rw [show (1 : ℝ) - q = 1 + (-q) from by ring]
    rw [rpow_add hJpos, rpow_one]

Dependency Graph

Location

thesis/CESProofs/Potential/Defs.lean:87

Module Section

Core definitions for the Lean formalization of Paper 2:

In the same file