BanditRLProof.Algorithms.UCBArmStreamSource

Read the next unused latent reward of the arm selected at time `t`. The action trace may depend on the whole sample point. The coordinate index is the number of earlier selections of the currently selected arm.

def rewardFromArmStream {Omega : Type u} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) : Omega -> RewardTrace Real

Rewards consumed from one arm are exactly the prefix of that arm's latent stream whose length is the realized pull count.

theorem sumRewards_rewardFromArmStream_eq_armPrefixSum {Omega : Type u} {K : Nat} (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (omega : Omega) (arm : Fin K) (n : Nat) : sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n = armPrefixSum arm (pullCount (action omega) arm n) (armStream omega)

The next-unused-coordinate reward rule produces a fixed-arm prefix source as soon as the latent stream coordinates are measurable.

def fixedArmPrefixSourceOfArmStream {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) : FixedArmPrefixSource action (rewardFromArmStream action armStream) where

Fixed-count peeling for rewards generated by the next-unused-coordinate rule, with complete-stream law transport to a canonical stream.

theorem measure_pullCount_prod_sumRewards_rewardFromArmStream_mem_le_identDistrib {Omega : Type u} {Xi : Type v} {K : Nat} [MeasurableSpace Omega] [MeasurableSpace Xi] (mu : Measure Omega) (nu : Measure Xi) (action : Omega -> ActionTrace (Fin K)) (armStream : Omega -> ArmRewardStream K) (hmeasurable : forall i arm, Measurable (fun omega => armStream omega i arm)) (canonicalStream : Xi -> ArmRewardStream K) (hstreamLaw : IdentDistrib armStream canonicalStream mu nu) (arm : Fin K) (n : Nat) (s : Set (Nat × Real)) [DecidablePred (fun k : Nat => k ∈ Prod.fst '' s)] (hs : MeasurableSet s) : mu {omega | (pullCount (action omega) arm n, sumRewards (action omega) (rewardFromArmStream action armStream omega) arm n) ∈ s} ≤ ((Finset.range (n + 1)).filter (fun k => k ∈ Prod.fst '' s)).sum (fun k => nu {xi | armPrefixSum arm k (canonicalStream xi) ∈ Prod.mk k ⁻¹' s})

The canonical stream space supplies its own measurable latent stream.

def canonicalFixedArmPrefixSource {K : Nat} (action : ArmRewardStream K -> ActionTrace (Fin K)) : FixedArmPrefixSource action (rewardFromArmStream action id)

Pathwise peeling directly on the canonical latent stream space. This theorem is ready for any recursively defined action trace on that space; probability or stationarity assumptions enter only in later fixed-prefix tail leaves.

theorem measure_pullCount_prod_sumRewards_rewardFromCanonicalArmStream_mem_le {K : Nat} (mu : Measure (ArmRewardStream K)) (action : ArmRewardStream K -> ActionTrace (Fin K)) (arm : Fin K) (n : Nat) (s : Set (Nat × Real)) [DecidablePred (fun k : Nat => k ∈ Prod.fst '' s)] : mu {stream | (pullCount (action stream) arm n, sumRewards (action stream) (rewardFromArmStream action id stream) arm n) ∈ s} ≤ ((Finset.range (n + 1)).filter (fun k => k ∈ Prod.fst '' s)).sum (fun k => mu {stream | armPrefixSum arm k stream ∈ Prod.mk k ⁻¹' s})