Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Potential/QEquilibrium.lean:129

Module Section

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

In the same file