Isoquant Dist Sq

def proved Curvature Roles

Documentation

Lean 4 Proof

def isoquantDistSq (J : ℕ) (x y : Fin J → ℝ) (Fx Fy : ℝ) : ℝ :=
  ∑ j : Fin J, (x j / Fx - y j / Fy) ^ 2

Dependency Graph

Used by

chordalDistSq chordalDistSq_self chordalDistSq_nonneg

Location

thesis/CESProofs/CurvatureRoles/Superadditivity.lean:31

Module Section

Superadditivity of CES (Paper 1, Section 6):

In the same file

geodesicDistSq weightedIsoquantDistSq 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