Effective Curvature At Symmetry

theorem proved Foundationskey theorem

Documentation

Lean 4 Proof

theorem effectiveCurvature_at_symmetry (hJ : 0 < J) (ρ : ℝ) :
    effectiveCurvatureAt ρ
      (fun _ : Fin J => (1 : ℝ) / ↑J) =
      curvatureK J ρ := by
  unfold effectiveCurvatureAt escortHerfindahl curvatureK
  simp only [Finset.sum_const, Finset.card_fin,
    nsmul_eq_mul]
  have hJne : (↑J : ℝ) ≠ 0 :=
    Nat.cast_ne_zero.mpr (by omega)
  field_simp

Dependency Graph

Location

thesis/CESProofs/Foundations/GeneralHessian.lean:248

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