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

Vec Norm Sq

defprovedFoundations

Documentation

Lean 4 Proof

def vecNormSq (J : ℕ) (v : Fin J → ℝ) : ℝ := ∑ j : Fin J, v j ^ 2

Dependency Graph

Used by

ces_strict_concavity_on_perp secondFundamentalFormQF strategic_bound cesHessianQF_neg_semidef networkHessian_spectralGap_bound fiedlerVector tsallisHessian_uniform_on_perp induced_metric_eq_vecNormSq uniform_spectralGap cesHessianQF_on_perp adding_link_increases_gap hessianQF_eq_negK_norm spectralGap isoquant_umbilic manipulation_magnitude disconnected_zero_curvature uniform_fiedler_degenerate uniform_laplacianQF_on_perp logCesHessian_on_perp

Location

thesis/CESProofs/Foundations/Hessian.lean:46

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

cesHessianQF cesEigenvaluePerp vecSum orthToOne 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