channel_quality_transfer

formal source

  66/-! ## Transfer Lemmas for Channels -/
  67
  68/-- If two octaves have equivalent channels, their quality orderings agree. -/
  69theorem channel_quality_transfer
  70    {i₁ : O₁.channels.Index} {i₂ : O₂.channels.Index}
  71    (f : OctaveMorphism O₁ O₂)
  72    (hchan : ∀ x : O₁.State,
  73      (O₂.channels.channel i₂).stateQuality (f.map x) =
  74      (O₁.channels.channel i₁).stateQuality x) :
  75    ∀ x y : O₁.State,
  76      (O₁.channels.channel i₁).stateQuality x ≤
  77      (O₁.channels.channel i₁).stateQuality y →
  78      (O₂.channels.channel i₂).stateQuality (f.map x) ≤
  79      (O₂.channels.channel i₂).stateQuality (f.map y) := by
  80  intro x y hxy
  81  rw [hchan x, hchan y]
  82  exact hxy
  83
  84/-! ## The "Same Pattern, Different Scale" Principle -/
  85
  86/-- Two octaves manifest the same pattern if they're equivalent. -/
  87def samePattern (O₁ O₂ : Octave) : Prop :=
  88  Nonempty (OctaveEquiv O₁ O₂)
  89
  90theorem samePattern_refl (O : Octave) : samePattern O O :=
  91  ⟨OctaveEquiv.refl O⟩
  92
  93theorem samePattern_symm {O₁ O₂ : Octave} (h : samePattern O₁ O₂) :
  94    samePattern O₂ O₁ :=
  95  let ⟨e⟩ := h
  96  ⟨OctaveEquiv.symm e⟩
  97
  98end RRF.Theorems
  99end IndisputableMonolith