Level Welfare Loss Nonneg

theorem proved Hierarchy

Documentation

Lean 4 Proof

theorem levelWelfareLoss_nonneg {W_nn z : ℝ} (hW : 0 < W_nn) (hz : 0 < z) :
    0 ≤ levelWelfareLoss W_nn z :=
  mul_nonneg (le_of_lt hW) (welfareDistanceFn_nonneg hz)

Dependency Graph

Location

thesis/CESProofs/Hierarchy/WelfareDecomposition.lean:177

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