Documentation

Lean 4 Proof

theorem rho_drift_shifts_Tstar {J : ℕ} (hJ : 2 ≤ J)
    {rho1 rho2 : ℝ} (hrho1 : rho1 < 1) (hrho2 : rho2 < 1)
    (hrho : rho1 < rho2) {c d_sq : ℝ} (hc : 0 < c) (hd : 0 < d_sq) :
    criticalFriction J rho1 c d_sq ≠ criticalFriction J rho2 c d_sq :=
  ne_of_lt (complementary_goods_more_fragile hJ hrho1 hrho2 hrho hc hd)

Dependency Graph

Location

thesis/CESProofs/Applications/TimeInconsistency.lean:137

Module Section

Time Inconsistency Resolution via Upstream Reform (Gap 11)

In the same file