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

CES General Hessian QF

defprovedFoundations

Documentation

Lean 4 Proof

def cesGeneralHessianQF (ρ F : ℝ)
    (P x v : Fin J → ℝ) : ℝ :=
  ∑ i : Fin J, ∑ j : Fin J,
    cesGeneralHessianEntry ρ F P x i j * v i * v j

Dependency Graph

Used by

cesGeneralHessianQF_neg_semidef cesGeneralHessianQF_eq_neg_variance cesGeneralHessianQF_euler general_bridge_qf

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:64

Module Section

General CES Hessian at Arbitrary Allocation

In the same file

cesGeneralHessianEntry escortHerfindahl effectiveCurvatureAt multinomial_qf cesGeneralHessianQF_eq_neg_variance weighted_variance_nonneg cesGeneralHessianQF_neg_semidef cesGeneralHessianQF_euler effectiveCurvature_at_symmetry effectiveCurvature_eq_generalK effectiveCurvature_decreasing effectiveCurvature_le_K generalHessianQF_specializes_to_symmetric escortFisherQF general_bridge_qf escortFisherQF_nonneg escortFisherQF_zero_radial