Documentation

Lean 4 Proof

theorem irreversibility_of_adoption {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) :
    criticalFrictionReal J_crit ρ c d_sq < criticalFrictionReal J_high ρ c d_sq := by
  have hJh : 1 < J_high := by linarith
  rw [criticalFrictionReal_eq J_crit ρ c d_sq hJc (by linarith),
      criticalFrictionReal_eq J_high ρ c d_sq hJh (by linarith)]
  apply div_lt_div_of_pos_right _ (by linarith)
  have hc2 : 0 < c ^ 2 := sq_pos_of_pos hc
  nlinarith [mul_pos hc2 hd]

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/RegimeShift.lean:118

Module Section

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

In the same file