CES Hessian QF

def proved Foundations

Documentation

Lean 4 Proof

def cesHessianQF (J : ℕ) (ρ c : ℝ) (v : Fin J → ℝ) : ℝ :=
  (1 - ρ) / ((↑J : ℝ) ^ 2 * c) * ((∑ j : Fin J, v j) ^ 2 - ↑J * ∑ j : Fin J, v j ^ 2)

Dependency Graph

Used by

ces_strict_concavity_on_perp strategic_bound saddle_point_substitutes cesHessianQF_neg_semidef strategic_instability cesHessianQF_on_perp hessianQF_eq_negK_norm strategic_independence_qualitative cesHessianQF_pos_on_perp SextupleRoleStatement logCesHessianQF unique_equilibrium_complements manipulation_magnitude cesHessianQF_on_one cesHessianQF_eq_sum secondFF_from_hessian generalHessianQF_specializes_to_symmetric cesHessianQF_pos_semidef_substitute uniform_networkHessian_eq_cesHessian

Location

thesis/CESProofs/Foundations/Hessian.lean:33

Module Section

Gradient and Hessian of CES at the symmetric point.

In the same file

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