BanditRLProof.Algorithms.UCBFixedCountPeeling

A table containing one infinite reward stream for every finite arm.

abbrev ArmRewardStream (K : Nat)

Sum of the first `k` rewards in one arm's stream.

def armPrefixSum {K : Nat} (arm : Fin K) (k : Nat) (stream : ArmRewardStream K) : Real

A fixed-arm prefix sum is measurable on the full stream space.

theorem measurable_armPrefixSum {K : Nat} (arm : Fin K) (k : Nat) : Measurable (armPrefixSum arm k)

Pathwise source contract behind fixed-count peeling. For each sample point, arm, and horizon, the selected reward sum must be the prefix sum of that arm's latent stream at the realized pull count.

structure FixedArmPrefixSource {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) where

The complete latent arm stream supplied by a source is measurable.

theorem FixedArmPrefixSource.measurable_armStream {Omega : Type u} {K : Nat} [MeasurableSpace Omega] {action : Omega -> ActionTrace (Fin K)} {reward : Omega -> RewardTrace Real} (source : FixedArmPrefixSource action reward) : Measurable source.armStream

Every fixed prefix sum read from a source is measurable.

theorem FixedArmPrefixSource.measurable_armPrefixSum {Omega : Type u} {K : Nat} [MeasurableSpace Omega] {action : Omega -> ActionTrace (Fin K)} {reward : Omega -> RewardTrace Real} (source : FixedArmPrefixSource action reward) (arm : Fin K) (k : Nat) : Measurable (fun omega => UCB.armPrefixSum arm k (source.armStream omega))

Pathwise fixed-count peeling. The adaptive `(pullCount, sumRewards)` event is covered by the finite union of fixed-prefix events for counts at most `n`. This is an outer-measure bound, so the event set itself need not be measurable.

theorem measure_pullCount_prod_sumRewards_mem_le_of_fixedArmPrefixSource {Omega : Type u} {K : Nat} [MeasurableSpace Omega] (mu : Measure Omega) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (source : FixedArmPrefixSource action reward) (arm : Fin K) (n : Nat) (s : Set (Nat × Real)) [DecidablePred (fun k : Nat => k ∈ Prod.fst '' s)] : mu {omega | (pullCount (action omega) arm n, sumRewards (action omega) (reward omega) arm n) ∈ s} ≤ ((Finset.range (n + 1)).filter (fun k => k ∈ Prod.fst '' s)).sum (fun k => mu {omega | UCB.armPrefixSum arm k (source.armStream omega) ∈ Prod.mk k ⁻¹' s})

Fixed-count peeling with law transport to a canonical arm-reward stream. One `IdentDistrib` hypothesis for the complete latent stream supplies every fixed-prefix law by measurable composition. This is the local counterpart of the law-transport step in LML `prob_pullCount_prod_sumRewards_mem_le`.

theorem measure_pullCount_prod_sumRewards_mem_le_of_fixedArmPrefixSource_identDistrib {Omega : Type u} {Xi : Type v} {K : Nat} [MeasurableSpace Omega] [MeasurableSpace Xi] (mu : Measure Omega) (nu : Measure Xi) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (source : FixedArmPrefixSource action reward) (canonicalStream : Xi -> ArmRewardStream K) (hstreamLaw : IdentDistrib source.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) (reward omega) arm n) ∈ s} ≤ ((Finset.range (n + 1)).filter (fun k => k ∈ Prod.fst '' s)).sum (fun k => nu {xi | UCB.armPrefixSum arm k (canonicalStream xi) ∈ Prod.mk k ⁻¹' s})