ChannelBundle

formal source

  30end DisplayChannel
  31
  32/-- A collection of display channels on the same state space. -/
  33structure ChannelBundle (State : Type*) where
  34  Index : Type*
  35  Obs : Index → Type*
  36  channel : (i : Index) → DisplayChannel State (Obs i)
  37
  38namespace ChannelBundle
  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