Documentation

Lean 4 Proof

theorem aggregateWelfareLoss_eq_zero_iff (w z : Fin N → ℝ)
    (hw : ∀ n, 0 < w n) (hz : ∀ n, 0 < z n) :
    aggregateWelfareLoss w z = 0 ↔ ∀ n, z n = 1 := by
  simp only [aggregateWelfareLoss]
  constructor
  · intro h
    -- Each term is non-negative and the sum is zero, so each term is zero
    have hterms : ∀ n, w n * welfareDistanceFn (z n) = 0 := by
      intro n
      have hnn : ∀ m, 0 ≤ w m * welfareDistanceFn (z m) :=
        fun m => mul_nonneg (le_of_lt (hw m)) (welfareDistanceFn_nonneg (hz m))
      exact (Finset.sum_eq_zero_iff_of_nonneg fun m _ => hnn m).mp h n (Finset.mem_univ n)
    intro n
    have := hterms n
    have hwn : w n ≠ 0 := ne_of_gt (hw n)
    rw [mul_eq_zero] at this
    cases this with
    | inl h => exact absurd h hwn
    | inr h => exact (welfareDistanceFn_eq_zero_iff (hz n)).mp h
  · intro h
    apply Finset.sum_eq_zero
    intro n _
    rw [h n, welfareDistanceFn_at_one, mul_zero]

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:45

Module Section

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

In the same file