Documentation

Lean 4 Proof

theorem lafferMaxRevenue_decreasing_in_η {B₀ η₁ η₂ : ℝ}
    (hB : 0 < B₀) (hη₁ : 0 < η₁) (_hη₂ : 0 < η₂) (hη : η₁ < η₂) :
    lafferMaxRevenue B₀ η₂ < lafferMaxRevenue B₀ η₁ := by
  simp only [lafferMaxRevenue]
  exact div_lt_div_of_pos_left hB (by linarith) (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:441

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file