Sections / Section 5: General Hessian and Isoquant Geometry / cesEigenvaluePerp

CES Eigenvalue Perp

defprovedFoundations

Documentation

Lean 4 Proof

def cesEigenvaluePerp (J : ℕ) (ρ c : ℝ) : ℝ := -(1 - ρ) / (↑J * c)

Dependency Graph

Used by

ces_strict_concavity_on_perp curvature_eq_neg_eigenvalue_sqrt strategic_bound cesEigenvaluePerp_neg cesCriticalStep_eq saddle_point_substitutes curvature_conservation cesHessianQF_neg_semidef diversity_encoding ces_period_two_at_critical cesHessianQF_on_perp cesEigenvaluePerp_sq hessianQF_eq_negK_norm SextupleRoleStatement hessLogF_from_cesEigenvalue eos_at_boundary ces_stable_iff weighted_conservation_at_equal_weights eigenvalue_perp_pos_substitute cesCriticalStep curvature_conservation_as_holder_complement eigenvaluePerp_sq_proportional_to_K_sq cesEigenvaluePerp_abs_pos logCesHessian_on_perp

Location

thesis/CESProofs/Foundations/Hessian.lean:37

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

cesHessianQF vecSum orthToOne vecNormSq ces_gradient_symmetric cesHessianQF_on_one cesHessianQF_on_perp cesHessianQF_neg_semidef ces_strict_concavity_on_perp cesHessianEntry cesHessianQF_eq_sum cesPrincipalCurvature curvature_lemma curvature_pos curvature_alt_form