IRS Scale Eigenvalue At Crs

theorem proved CES Potential

Documentation

Lean 4 Proof

theorem irs_scale_eigenvalue_at_crs (hJ : 0 < J) (c : ℝ) :
    irsEigenvalueScale J 1 c = 0 := by
  simp [irsEigenvalueScale]

Dependency Graph

Location

thesis/CESProofs/Potential/IRS.lean:80

Module Section

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

In the same file

crs_forced scaling_idempotency irsEigenvalueScale irsEigenvaluePerp irs_scale_eigenvalue_pos irs_diversity_eigenvalue_neg scaleScopeCrossPartialSign scale_scope_complementarity no_scale_scope_at_crs