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

Effective Curvature At

defprovedFoundations

Documentation

Lean 4 Proof

def effectiveCurvatureAt (ρ : ℝ) (P : Fin J → ℝ) : ℝ :=
  (1 - ρ) * (1 - escortHerfindahl P)

Dependency Graph

Used by

effectiveCurvature_eq_generalK effectiveCurvature_le_K effectiveCurvature_at_symmetry effectiveCurvature_decreasing

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:82

Module Section

General CES Hessian at Arbitrary Allocation

In the same file

cesGeneralHessianEntry cesGeneralHessianQF escortHerfindahl 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