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

CES Principal Curvature

defprovedFoundations

Documentation

Lean 4 Proof

def cesPrincipalCurvature (J : ℕ) (ρ c : ℝ) : ℝ :=
  (1 - ρ) / (c * Real.sqrt ↑J)

Dependency Graph

Used by

sectionalCurvature_explicit secondFundamentalFormQF curvature_eq_neg_eigenvalue_sqrt sectionalCurvature_eq_zero_iff curvature_alt_form curvature_lemma sectionalCurvature_via_bridge isoquant_umbilic sectionalCurvature principalCurvature_trichotomy spaceForm_at_symmetry positive_curvature_amplifies_gap meanCurvatureTrace gaussCurvature curvature_pos

Location

thesis/CESProofs/Foundations/Hessian.lean:185

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

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