Documentation

Lean 4 Proof

lemma fr_inner_nonneg {S S_crit : ℝ} (_hS : 0 ≤ S) (_hSc : 0 < S_crit) :
    0 ≤ 1 - min 1 (S / S_crit) := by
  simp [sub_nonneg]

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:349

Module Section

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

In the same file