Documentation

Lean 4 Proof

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

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:448

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file