Documentation

Lean 4 Proof

def levelEffect (s₀ ψ δ τ : ℝ) : ℝ :=
  investmentRate s₀ ψ τ / δ

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/GrowthTax.lean:62

Module Section

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

In the same file