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

Escort Herfindahl

defprovedFoundations

Documentation

Lean 4 Proof

def escortHerfindahl (P : Fin J → ℝ) : ℝ :=
  ∑ j, P j ^ 2

Dependency Graph

Used by

effectiveCurvatureAt effectiveCurvature_eq_generalK effectiveCurvature_le_K effectiveCurvature_at_symmetry effectiveCurvature_decreasing

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:72

Module Section

General CES Hessian at Arbitrary Allocation

In the same file

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