BanditRLProof.Algorithms.UCBArmStreamProcess

Round-robin arm at an absolute time coordinate.

def initializationArm {K : Nat} (hK : 0 < K) (t : Nat) : Fin K

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

theorem initializationArm_zero {K : Nat} (hK : 0 < K) : initializationArm hK 0 = Fin.mk 0 hK

LML-shaped next action after an inclusive history through time `n`. The first `K` actions are round robin. Once that prefix is complete, the native Real UCB history index selects a least-encoded maximizing arm.

noncomputable def realHistoryNextArm {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Fin K

The next-arm selector is measurable on the finite history space.

theorem measurable_realHistoryNextArm {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => realHistoryNextArm hK c n history)

Joint evaluation of an arm stream at countable random coordinates.

theorem measurable_armRewardStream_apply {K : Nat} : Measurable (fun input : ArmRewardStream K × (Nat × Fin K) => input.1 input.2.1 input.2.2)

Inclusive pair history of the deterministic UCB process driven by a latent arm-reward stream.

noncomputable def armStreamHistory {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) : (n : Nat) -> History.FinitePairHistory (Fin K) Real n | 0 => let arm := initializationArm hK 0 fun _ => (arm, stream 0 arm) | n + 1 => let history := armStreamHistory hK c stream n let arm := realHistoryNextArm hK c n history let count := ETC.realHistoryPullCount n history arm History.extendPairHistorySucc history (arm, stream count arm) /-- Action trace extracted from the recursive inclusive histories. -/ noncomputable def armStreamAction {K : Nat} (hK : 0 < K) (c : Real) : ArmRewardStream K -> ActionTrace (Fin K)

Action trace extracted from the recursive inclusive histories.

noncomputable def armStreamAction {K : Nat} (hK : 0 < K) (c : Real) : ArmRewardStream K -> ActionTrace (Fin K)

Reward trace obtained by reading each selected arm's next unused value.

noncomputable def armStreamReward {K : Nat} (hK : 0 < K) (c : Real) : ArmRewardStream K -> RewardTrace Real

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

theorem armStreamAction_zero {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) : armStreamAction hK c stream 0 = initializationArm hK 0

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

theorem armStreamAction_succ {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) : armStreamAction hK c stream (n + 1) = realHistoryNextArm hK c n (armStreamHistory hK c stream n)

The recursively maintained history is exactly the finite pair history of the extracted action and next-unused-coordinate reward traces.

theorem armStreamHistory_eq_finitePairHistoryOfTrace {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) : armStreamHistory hK c stream n = History.finitePairHistoryOfTrace (armStreamAction hK c stream) (armStreamReward hK c stream) n

Every recursively generated inclusive history is measurable in the stream.

theorem measurable_armStreamHistory {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Measurable (fun stream : ArmRewardStream K => armStreamHistory hK c stream n)

Every action coordinate of the recursive arm-stream process is measurable.

theorem measurable_armStreamAction {K : Nat} (hK : 0 < K) (c : Real) (t : Nat) : Measurable (fun stream : ArmRewardStream K => armStreamAction hK c stream t)

Every reward coordinate of the recursive arm-stream process is measurable.

theorem measurable_armStreamReward {K : Nat} (hK : 0 < K) (c : Real) (t : Nat) : Measurable (fun stream : ArmRewardStream K => armStreamReward hK c stream t)

The action after time `n` is the LML-shaped selector on its actual history.

theorem armStreamAction_succ_eq_realHistoryNextArm_actualHistory {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) : armStreamAction hK c stream (n + 1) = realHistoryNextArm hK c n (History.finitePairHistoryOfTrace (armStreamAction hK c stream) (armStreamReward hK c stream) n)

After initialization, the generated action is the native Real UCB index action.

theorem armStreamAction_succ_eq_realHistoryIndexAction_of_not_lt {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) (hn : ¬ n < K - 1) : armStreamAction hK c stream (n + 1) = realHistoryIndexAction hK c n (History.finitePairHistoryOfTrace (armStreamAction hK c stream) (armStreamReward hK c stream) n)

The recursive process satisfies the fixed-arm latent-prefix source.

noncomputable def armStreamUCBFixedArmPrefixSource {K : Nat} (hK : 0 < K) (c : Real) : FixedArmPrefixSource (armStreamAction hK c) (armStreamReward hK c)

Stationary product law: one independent time stream for every arm law.

noncomputable def armStreamMeasure {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure (ArmRewardStream K)

Fixed-count peeling for the actual recursive UCB process under the stationary product arm-stream law.

theorem measure_pullCount_prod_sumRewards_armStreamUCB_mem_le {K : Nat} (hK : 0 < K) (c : Real) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (arm : Fin K) (n : Nat) (s : Set (Nat × Real)) [DecidablePred (fun k : Nat => k ∈ Prod.fst '' s)] : armStreamMeasure nu {stream | (pullCount (armStreamAction hK c stream) arm n, sumRewards (armStreamAction hK c stream) (armStreamReward hK c stream) arm n) ∈ s} ≤ ((Finset.range (n + 1)).filter (fun k => k ∈ Prod.fst '' s)).sum (fun k => armStreamMeasure nu {stream | armPrefixSum arm k stream ∈ Prod.mk k ⁻¹' s})