ledgerJlogCost_post

formal source

 180  dsimp [ledgerJlogCost]
 181  exact add_nonneg h₁ h₂
 182
 183private lemma ledgerJlogCost_post {d : Nat} (L : LedgerState d) (k : Fin d) (side : Side) :
 184    ledgerJlogCost (d := d) L (post L k side) = Cost.Jlog (1 : ℝ) := by
 185  classical
 186  cases side with
 187  | debit =>
 188      -- debit has one +1 delta at k; credit deltas are 0
 189      have hdeb :
 190          (∑ i : Fin d, Cost.Jlog (((post L k Side.debit).debit i - L.debit i : ℤ) : ℝ))
 191            = Cost.Jlog (1 : ℝ) := by
 192        let f : Fin d → ℝ := fun i => Cost.Jlog (((post L k Side.debit).debit i - L.debit i : ℤ) : ℝ)
 193        have hsplit :=
 194          (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
 195        have fk : f k = Cost.Jlog (1 : ℝ) := by
 196          simp [f, post]
 197        have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
 198          refine Finset.sum_eq_zero ?_
 199          intro i hi
 200          have hik : i ≠ k := by simpa [Finset.mem_erase] using hi
 201          simp [f, post, hik]
 202        -- `sum univ = f k + sum (erase k)`
 203        calc
 204          (∑ i : Fin d, f i) =
 205              f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
 206            simpa using hsplit.symm
 207          _ = Cost.Jlog (1 : ℝ) := by simp [fk, hErase]
 208      have hcred :
 209          (∑ i : Fin d, Cost.Jlog (((post L k Side.debit).credit i - L.credit i : ℤ) : ℝ)) = 0 := by
 210        refine Finset.sum_eq_zero ?_
 211        intro i _
 212        simp [post]
 213      -- avoid `simp` unfolding `Jlog` into exp-sums (it introduces `-↑d` terms).