Documentation

Lean 4 Proof

def dynamicWedge (B₀ η D₀ δ_gap τ : ℝ) : ℝ :=
  lafferRevenue B₀ η τ * δ_gap / (discountGap D₀ δ_gap τ) ^ 2

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:73

Module Section

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

In the same file