Log CES Eigenvalue Perp

def proved CES Potential

Documentation

Lean 4 Proof

def logCesEigenvaluePerp (J : ℕ) (ρ c : ℝ) : ℝ := -(1 - ρ) / (↑J * c ^ 2)

Dependency Graph

Used by

landscape_structure logCesEigenvaluePerp_neg eigenstructure_bridge bridge_eigenvalue convergenceRate sectorRelaxRate effectiveCurvature_taylor sector_relaxation_rate_eq logCesHessian_on_perp

Location

thesis/CESProofs/Potential/Appendix.lean:37

Module Section

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

In the same file

logCesHessianQF logCesHessian_on_perp logCesEigenvaluePerp_neg qPartitionFun qPartitionFun_pos_at_one qPartitionFun_equal_payoffs tsallisHessianDiag tsallisHessian_uniform_on_perp tsallisHessianDiag_neg