DisplayChannel

formal source

  11namespace RRF.Core
  12
  13/-- A display channel from State to Observation. -/
  14structure DisplayChannel (State Obs : Type*) where
  15  observe : State → Obs
  16  quality : Obs → ℝ
  17
  18namespace DisplayChannel
  19
  20variable {State Obs : Type*}
  21
  22/-- The composed quality function: State → ℝ. -/
  23def stateQuality (C : DisplayChannel State Obs) : State → ℝ :=
  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