def
definition
def or abbrev
net_flow
show as:
view Lean formalization →
formal statement (Lean)
99noncomputable def net_flow (L : Ledger) (agent : ℕ) : ℝ :=
proof body
Definition body.
100 L.events.foldl (fun acc e =>
101 if e.source = agent then acc + Real.log e.ratio
102 else if e.target = agent then acc + Real.log e.ratio
103 else acc) 0
104
105/-! ## The Empty Ledger -/
106
107/-- The empty ledger: no events. -/