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

Orth To One

defprovedFoundations

Documentation

Lean 4 Proof

def orthToOne (J : ℕ) (v : Fin J → ℝ) : Prop := vecSum J v = 0

Dependency Graph

Used by

gradient_orthogonal_to_onePerp ces_strict_concavity_on_perp strategic_bound saddle_point_substitutes tangentSpace_is_onePerp cesHessianQF_neg_semidef networkHessian_spectralGap_bound fiedlerVector tsallisHessian_uniform_on_perp strategic_instability uniform_spectralGap cesHessianQF_on_perp adding_link_increases_gap hessianQF_eq_negK_norm strategic_independence_qualitative cesHessianQF_pos_on_perp spectralGap SextupleRoleStatement unique_equilibrium_complements manipulation_magnitude secondFF_from_hessian disconnected_zero_curvature cesHessianQF_pos_semidef_substitute detection_asymmetry uniform_fiedler_degenerate uniform_laplacianQF_on_perp logCesHessian_on_perp

Location

thesis/CESProofs/Foundations/Hessian.lean:43

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

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