isOptimal

formal source

  24  C.quality ∘ C.observe
  25
  26/-- A state is optimal in channel C if it minimizes quality. -/
  27def isOptimal (C : DisplayChannel State Obs) (x : State) : Prop :=
  28  ∀ y, C.stateQuality x ≤ C.stateQuality y
  29
  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