Documentation

Lean 4 Proof

theorem allocationDistortion_nonneg {T Tstar : ℝ} (hT : 0 ≤ T) (hTs : 0 < Tstar) :
    0 ≤ allocationDistortion T Tstar := by
  simp only [allocationDistortion]
  have : max 0 (1 - T / Tstar) ≤ 1 :=
    max_le zero_le_one (by linarith [div_nonneg hT (le_of_lt hTs)])
  linarith

Dependency Graph

Used by

Location

thesis/CESProofs/Potential/MacroApplications.lean:161

Module Section

Macroeconomic Applications of the CES Potential

In the same file