entry_cost_zero_iff_unity

formal source

  72  exact Jcost_nonneg e.ratio_pos
  73
  74/-- The J-cost is zero iff the ratio is 1. -/
  75theorem entry_cost_zero_iff_unity (e : LedgerEntry) : e.cost = 0 ↔ e.ratio = 1 := by
  76  rw [e.cost_eq]
  77  exact Jcost_eq_zero_iff e.ratio e.ratio_pos
  78
  79/-! ## Ledger Structure with Conservation -/
  80
  81/-- A ledger is a collection of entries with conservation constraint. -/
  82structure Ledger where
  83  /-- The entries in the ledger -/
  84  entries : List LedgerEntry
  85  /-- Total balance (sum of log-ratios) -/
  86  balance : ℝ
  87  /-- Balance equals sum of log-ratios -/
  88  balance_eq : balance = (entries.map (fun e => Real.log e.ratio)).sum
  89
  90/-- The total J-cost of a ledger. -/
  91noncomputable def totalCost (L : Ledger) : ℝ :=
  92  (L.entries.map (·.cost)).sum
  93
  94/-- Empty ledger has zero balance. -/
  95def emptyLedger : Ledger := {
  96  entries := []
  97  balance := 0
  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