Documentation

Lean 4 Proof

theorem diversityWelfareLoss_nonneg {J Jstar : ℝ}
    (hJ : 0 < J) (hJs : 0 < Jstar) :
    0 ≤ diversityWelfareLoss J Jstar :=
  welfareDistanceFn_nonneg (div_pos hJ hJs)

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:273

Module Section

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

In the same file