Level Welfare Loss

def proved Hierarchy

Documentation

Lean 4 Proof

def levelWelfareLoss (W_nn z : ℝ) : ℝ := W_nn * welfareDistanceFn z

Dependency Graph

Used by

levelWelfareLoss_nonneg

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:174

Module Section

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

In the same file

aggregateWelfareLoss 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_nonneg logistic_fragility_positive logistic_fragility_negative logistic_fragility_unbounded knockout_cascade_step knockout_cascade welfareDistanceFn_pos