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

Effective Curvature Eq General K

theoremprovedFoundations

Documentation

Lean 4 Proof

theorem effectiveCurvature_eq_generalK (ρ : ℝ)
    (P : Fin J → ℝ) :
    effectiveCurvatureAt ρ P = generalCurvatureK J ρ P := by
  simp only [effectiveCurvatureAt, escortHerfindahl,
    generalCurvatureK]

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:267

Module Section

General CES Hessian at Arbitrary Allocation

In the same file

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