Escort Fisher QF

def proved Foundations

Documentation

Lean 4 Proof

def escortFisherQF (ρ : ℝ) (P x v : Fin J → ℝ) : ℝ :=
  ρ ^ 2 * ((∑ k, P k * (v k / x k) ^ 2) -
            (∑ k, P k * (v k / x k)) ^ 2)

Dependency Graph

Used by

escortFisherQF_nonneg escortFisherQF_zero_radial general_bridge_qf

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:368

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_eq_generalK effectiveCurvature_decreasing effectiveCurvature_le_K generalHessianQF_specializes_to_symmetric general_bridge_qf escortFisherQF_nonneg escortFisherQF_zero_radial