preserves_equilibria

formal source

  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) :
  78    O₂.strain.isBalanced (f.map x) := by
  79  simp only [StrainFunctional.isBalanced] at *
  80  rw [hx] at hf
  81  have h₁ := @StrainFunctional.NonNeg.nonneg _ O₂.strain inst (f.map x)
  82  linarith
  83
  84end OctaveMorphism
  85
  86/-- Two octaves are equivalent if there exist mutually inverse morphisms
  87    that both preserve strain exactly (isometric in both directions). -/
  88structure OctaveEquiv (O₁ O₂ : Octave) where
  89  /-- Forward morphism. -/
  90  toFun : OctaveMorphism O₁ O₂
  91  /-- Backward morphism. -/
  92  invFun : OctaveMorphism O₂ O₁
  93  /-- Strain is preserved exactly (forward isometry). -/
  94  strain_eq : ∀ x, O₂.strain.J (toFun.map x) = O₁.strain.J x
  95  /-- Strain is preserved exactly (inverse isometry). -/
  96  strain_eq_inv : ∀ y, O₁.strain.J (invFun.map y) = O₂.strain.J y
  97
  98namespace OctaveEquiv
  99
 100/-- Reflexivity. -/
 101def refl (O : Octave) : OctaveEquiv O O where
 102  toFun := OctaveMorphism.id O
 103  invFun := OctaveMorphism.id O