Documentation

Lean 4 Proof

theorem efficiencyGap_nonneg {K T Tstar : ℝ} (hK : 0 ≤ K) (hT : 0 ≤ T) (hTs : 0 < Tstar) :
    0 ≤ efficiencyGap K T Tstar := by
  simp only [efficiencyGap]
  apply div_nonneg
  · exact mul_nonneg hK hT
  · linarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/Defs.lean:157

Module Section

Core definitions for the Lean formalization of Paper 3:

In the same file