Documentation

Lean 4 Proof

theorem rho_ordering_criticalFriction {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 := by
  simp only [criticalFriction]
  -- Numerator is the same positive constant
  have hnum : 0 < 2 * (↑J - 1) * c ^ 2 * d_sq := by
    apply mul_pos
    · apply mul_pos
      · apply mul_pos (by norm_num)
        · have : (1 : ℝ) < ↑J := by exact_mod_cast (show 1 < J by omega)
          linarith
      · exact sq_pos_of_pos hc
    · exact hd
  -- K_1 > K_2 (curvature decreasing in rho)
  have hK12 : curvatureK J rho_2 < curvatureK J rho_1 :=
    K_increases_with_complementarity hJ hrho2 hrho1 h12
  have hK1 : 0 < curvatureK J rho_1 := curvatureK_pos hJ hrho1
  have hK2 : 0 < curvatureK J rho_2 := curvatureK_pos hJ hrho2
  -- num/K_1 < num/K_2 because K_1 > K_2 > 0
  exact div_lt_div_of_pos_left hnum hK2 hK12

Dependency Graph

Used by

Location

thesis/CESProofs/Dynamics/BusinessCycles.lean:154

Module Section

Results 47-62: Business Cycles on the CES Landscape

In the same file