Diversity Welfare Loss

def proved Dynamics & Crises

Documentation

Lean 4 Proof

def diversityWelfareLoss (J Jstar : ℝ) : ℝ :=
  welfareDistanceFn (J / Jstar)

Dependency Graph

Used by

diversityWelfareLoss_nonneg diversityWelfareLoss_eq_zero_iff

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:252

Module Section

## Welfare with Endogenous J (merged from EntryExitWelfare.lean)