Documentation

Lean 4 Proof

theorem value_function_welfare_contribution {J_low J_high ρ c : ℝ}
    (hJl : 1 < J_low) (hJlh : J_low < J_high)
    (hρ0 : 0 < ρ) (hρ1 : ρ < 1) (hc : 0 < c) :
    0 < valueFunction J_high ρ c - valueFunction J_low ρ c := by
  linarith [valueFunction_increasing hJl hJlh hρ0 hρ1 hc]

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:316

Module Section

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

In the same file