isGloballyOptimal

formal source

  39
  40variable {State : Type*}
  41
  42def isGloballyOptimal (B : ChannelBundle State) (x : State) : Prop :=
  43  ∀ i, (B.channel i).isOptimal x
  44
  45end ChannelBundle
  46
  47/-- Two channels are quality-equivalent if they induce the same ordering on states. -/
  48abbrev QualityEquiv {State Obs₁ Obs₂ : Type*}
  49    (C₁ : DisplayChannel State Obs₁)
  50    (C₂ : DisplayChannel State Obs₂) : Prop :=
  51  ∀ x y : State, C₁.stateQuality x ≤ C₁.stateQuality y ↔
  52                  C₂.stateQuality x ≤ C₂.stateQuality y
  53
  54namespace QualityEquiv
  55
  56variable {State Obs₁ Obs₂ Obs₃ : Type*}
  57
  58theorem refl (C : DisplayChannel State Obs₁) : QualityEquiv C C :=
  59  fun _ _ => Iff.rfl
  60
  61theorem symm {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}
  62    (h : QualityEquiv C₁ C₂) : QualityEquiv C₂ C₁ :=
  63  fun x y => (h x y).symm
  64
  65theorem trans {C₁ : DisplayChannel State Obs₁}
  66    {C₂ : DisplayChannel State Obs₂}
  67    {C₃ : DisplayChannel State Obs₃}
  68    (h₁₂ : QualityEquiv C₁ C₂) (h₂₃ : QualityEquiv C₂ C₃) : QualityEquiv C₁ C₃ :=
  69  fun x y => (h₁₂ x y).trans (h₂₃ x y)
  70
  71/-- Quality-equivalent channels have the same optimal states. -/
  72theorem optimal_iff {C₁ : DisplayChannel State Obs₁} {C₂ : DisplayChannel State Obs₂}