Scale Scope Cross Partial Sign

def proved CES Potential

Documentation

Lean 4 Proof

def scaleScopeCrossPartialSign (γ ρ : ℝ) : ℝ := γ * (γ - 1) * (1 - ρ)

Dependency Graph

Used by

firm_scope_irs_complementarity scale_scope_complementarity no_scale_scope_at_crs firm_scope_no_complementarity_at_crs scale_scope_monotone_in_gamma

Location

thesis/CESProofs/Potential/IRS.lean:117

Module Section

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

In the same file

crs_forced scaling_idempotency irsEigenvalueScale irsEigenvaluePerp irs_scale_eigenvalue_at_crs irs_scale_eigenvalue_pos irs_diversity_eigenvalue_neg scale_scope_complementarity no_scale_scope_at_crs