BanditRLProof.DelayedFeedback.Processing

Feedback source rounds that are available before action `t` but have not yet been processed. This is the set-level content of Algorithm 5's `B(t) \ S`; the source sequence order remains a later algorithm-state choice.

def newlyObservedBefore (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) : Finset Nat

Strictly available feedback remains available at every later action round.

theorem observedBefore_mono (delay : Nat → Nat) {t u : Nat} (htu : t ≤ u) : observedBefore delay t ⊆ observedBefore delay u

A source round is never both already processed and newly observed.

theorem processed_disjoint_newlyObservedBefore (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) : Disjoint processed (newlyObservedBefore delay processed t)

If all processed rounds were legitimately available, adjoining every new arrival yields exactly the current available set.

theorem processed_union_newlyObservedBefore (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) (hprocessed : processed ⊆ observedBefore delay t) : processed ∪ newlyObservedBefore delay processed t = observedBefore delay t

The update obtained by processing every currently new arrival is the current available set.

def processAllNew (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) : Finset Nat

No declaration docstring is present; use the chapter context and exact statement below.

theorem processAllNew_eq_observedBefore (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) (hprocessed : processed ⊆ observedBefore delay t) : processAllNew delay processed t = observedBefore delay t

A completed earlier available set is a valid processed prefix later.

theorem previousObservedBefore_subset_current (delay : Nat → Nat) {t u : Nat} (htu : t ≤ u) : observedBefore delay t ⊆ observedBefore delay u

Starting from the fully processed set at an earlier round and processing all arrivals through a later round yields exactly the later available set.

theorem processAllNew_from_previous_eq_current (delay : Nat → Nat) {t u : Nat} (htu : t ≤ u) : processAllNew delay (observedBefore delay t) u = observedBefore delay u

Outstanding feedback cannot appear in the newly observed batch at the same action time.

theorem outstandingAt_disjoint_newlyObservedBefore (delay : Nat → Nat) (processed : Finset Nat) (t : Nat) : Disjoint (outstandingAt delay t) (newlyObservedBefore delay processed t)