IRS Eigenvalue Scale

def proved CES Potential

Documentation

Lean 4 Proof

def irsEigenvalueScale (J : ℕ) (γ c : ℝ) : ℝ :=
  γ * (γ - 1) / ↑J * c ^ (γ - 2)

Dependency Graph

Used by

irs_scale_eigenvalue_at_crs irs_scale_eigenvalue_pos irs_scale_immune_to_friction

Location

thesis/CESProofs/Potential/IRS.lean:72

Module Section

Increasing returns to scale results (Paper 1, Section 11):

In the same file

crs_forced scaling_idempotency irsEigenvaluePerp irs_scale_eigenvalue_at_crs irs_scale_eigenvalue_pos irs_diversity_eigenvalue_neg scaleScopeCrossPartialSign scale_scope_complementarity no_scale_scope_at_crs