Documentation

Lean 4 Proof

theorem welfareContribution_nonneg {sigma_prev delta beta_n : ℝ}
    (hs : 0 ≤ sigma_prev) (hb : 0 < beta_n) :
    0 ≤ welfareContribution sigma_prev delta beta_n := by
  simp only [welfareContribution]
  apply div_nonneg
  · exact mul_nonneg hs (sq_nonneg _)
  · linarith

Dependency Graph

Location

thesis/CESProofs/Hierarchy/Defs.lean:230

Module Section

Core definitions for the Lean formalization of Paper 4:

In the same file