isMinimizer

formal source

  58  S.J x ≤ S.J y
  59
  60/-- A state x is a minimizer if no state is strictly better. -/
  61def isMinimizer (S : StrainFunctional State) (x : State) : Prop :=
  62  ∀ y, S.weaklyBetter x y
  63
  64/-- For non-negative strain, equilibria are minimizers. -/
  65theorem equilibria_are_minimizers [NonNeg S] (x : State) (hx : S.isBalanced x) :
  66    S.isMinimizer x := by
  67  intro y
  68  simp only [weaklyBetter, isBalanced] at *
  69  rw [hx]
  70  exact NonNeg.nonneg y
  71
  72end StrainFunctional
  73
  74/-- A ledger constraint: the sum of debits equals the sum of credits. -/
  75structure LedgerConstraint (State : Type*) where
  76  /-- Total debit for a state. -/
  77  debit : State → ℤ
  78  /-- Total credit for a state. -/
  79  credit : State → ℤ
  80
  81namespace LedgerConstraint
  82
  83variable {State : Type*}
  84
  85/-- A state satisfies the ledger constraint if debit = credit. -/
  86def isClosed (L : LedgerConstraint State) (x : State) : Prop :=
  87  L.debit x = L.credit x
  88
  89/-- The net balance (should be zero for closed ledgers). -/
  90def net (L : LedgerConstraint State) (x : State) : ℤ :=
  91  L.debit x - L.credit x