Documentation

Lean 4 Proof

theorem persistencePremium_pos {J_crit J_high ρ c d_sq : ℝ}
    (hJc : 1 < J_crit) (hJch : J_crit < J_high) (hρ : ρ < 1)
    (hc : 0 < c) (hd : 0 < d_sq) :
    0 < persistencePremium J_high J_crit ρ c d_sq := by
  simp only [persistencePremium]
  linarith [irreversibility_of_adoption hJc hJch hρ hc hd]

Dependency Graph

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:134

Module Section

Paper 3c, Section 3: First-Order Regime Shift

In the same file