Documentation

Lean 4 Proof

theorem lyapunov_within_level_dissipation
    (sigma : Fin N → ℝ) (z : Fin N → ℝ)
    (hsigma : ∀ n, 0 < sigma n) (hz : ∀ n, 0 < z n) :
    0 ≤ ∑ n : Fin N, sigma n * welfareDistanceFn (z n) := by
  exact Finset.sum_nonneg fun n _ =>
    mul_nonneg (le_of_lt (hsigma n)) (welfareDistanceFn_nonneg (hz n))

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:91

Module Section

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

In the same file