Documentation

Lean 4 Proof

theorem recovery_ordering {J : ℕ} (hJ : 2 ≤ J) {rho_1 rho_2 c d_sq : ℝ}
    (hc : 0 < c) (hd : 0 < d_sq)
    (hrho1 : rho_1 < 1) (hrho2 : rho_2 < 1) (h12 : rho_1 < rho_2) :
    criticalFriction J rho_1 c d_sq < criticalFriction J rho_2 c d_sq :=
  rho_ordering_criticalFriction hJ hc hd hrho1 hrho2 h12

Dependency Graph

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:191

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file