Weighted Isoquant Dist Sq

def proved Curvature Roles

Documentation

Lean 4 Proof

def weightedIsoquantDistSq (J : ℕ) (ρ : ℝ) (x' y' : Fin J → ℝ) : ℝ :=
  ∑ j : Fin J, max (x' j) (y' j) ^ (ρ - 2) * (x' j - y' j) ^ 2

Dependency Graph

Used by

powerMean_isoquant_strong_concavity_weighted

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:37

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file

geodesicDistSq isoquantDistSq superadditivity_qualitative harmonic_mean_ge_half_min concaveOn_nonneg_of_endpoints rpow_concavity_deficit bernoulli_rpow_ge_linear powerMean_isoquant_strong_concavity_weighted superadditivity_quantitative_bound