Q Partition Function

def proved CES Potential

Documentation

Lean 4 Proof

def qPartitionFun (J : ℕ) (q T : ℝ) (ε : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, qExp q (ε j / T)

Dependency Graph

Used by

qPartitionFun_equal_payoffs qPartitionFun_pos_at_one

Location

thesis/CESProofs/Potential/Appendix.lean:71

Module Section

Appendix Lemmas 1-3 (Paper 2, Appendix A)

In the same file

logCesHessianQF logCesEigenvaluePerp logCesHessian_on_perp logCesEigenvaluePerp_neg qPartitionFun_pos_at_one qPartitionFun_equal_payoffs tsallisHessianDiag tsallisHessian_uniform_on_perp tsallisHessianDiag_neg