mkEntry

formal source

  57  cost_eq : cost = Jcost ratio
  58
  59/-- Create a ledger entry from a ratio and phase. -/
  60noncomputable def mkEntry (id : ℕ) (r : ℝ) (hr : 0 < r) (p : Fin 8) : LedgerEntry := {
  61  id := id
  62  ratio := r
  63  ratio_pos := hr
  64  cost := Jcost r
  65  phase := p
  66  cost_eq := rfl
  67}
  68
  69/-- The J-cost of an entry is non-negative. -/
  70theorem entry_cost_nonneg (e : LedgerEntry) : 0 ≤ e.cost := by
  71  rw [e.cost_eq]
  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. -/