Documentation

Lean 4 Proof

theorem displacement_dominance {theta_disp theta_rest delta_off g_off : ℝ}
    (hg : 0 < g_off) (hrest : 0 < theta_rest)
    (h_ratio : delta_off / g_off < theta_disp / theta_rest) :
    delta_off * theta_rest < theta_disp * g_off := by
  rwa [div_lt_div_iff₀ hg hrest] at h_ratio

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:218

Module Section

Paper 7: Settlement Feedback and Monetary Policy in a Mesh Economy

In the same file