wellPosed

formal source

  44def equilibria : Set O.State := O.strain.equilibria
  45
  46/-- An octave is well-posed if it has at least one equilibrium. -/
  47def wellPosed : Prop := ∃ x : O.State, O.strain.isBalanced x
  48
  49end Octave
  50
  51/-- A morphism between octaves: a map that preserves strain ordering. -/
  52structure OctaveMorphism (O₁ O₂ : Octave) where
  53  /-- The underlying map on states. -/
  54  map : O₁.State → O₂.State
  55  /-- The map preserves strain ordering. -/
  56  preserves_order : ∀ x y, O₁.strain.weaklyBetter x y →
  57                           O₂.strain.weaklyBetter (map x) (map y)
  58
  59namespace OctaveMorphism
  60
  61/-- Identity morphism. -/
  62def id (O : Octave) : OctaveMorphism O O where
  63  map := fun x => x
  64  preserves_order := fun _ _ h => h
  65
  66/-- Composition of morphisms. -/
  67def comp {O₁ O₂ O₃ : Octave}
  68    (g : OctaveMorphism O₂ O₃) (f : OctaveMorphism O₁ O₂) : OctaveMorphism O₁ O₃ where
  69  map := g.map ∘ f.map
  70  preserves_order := fun x y h => g.preserves_order _ _ (f.preserves_order x y h)
  71
  72/-- Morphisms preserve equilibria (if target has NonNeg strain). -/
  73theorem preserves_equilibria {O₁ O₂ : Octave}
  74    [inst : StrainFunctional.NonNeg O₂.strain]
  75    (f : OctaveMorphism O₁ O₂)
  76    (x : O₁.State) (hx : O₁.strain.isBalanced x)
  77    (hf : O₂.strain.J (f.map x) ≤ O₁.strain.J x) :