Q Exp Allocation

def proved CES Potential

Documentation

Lean 4 Proof

def qExpAllocation (J : ℕ) (q T : ℝ) (ε : Fin J → ℝ) : Fin J → ℝ :=
  let Z := ∑ j : Fin J, qExp q (ε j / T)
  fun j => qExp q (ε j / T) / Z

Dependency Graph

Used by

qExpAllocation_at_one ten_views_one_object qExpAllocation_is_shareFunction logit_recovery qExp_logit_identity

Location

thesis/CESProofs/Potential/QEquilibrium.lean:30

Module Section

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

In the same file

qExp_is_optimizer qExpAllocation_at_one compact_support_q_lt_one pareto_exponent_pos pareto_exponent_decreasing logit_recovery