Documentation

Lean 4 Proof

theorem extendedWelfare_at_optimum {V_base W_J Jstar : ℝ}
    (hJs : 0 < Jstar) :
    extendedWelfare V_base W_J Jstar Jstar = V_base := by
  simp only [extendedWelfare]
  rw [div_self (ne_of_gt hJs)]
  rw [welfareDistanceFn_at_one]
  ring

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:264

Module Section

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

In the same file