strictlyBetter

formal source

  50  ∃! x, S.isBalanced x
  51
  52/-- Strict improvement: x is strictly better than y. -/
  53def strictlyBetter (S : StrainFunctional State) (x y : State) : Prop :=
  54  S.J x < S.J y
  55
  56/-- Weak improvement: x is at least as good as y. -/
  57def weaklyBetter (S : StrainFunctional State) (x y : State) : Prop :=
  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*}