Documentation

Lean 4 Proof

def extendedWelfare (V_base W_J J Jstar : ℝ) : ℝ :=
  V_base + W_J * welfareDistanceFn (J / Jstar)

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:259

Module Section

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

In the same file