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

Vec Sum

defprovedFoundations

Documentation

Lean 4 Proof

def vecSum (J : ℕ) (v : Fin J → ℝ) : ℝ := ∑ j : Fin J, v j

Dependency Graph

Used by

gradient_orthogonal_to_onePerp tangentSpace_is_onePerp orthToOne uniform_spectralGap cesHessianQF_on_perp disconnected_zero_curvature uniform_fiedler_degenerate uniform_laplacianQF_on_perp logCesHessian_on_perp

Location

thesis/CESProofs/Foundations/Hessian.lean:40

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

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