Documentation

Lean 4 Proof

theorem irs_shifts_integration_boundary
    {K_eff γ₁ γ₂ T g h : ℝ}
    (hK : 0 < K_eff) (hg : 0 < g) (hγ : γ₁ < γ₂) :
    irsFirmProfit K_eff γ₁ T g h < irsFirmProfit K_eff γ₂ T g h := by
  unfold irsFirmProfit
  have hKg : 0 < K_eff * g := mul_pos hK hg
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Potential/FirmScope.lean:260

Module Section

## IRS and Firm Scope

In the same file