Firm Scope No Complementarity At Crs

theorem proved CES Potential

Documentation

Lean 4 Proof

theorem firm_scope_no_complementarity_at_crs
    (ρ : ℝ) :
    scaleScopeCrossPartialSign 1 ρ = 0 := by
  exact no_scale_scope_at_crs ρ

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:252

Module Section

## IRS and Firm Scope

In the same file

firmScopeObjective optimal_scope_foc integration_boundary williamson_special_case monotone_integration spillover_adjusted_boundary fragilityIndex fragility_total fragility_bounds knockout_from_paper1 irs_scale_immune_to_friction irs_amplifies_diversity_window irs_diversity_eigenvalue_nonpos firm_scope_irs_complementarity irs_shifts_integration_boundary scale_scope_monotone_in_gamma