Documentation

Lean 4 Proof

theorem upstream_reform_for_J {beta sigma_prev sigma_prev' : ℝ}
    (hb : 0 < beta) (hsp : 0 < sigma_prev) (hsp' : 0 < sigma_prev')
    (hred : sigma_prev' < sigma_prev) {sigma_n J_n Fbar_n : ℝ}
    (hsn : 0 < sigma_n) (hJn : 0 < J_n) (hFn : 0 < Fbar_n) :
    -- Lower sigma_{n-1} raises the NGM entry k_{n,n-1}
    ngmEntryReal beta sigma_n J_n Fbar_n sigma_prev <
    ngmEntryReal beta sigma_n J_n Fbar_n sigma_prev' := by
  simp only [ngmEntryReal]
  apply div_lt_div_of_pos_left (by positivity) hsp' hred

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:332

Module Section

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

In the same file