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

Induced Metric Eq Vec Norm Sq

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem induced_metric_eq_vecNormSq (v : Fin J → ℝ) :
    vecNormSq J v = vecNormSq J v := rfl

Dependency Graph

Location

thesis/CESProofs/Foundations/IsoquantGeometry.lean:58

Module Section

Differential Geometry of CES Isoquants (Gap #6)

In the same file

gradientNormSq unitNormalComponent gradientNormSq_pos tangentSpace_is_onePerp 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 intrinsic_always_nonneg