Documentation

Lean 4 Proof

theorem lafferPeak_below_upper {η : ℝ} (hη : 0 < η) :
    lafferPeak η < 1 / η := by
  simp only [lafferPeak]
  exact div_lt_div_of_pos_left one_pos hη (by linarith)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:233

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file