Documentation

Lean 4 Proof

theorem upstream_reform_beta_for_J {beta beta' sigma_n J_n Fbar_n sigma_prev : ℝ}
    (_hb : 0 < beta) (_hb' : 0 < beta') (hbb : beta < beta')
    (hsn : 0 < sigma_n) (hJn : 0 < J_n) (hFn : 0 < Fbar_n)
    (hsp : 0 < sigma_prev) :
    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_right _ hsp
  have h1 : 0 < sigma_n * J_n * Fbar_n := by positivity
  nlinarith

Dependency Graph

Location

thesis/CESProofs/Dynamics/EntryExitDynamics.lean:343

Module Section

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

In the same file