Documentation

Lean 4 Proof

theorem lafferMaxRevenue_pos {B₀ η : ℝ} (hB : 0 < B₀) (hη : 0 < η) :
    0 < lafferMaxRevenue B₀ η := by
  simp only [lafferMaxRevenue]
  exact div_pos hB (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:221

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file