Documentation

Lean 4 Proof

theorem dynamic_wedge_pos {B₀ η D₀ δ_gap τ : ℝ}
    (hR : 0 < lafferRevenue B₀ η τ) (hδ : 0 < δ_gap)
    (hD : 0 < discountGap D₀ δ_gap τ) :
    0 < dynamicWedge B₀ η D₀ δ_gap τ := by
  simp only [dynamicWedge]
  exact div_pos (mul_pos hR hδ) (sq_pos_of_pos hD)

Dependency Graph

Location

thesis/CESProofs/Macro/GrowthTax.lean:405

Module Section

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

In the same file