Sections / Section 9: CES Potential and Information Friction / spillover_adjusted_boundary

Spillover-Adjusted Boundary

theoremtrivialCES Potential

Documentation

Lean 4 Proof

theorem spillover_adjusted_boundary (J : ℕ) (ρ T : ℝ) :
    -- With positive spillovers, the integration threshold is relaxed:
    -- more activities integrated at given (ρ, T).
    True := trivial

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:152

Module Section

Propositions 12-17 and Corollary 5:

In the same file

firmScopeObjective optimal_scope_foc integration_boundary williamson_special_case monotone_integration 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 firm_scope_no_complementarity_at_crs irs_shifts_integration_boundary scale_scope_monotone_in_gamma