Aggregate Welfare Loss

def proved Hierarchy

Documentation

Lean 4 Proof

def aggregateWelfareLoss (w z : Fin N → ℝ) : ℝ :=
  ∑ n : Fin N, w n * welfareDistanceFn (z n)

Dependency Graph

Used by

aggregateWelfareLoss_nonneg aggregateWelfareLoss_eq_zero_iff

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:29

Module Section

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

In the same file

aggregateWelfareLoss_nonneg aggregateWelfareLoss_eq_zero_iff welfare_lyapunov_dissipation lyapunov_within_level_dissipation eigenstructure_bridge_diagonal bridge_eigenvalue bridge_W_uniform_depreciation welfare_loss_quadratic_approx levelWelfareLoss levelWelfareLoss_nonneg logistic_fragility_positive logistic_fragility_negative logistic_fragility_unbounded knockout_cascade_step knockout_cascade welfareDistanceFn_pos