NonNeg

formal source

  34variable {State : Type*}
  35
  36/-- A strain functional is non-negative if J(x) ≥ 0 for all x. -/
  37class NonNeg (S : StrainFunctional State) : Prop where
  38  nonneg : ∀ x, 0 ≤ S.J x
  39
  40/-- A state is balanced/equilibrium if its strain is exactly zero. -/
  41def isBalanced (S : StrainFunctional State) (x : State) : Prop :=
  42  S.J x = 0
  43
  44/-- The set of equilibrium states. -/
  45def equilibria (S : StrainFunctional State) : Set State :=
  46  { x | S.isBalanced x }
  47
  48/-- A strain functional has a unique minimum if there's exactly one equilibrium. -/
  49def hasUniqueMin (S : StrainFunctional State) : Prop :=
  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