Documentation

Lean 4 Proof

theorem transition_iff_det_sign (e : SettlementEconomy) :
    0 < e.self_phi * e.self_S - e.cross_phi_S * e.cross_S_phi ↔
    settlementR0 e < 1 := by
  simp only [settlementR0]
  rw [div_lt_one (mul_pos e.h_self_phi e.h_self_S)]
  constructor
  · intro h; linarith
  · intro h; linarith

Dependency Graph

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:181

Module Section

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

In the same file