empty_ledger_balance

formal source

  98  balance_eq := by simp
  99}
 100
 101theorem empty_ledger_balance : emptyLedger.balance = 0 := rfl
 102
 103theorem empty_ledger_cost : totalCost emptyLedger = 0 := by
 104  simp [totalCost, emptyLedger]
 105
 106/-! ## Ledger Updates -/
 107
 108/-- A ledger update is a pair of entries that cancel (reciprocal ratios). -/
 109structure LedgerUpdate where
 110  /-- First entry -/
 111  entry1 : LedgerEntry
 112  /-- Second entry (reciprocal) -/
 113  entry2 : LedgerEntry
 114  /-- The ratios are reciprocals -/
 115  reciprocal : entry2.ratio = entry1.ratio⁻¹
 116  /-- Different IDs -/
 117  distinct : entry1.id ≠ entry2.id
 118
 119/-- Apply an update to a ledger. -/
 120noncomputable def applyUpdate (L : Ledger) (u : LedgerUpdate) : Ledger := {
 121  entries := u.entry1 :: u.entry2 :: L.entries
 122  balance := L.balance  -- Preserved because log(r) + log(1/r) = 0
 123  balance_eq := by
 124    simp only [List.map_cons, List.sum_cons]
 125    have h_cancel : Real.log u.entry1.ratio + Real.log u.entry2.ratio = 0 := by
 126      rw [u.reciprocal, Real.log_inv]
 127      ring
 128    rw [L.balance_eq]
 129    linarith [h_cancel]
 130}
 131