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

Sectional Curvature

defprovedFoundations

Documentation

Lean 4 Proof

def sectionalCurvature (J : ℕ) (ρ c : ℝ) : ℝ :=
  cesPrincipalCurvature J ρ c ^ 2

Dependency Graph

Used by

sectionalCurvature_from_K sectionalCurvature_explicit sectionalCurvature_eq_zero_iff sectionalCurvature_via_bridge superadditivity_bound_conservative sectionalCurvature_nonneg spaceForm_at_symmetry positive_curvature_amplifies_gap arc_ge_chord intrinsic_always_nonneg

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:132

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file

gradientNormSq unitNormalComponent gradientNormSq_pos tangentSpace_is_onePerp induced_metric_eq_vecNormSq secondFundamentalFormQF gaussCurvature meanCurvatureTrace curvature_eq_neg_eigenvalue_sqrt secondFF_from_hessian gaussCurvature_pos meanCurvature_pos sectionalCurvature_nonneg sectionalCurvature_eq_zero_iff sectionalCurvature_explicit sectionalCurvature_from_K principalCurvature_trichotomy isoquant_umbilic spaceForm_at_symmetry intrinsic_always_nonneg