Lean module · UCB
BanditRLProof.Algorithms.UCBArmStreamSource
# Latent arm-stream reward source for UCB peeling This module implements the pathwise reward-consumption rule used by the pinned LML UCB route. Whenever an action is selected, the observed reward is the next unused coordinate of that arm's latent stream. Consequently, the selected reward sum is exactly the stream prefix whose length is the realized pull count, so it supplies `FixedArmPrefixSource` without an extra pathwise hypothesis.
Module map
Imports
BanditRLProof.Algorithms.UCBFixedCountPeeling
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.UCB.rewardFromArmStream
Compiled
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
theorem
BanditRLProof.UCB.sumRewards_rewardFromArmStream_eq_armPrefixSum
Compiled
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)
def
BanditRLProof.UCB.fixedArmPrefixSourceOfArmStream
Compiled
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
theorem
BanditRLProof.UCB.measure_pullCount_prod_sumRewards_rewardFromArmStream_mem_le_identDistrib
Compiled
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})
def
BanditRLProof.UCB.canonicalFixedArmPrefixSource
Compiled
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)
theorem
BanditRLProof.UCB.measure_pullCount_prod_sumRewards_rewardFromCanonicalArmStream_mem_le
Compiled
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})