Documentation

Lean 4 Proof

def frDerivMagnitude (FR₀ α_FR S_crit S : ℝ) : ℝ :=
  FR₀ * α_FR / S_crit * (1 - S / S_crit) ^ (α_FR - 1)

Dependency Graph

Used by

Location

thesis/CESProofs/Applications/SettlementFeedback.lean:452

Module Section

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

In the same file