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

Chordal Dist Sq Self

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem chordalDistSq_self (x : Fin J → ℝ) {c : ℝ} (_hc : c ≠ 0) :
    chordalDistSq J x x c = 0 := by
  simp [chordalDistSq, isoquantDistSq]

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:244

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 sectionalCurvature_nonneg sectionalCurvature_eq_zero_iff sectionalCurvature_explicit sectionalCurvature_from_K principalCurvature_trichotomy isoquant_umbilic spaceForm_at_symmetry