Documentation

Lean 4 Proof

def taxRevenueShare (τ_L τ_K τ_C τ_corp s_L s_K s Jσ : ℝ) : ℝ :=
  τ_L * s_L + τ_K * s_K + τ_C * (1 - s) + τ_corp / Jσ

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TaxStructure.lean:39

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file