Documentation

Lean 4 Proof

theorem ramsey_inverse_elasticity {a e₁ e₂ : ℝ}
    (ha : 0 < a) (he₁ : 0 < e₁) (he₂ : 0 < e₂) (he : e₁ < e₂) :
    saezTopRate a e₂ < saezTopRate a e₁ :=
  saezTopRate_decreasing_in_e ha he₁ he₂ he

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:445

Module Section

Growth and Dynamic Tax Revenue (Layer 4-5 of Macro Extension)

In the same file