Documentation

Lean 4 Proof

theorem welfareLoss_nonneg {Fstar Fx : ℝ} (h : Fx ≤ Fstar) :
    0 ≤ welfareLoss Fstar Fx := by
  simp [welfareLoss]; linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/Defs.lean:97

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file