Documentation

Lean 4 Proof

theorem qExpAllocation_at_one (T : ℝ) (ε : Fin J → ℝ) :
    qExpAllocation J 1 T ε = fun j =>
    Real.exp (ε j / T) / ∑ k : Fin J, Real.exp (ε k / T) := by
  simp [qExpAllocation, qExp]

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/QEquilibrium.lean:56

Module Section

Propositions 3-4: q-Exponential Equilibrium and Tail Behavior

In the same file