General Curvature K

def proved Foundations

Documentation

Lean 4 Proof

def generalCurvatureK (J : ℕ) (ρ : ℝ) (a : Fin J → ℝ) : ℝ :=
  (1 - ρ) * (1 - ∑ j : Fin J, a j ^ 2)

Dependency Graph

Used by

Tstar_increasing_in_herfindahl effectiveCurvature_eq_generalK generalEffectiveCurvatureKeff generalKeff_zero_friction rho_ordering_preserved_general_weights K_deficit_from_concentration gen_quadruple_K_pos K_positive_nondegenerate knockout_risk_increases_with_concentration equal_weight_entry_maximizes_K levelGeneralCurvature equal_weights_maximize_K generalCriticalFriction K_decreasing_in_herfindahl_sector sectorGeneralCurvature K_decreasing_in_herfindahl K_reduction_equal_weights equalWeights_maximize_K

Location

thesis/CESProofs/Foundations/GeneralWeights.lean:27

Module Section

General-weight CES results (Paper 1, Section 10):

In the same file

gen_hessian_equal_marginals genCesHessianQF secular_equation K_reduction_equal_weights gen_quadruple_K_pos equal_weights_maximize_K equalWeights_maximize_K weighted_emergence