ledgerL1Cost_eq_zero_iff

formal source

 608
 609/-! ### Zero-cost characterization -/
 610
 611theorem ledgerL1Cost_eq_zero_iff {d : Nat} (L L' : LedgerState d) :
 612    ledgerL1Cost (d := d) L L' = 0 ↔ L' = L := by
 613  classical
 614  cases L with
 615  | mk debit credit =>
 616    cases L' with
 617    | mk debit' credit' =>
 618      constructor
 619      · intro h0
 620        -- split into debit/credit sums
 621        let dSum : Nat := ∑ i : Fin d, Int.natAbs (debit' i - debit i)
 622        let cSum : Nat := ∑ i : Fin d, Int.natAbs (credit' i - credit i)
 623        have hsplit : dSum + cSum = 0 := by
 624          simpa [ledgerL1Cost, dSum, cSum] using h0
 625        have hd0 : dSum = 0 ∧ cSum = 0 := Nat.add_eq_zero_iff.mp hsplit
 626        have hdebit0 :
 627            ∀ i : Fin d, Int.natAbs (debit' i - debit i) = 0 := by
 628          have h' :
 629              Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (debit' i - debit i)) = 0 := by
 630            simpa [dSum] using hd0.1
 631          have hall :=
 632            (Finset.sum_eq_zero_iff_of_nonneg (s := (Finset.univ : Finset (Fin d)))
 633              (f := fun i => Int.natAbs (debit' i - debit i))
 634              (fun _ _ => Nat.zero_le _)).1 h'
 635          intro i
 636          exact hall i (by simp)
 637        have hcredit0 :
 638            ∀ i : Fin d, Int.natAbs (credit' i - credit i) = 0 := by
 639          have h' :
 640              Finset.sum (Finset.univ : Finset (Fin d)) (fun i => Int.natAbs (credit' i - credit i)) = 0 := by
 641            simpa [cSum] using hd0.2