Documentation

Lean 4 Proof

theorem diversityWelfareLoss_eq_zero_iff {J Jstar : ℝ}
    (hJ : 0 < J) (hJs : 0 < Jstar) :
    diversityWelfareLoss J Jstar = 0 ↔ J = Jstar := by
  simp only [diversityWelfareLoss]
  rw [welfareDistanceFn_eq_zero_iff (div_pos hJ hJs)]
  constructor
  · intro h; linarith [div_eq_one_iff_eq (ne_of_gt hJs) |>.mp h]
  · intro h; rw [h, div_self (ne_of_gt hJs)]

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:279

Module Section

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

In the same file