Saez Top Rate Decreasing In A

theorem proved Macroeconomics

Documentation

Lean 4 Proof

theorem saezTopRate_decreasing_in_a {a₁ a₂ e : ℝ}
    (_ha₁ : 0 < a₁) (_ha₂ : 0 < a₂) (_he : 0 < e) (ha : a₁ < a₂) :
    saezTopRate a₂ e < saezTopRate a₁ e := by
  simp only [saezTopRate]
  exact div_lt_div_of_pos_left one_pos (by nlinarith) (by nlinarith)

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:326

Module Section

Government Tax Structure (Layer 3 of Macro Extension)