lemma
proved
tactic proof
ledgerJlogCost_post
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Tactic-mode proof.
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).
214 simp only [ledgerJlogCost, hdeb, hcred, add_zero, zero_add]
215 | credit =>
216 have hdeb :
217 (∑ i : Fin d, Cost.Jlog (((post L k Side.credit).debit i - L.debit i : ℤ) : ℝ)) = 0 := by
218 refine Finset.sum_eq_zero ?_
219 intro i _
220 simp [post]
221 have hcred :
222 (∑ i : Fin d, Cost.Jlog (((post L k Side.credit).credit i - L.credit i : ℤ) : ℝ))
223 = Cost.Jlog (1 : ℝ) := by
224 let f : Fin d → ℝ := fun i => Cost.Jlog (((post L k Side.credit).credit i - L.credit i : ℤ) : ℝ)
225 have hsplit :=
226 (Finset.add_sum_erase (s := (Finset.univ : Finset (Fin d))) (f := f) (a := k) (by simp))
227 have fk : f k = Cost.Jlog (1 : ℝ) := by
228 simp [f, post]
229 have hErase : Finset.sum (Finset.univ.erase k : Finset (Fin d)) f = 0 := by
230 refine Finset.sum_eq_zero ?_
231 intro i hi
232 have hik : i ≠ k := by simpa [Finset.mem_erase] using hi
233 simp [f, post, hik]
234 calc
235 (∑ i : Fin d, f i) =
236 f k + Finset.sum (Finset.univ.erase k : Finset (Fin d)) f := by
237 simpa using hsplit.symm
238 _ = Cost.Jlog (1 : ℝ) := by simp [fk, hErase]
239 simp only [ledgerJlogCost, hdeb, hcred, add_zero, zero_add]
240
241/-! ### Jlog-cost tightening: if a monotone nontrivial tick has Jlog-cost ≤ Jlog(1), it is a posting step. -/
242