Documentation

Lean 4 Proof

theorem taxRevenueShare_uniform {τ s_L s_K s Jσ : ℝ} :
    taxRevenueShare τ τ τ τ s_L s_K s Jσ =
    τ * (s_L + s_K + (1 - s)) + τ / Jσ := by
  simp only [taxRevenueShare]; ring

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:407

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file