Documentation

Lean 4 Proof

theorem debtSustainable_iff {r_B g b d : ℝ} :
    debtSustainable r_B g b d ↔ d ≤ (g - r_B) * b := by
  simp only [debtSustainable, debtDynamics]; constructor <;> intro h <;> linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Macro/TaxStructure.lean:365

Module Section

Government Tax Structure (Layer 3 of Macro Extension)

In the same file