Documentation

Lean 4 Proof

theorem taxRevenueShare_eq {τ_L τ_K τ_C τ_corp s_L s_K s Jσ : ℝ} :
    taxRevenueShare τ_L τ_K τ_C τ_corp s_L s_K s Jσ =
    τ_L * s_L + τ_K * s_K + τ_C * (1 - s) + τ_corp / Jσ := by
  simp only [taxRevenueShare]

Dependency Graph

Location

thesis/CESProofs/Macro/TaxStructure.lean:401

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file