IRS Eigenvalue Perp

def proved CES Potential

Documentation

Lean 4 Proof

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

Dependency Graph

Used by

irs_diversity_eigenvalue_neg irs_diversity_eigenvalue_nonpos irsEffectiveCurvaturePerp

Location

thesis/CESProofs/Potential/IRS.lean:76

Module Section

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

In the same file

crs_forced scaling_idempotency irsEigenvalueScale irs_scale_eigenvalue_at_crs irs_scale_eigenvalue_pos irs_diversity_eigenvalue_neg scaleScopeCrossPartialSign scale_scope_complementarity no_scale_scope_at_crs