No Scale Scope At Crs

theorem proved CES Potential

Documentation

Lean 4 Proof

theorem no_scale_scope_at_crs (ρ : ℝ) :
    scaleScopeCrossPartialSign 1 ρ = 0 := by
  simp [scaleScopeCrossPartialSign]

Dependency Graph

Used by

firm_scope_no_complementarity_at_crs

Location

thesis/CESProofs/Potential/IRS.lean:128

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 scaleScopeCrossPartialSign scale_scope_complementarity