Documentation

Lean 4 Proof

theorem tail_exponential_at_q_one (J : ℕ) (T : ℝ) (p : Fin J → ℝ) (ε : Fin J → ℝ) :
    -- At q = 1, the Tsallis entropy S_q reduces to Shannon entropy -Σ p log p.
    -- The entropy-maximizing allocation is logit/softmax, giving exponential tails.
    -- This is the boundary between power-law (q > 1) and compact support (q < 1).
    effectiveCESPotential J 1 T p ε =
    ∑ j : Fin J, p j * ε j - T * (-∑ j : Fin J, p j * Real.log (p j)) := by
  unfold effectiveCESPotential
  simp

Dependency Graph

Location

thesis/CESProofs/Foundations/AggregationInvariantClass.lean:117

Module Section

Aggregation-invariant class results from Paper 1, Section 5:

In the same file