Documentation

Lean 4 Proof

theorem settlementR0_pos (e : SettlementEconomy) : 0 < settlementR0 e :=
  div_pos (mul_pos e.h_cross_phi_S e.h_cross_S_phi)
          (mul_pos e.h_self_phi e.h_self_S)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:94

Module Section

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

In the same file