Documentation

Lean 4 Proof

theorem aggregateWelfareLoss_nonneg (w z : Fin N → ℝ)
    (hw : ∀ n, 0 < w n) (hz : ∀ n, 0 < z n) :
    0 ≤ aggregateWelfareLoss w z := by
  simp only [aggregateWelfareLoss]
  exact Finset.sum_nonneg fun n _ =>
    mul_nonneg (le_of_lt (hw n)) (welfareDistanceFn_nonneg (hz n))

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:37

Module Section

Theorems 7-8, Propositions 5 and 7, Corollary 3:

In the same file