Effective Curvature Decreasing

theorem proved Foundationskey theorem

Documentation

Lean 4 Proof

theorem effectiveCurvature_decreasing {ρ : ℝ} (hρ : ρ < 1)
    (P₁ P₂ : Fin J → ℝ)
    (hH : escortHerfindahl P₁ < escortHerfindahl P₂) :
    effectiveCurvatureAt ρ P₂ < effectiveCurvatureAt ρ P₁ := by
  unfold effectiveCurvatureAt
  have h1 : 0 < 1 - ρ := by linarith
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:284

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_le_K generalHessianQF_specializes_to_symmetric escortFisherQF general_bridge_qf escortFisherQF_nonneg escortFisherQF_zero_radial