Tax Revenue

def proved Macroeconomics

Documentation

Lean 4 Proof

def taxRevenue (τ_L τ_K τ_C τ_corp wL rK C Prof : ℝ) : ℝ :=
  τ_L * wL + τ_K * rK + τ_C * C + τ_corp * Prof

Dependency Graph

Used by

taxRevenue_zero_rates taxRevenue_increasing_in_τC taxRevenue_additive taxRevenue_scale taxRevenue_increasing_in_τL taxRevenue_increasing_in_τcorp taxRevenue_increasing_in_τK

Location

thesis/CESProofs/Macro/TaxStructure.lean:33

Module Section

Government Tax Structure (Layer 3 of Macro Extension)