BanditRLProof.Algorithms.UCBArmStreamConditionalReward

A flattened pull-index/arm coordinate of a latent arm-reward stream.

def armStreamCoordinate {K : Nat} (index : Nat × Fin K) : ArmRewardStream K -> Real

The latent arm stream with one specified coordinate omitted.

def armStreamWithoutCoordinate {K : Nat} (target : Nat × Fin K) : ArmRewardStream K -> ({index : Nat × Fin K // index ≠ target} -> Real)

Reconstruct a latent arm stream after supplying one omitted coordinate.

def armStreamInsertCoordinate {K : Nat} (target : Nat × Fin K) (value : Real) : ({index : Nat × Fin K // index ≠ target} -> Real) -> ArmRewardStream K

The history/action condition used by the successor reward kernel.

noncomputable def armStreamHistoryAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : ArmRewardStream K -> History.FinitePairHistory (Fin K) Real n × Fin K

The next unused pull-index/arm coordinate selected after history `n`.

noncomputable def armStreamNextCoordinate {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : ArmRewardStream K -> Nat × Fin K

The pull-index/arm coordinate encoded by a successor history/action condition.

noncomputable def armStreamCoordinateOfHistoryAction {K : Nat} (n : Nat) : History.FinitePairHistory (Fin K) Real n × Fin K -> Nat × Fin K

Conditions that encode one fixed next pull-index/arm coordinate.

def armStreamHistoryActionCoordinateBranch {K : Nat} (n : Nat) (target : Nat × Fin K) : Set (History.FinitePairHistory (Fin K) Real n × Fin K)

The stationary reward kernel selected by the arm component of a condition.

noncomputable abbrev armStreamSelectedRewardKernel {K : Nat} (n : Nat) (nu : Kernel (Fin K) Real) : Kernel (History.FinitePairHistory (Fin K) Real n × Fin K) Real

Latent streams for which one fixed pull-index/arm coordinate is selected next.

def armStreamNextCoordinateBranch {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) : Set (ArmRewardStream K)

Reconstructed successor condition using only a fixed coordinate's complement.

noncomputable def armStreamHistoryActionFromWithout {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) : ({index : Nat × Fin K // index ≠ target} -> Real) -> History.FinitePairHistory (Fin K) Real n × Fin K

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

theorem measurable_armStreamCoordinate {K : Nat} (index : Nat × Fin K) : Measurable (armStreamCoordinate index)

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

theorem measurable_armStreamWithoutCoordinate {K : Nat} (target : Nat × Fin K) : Measurable (armStreamWithoutCoordinate target)

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

theorem measurable_armStreamInsertCoordinate {K : Nat} (target : Nat × Fin K) (value : Real) : Measurable (armStreamInsertCoordinate target value)

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

theorem armStreamWithoutCoordinate_insertCoordinate {K : Nat} (target : Nat × Fin K) (value : Real) (rest : {index : Nat × Fin K // index ≠ target} -> Real) : armStreamWithoutCoordinate target (armStreamInsertCoordinate target value rest) = rest

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

theorem measurable_armStreamHistoryAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Measurable (armStreamHistoryAction hK c n)

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

theorem measurable_armStreamNextCoordinate {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Measurable (armStreamNextCoordinate hK c n)

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

theorem measurable_armStreamCoordinateOfHistoryAction {K : Nat} (n : Nat) : Measurable (armStreamCoordinateOfHistoryAction (K := K) n)

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

theorem measurableSet_armStreamHistoryActionCoordinateBranch {K : Nat} (n : Nat) (target : Nat × Fin K) : MeasurableSet (armStreamHistoryActionCoordinateBranch n target)

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

theorem measurableSet_armStreamNextCoordinateBranch {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) : MeasurableSet (armStreamNextCoordinateBranch hK c n target)

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

theorem armStreamNextCoordinate_eq_coordinateOfHistoryAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (stream : ArmRewardStream K) : armStreamNextCoordinate hK c n stream = armStreamCoordinateOfHistoryAction n (armStreamHistoryAction hK c n stream)

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

theorem pairwise_disjoint_armStreamHistoryActionCoordinateBranch {K : Nat} (n : Nat) : Pairwise (Function.onFun (fun s t : Set (History.FinitePairHistory (Fin K) Real n × Fin K) => Disjoint s t) (fun target : Nat × Fin K => armStreamHistoryActionCoordinateBranch n target))

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

theorem pairwise_disjoint_armStreamNextCoordinateBranch {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Pairwise (Function.onFun (fun s t : Set (ArmRewardStream K) => Disjoint s t) (fun target : Nat × Fin K => armStreamNextCoordinateBranch hK c n target))

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

theorem iUnion_armStreamHistoryActionCoordinateBranch {K : Nat} (n : Nat) : (⋃ target : Nat × Fin K, armStreamHistoryActionCoordinateBranch n target) = Set.univ

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

theorem iUnion_armStreamNextCoordinateBranch {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : (⋃ target : Nat × Fin K, armStreamNextCoordinateBranch hK c n target) = Set.univ

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

theorem measure_eq_sum_restrict_armStreamHistoryActionCoordinateBranch {K : Nat} (n : Nat) (mu : Measure (History.FinitePairHistory (Fin K) Real n × Fin K)) : mu = Measure.sum fun target : Nat × Fin K => mu.restrict (armStreamHistoryActionCoordinateBranch n target)

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

theorem armStreamMeasure_eq_sum_restrict_nextCoordinateBranch {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : armStreamMeasure nu = Measure.sum fun target : Nat × Fin K => (armStreamMeasure nu).restrict (armStreamNextCoordinateBranch hK c n target)

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

theorem measurable_armStreamHistoryActionFromWithout {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) : Measurable (armStreamHistoryActionFromWithout hK c n target value)

The first component of the next coordinate is the selected arm's current count.

theorem armStreamNextCoordinate_fst_eq_pullCount {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) : (armStreamNextCoordinate hK c n stream).1 = pullCount (armStreamAction hK c stream) (armStreamNextCoordinate hK c n stream).2 (n + 1)

The successor reward reads exactly the next coordinate selected after history `n`.

theorem armStreamReward_succ_eq_nextCoordinate {K : Nat} (hK : 0 < K) (c : Real) (stream : ArmRewardStream K) (n : Nat) : armStreamReward hK c stream (n + 1) = armStreamCoordinate (armStreamNextCoordinate hK c n stream) stream

The recursive history through `n` only reads coordinates whose pull index is strictly below the corresponding arm count at time `n + 1`.

theorem armStreamHistory_eq_of_eq_below_pullCount {K : Nat} (hK : 0 < K) (c : Real) (stream stream' : ArmRewardStream K) (n : Nat) (hagrees : ∀ arm index, index < pullCount (armStreamAction hK c stream) arm (n + 1) → stream index arm = stream' index arm) : armStreamHistory hK c stream n = armStreamHistory hK c stream' n

Changing one not-yet-consumed coordinate cannot alter the history already generated from the latent stream.

theorem armStreamHistory_eq_of_withoutCoordinate_eq_of_pullCount_le {K : Nat} (hK : 0 < K) (c : Real) (target : Nat × Fin K) (stream stream' : ArmRewardStream K) (n : Nat) (hwithout : armStreamWithoutCoordinate target stream = armStreamWithoutCoordinate target stream') (hfuture : pullCount (armStreamAction hK c stream) target.2 (n + 1) ≤ target.1) : armStreamHistory hK c stream n = armStreamHistory hK c stream' n

The event that a fixed coordinate is selected next factors through the stream with that coordinate omitted.

theorem armStreamNextCoordinate_eq_iff_insertCoordinate {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) (stream : ArmRewardStream K) : armStreamNextCoordinate hK c n stream = target ↔ armStreamNextCoordinate hK c n (armStreamInsertCoordinate target value (armStreamWithoutCoordinate target stream)) = target

On the branch selecting `target`, the actual successor condition equals its reconstruction from all coordinates except `target`.

theorem armStreamHistoryAction_eq_fromWithout_of_nextCoordinate_eq {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) (stream : ArmRewardStream K) (hnext : armStreamNextCoordinate hK c n stream = target) : armStreamHistoryAction hK c n stream = armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream)

All pull-index/arm coordinates are mutually independent.

theorem iIndepFun_armStreamMeasure_coordinate {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : iIndepFun (fun index : Nat × Fin K => armStreamCoordinate index) (armStreamMeasure nu)

A fixed coordinate is independent of the collection of all other coordinates.

theorem indepFun_armStreamMeasure_coordinate_without {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) : IndepFun (armStreamCoordinate target) (armStreamWithoutCoordinate target) (armStreamMeasure nu)

A fixed reward coordinate is independent of the reconstructed successor condition.

theorem indepFun_armStreamMeasure_coordinate_historyActionFromWithout {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) (value : Real) : IndepFun (armStreamCoordinate target) (fun stream : ArmRewardStream K => armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream)) (armStreamMeasure nu)

The reconstructed successor condition and a fixed omitted coordinate have a product joint law, with the prescribed arm marginal on the reward coordinate.

theorem armStreamMeasure_map_historyActionFromWithout_coordinate_eq_prod {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) (value : Real) : Measure.map (fun stream : ArmRewardStream K => (armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream), armStreamCoordinate target stream)) (armStreamMeasure nu) = (Measure.map (fun stream : ArmRewardStream K => armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream)) (armStreamMeasure nu)).prod (nu target.2)

The reconstructed condition is in `target`'s branch exactly on the actual branch.

theorem armStreamHistoryActionFromWithout_mem_coordinateBranch_iff {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) (stream : ArmRewardStream K) : armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream) ∈ armStreamHistoryActionCoordinateBranch n target ↔ stream ∈ armStreamNextCoordinateBranch hK c n target

Both actual and reconstructed condition maps induce the same branch restriction.

theorem map_historyActionFromWithout_restrict_coordinateBranch_eq_historyAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (target : Nat × Fin K) (value : Real) (mu : Measure (ArmRewardStream K)) : (Measure.map (fun stream : ArmRewardStream K => armStreamHistoryActionFromWithout hK c n target value (armStreamWithoutCoordinate target stream)) mu).restrict (armStreamHistoryActionCoordinateBranch n target) = (Measure.map (armStreamHistoryAction hK c n) mu).restrict (armStreamHistoryActionCoordinateBranch n target)

On one fixed next-coordinate branch, the actual successor condition/reward pair has the restricted condition marginal times the prescribed arm law.

theorem armStreamMeasure_map_historyAction_reward_restrict_branch_eq_prod {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) (value : Real) : Measure.map (fun stream : ArmRewardStream K => (armStreamHistoryAction hK c n stream, armStreamReward hK c stream (n + 1))) ((armStreamMeasure nu).restrict (armStreamNextCoordinateBranch hK c n target)) = ((Measure.map (armStreamHistoryAction hK c n) (armStreamMeasure nu)).restrict (armStreamHistoryActionCoordinateBranch n target)).prod (nu target.2)

The full successor condition/reward joint law is the condition marginal followed by the stationary law of the arm selected in that condition.

theorem armStreamMeasure_map_historyAction_reward_succ_eq_compProd {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure.map (fun stream : ArmRewardStream K => (armStreamHistoryAction hK c n stream, armStreamReward hK c stream (n + 1))) (armStreamMeasure nu) = Measure.compProd (Measure.map (armStreamHistoryAction hK c n) (armStreamMeasure nu)) (armStreamSelectedRewardKernel n nu)

The successor arm-stream reward conditional law is the selected arm law.

theorem armStreamReward_succ_condDistrib_ae_eq_nu {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.EventuallyEq (ae ((armStreamMeasure nu).map (armStreamHistoryAction hK c n))) (condDistrib (fun stream : ArmRewardStream K => armStreamReward hK c stream (n + 1)) (armStreamHistoryAction hK c n) (armStreamMeasure nu)) (armStreamSelectedRewardKernel n nu)

The packaged canonical successor-feedback kernel is the stationary selected law.

theorem canonicalArmStreamHistoryEnvironment_feedback_ae_eq_nu {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Filter.EventuallyEq (ae ((armStreamMeasure nu).map (armStreamHistoryAction hK (c * (sigma2 : Real)) n))) ((canonicalArmStreamHistoryEnvironment hK c sigma2 nu).feedback n) (armStreamSelectedRewardKernel n nu)

Given every other latent coordinate, a fixed coordinate still has its prescribed stationary arm law.

theorem armStreamMeasure_condDistrib_coordinate_given_without {K : Nat} (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (target : Nat × Fin K) : Filter.EventuallyEq (ae ((armStreamMeasure nu).map (armStreamWithoutCoordinate target))) (condDistrib (armStreamCoordinate target) (armStreamWithoutCoordinate target) (armStreamMeasure nu)) (Kernel.const _ (nu target.2))

The initial arm-stream reward conditional law is the selected arm law.

theorem armStreamReward_zero_condDistrib_ae_eq_nu {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.EventuallyEq (ae ((armStreamMeasure nu).map (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0))) (condDistrib (fun stream : ArmRewardStream K => armStreamReward hK (c * (sigma2 : Real)) stream 0) (fun stream : ArmRewardStream K => armStreamAction hK (c * (sigma2 : Real)) stream 0) (armStreamMeasure nu)) nu

The packaged canonical initial-feedback kernel is the stationary selected law.

theorem canonicalArmStreamHistoryEnvironment_initialFeedback_ae_eq_nu {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.EventuallyEq (ae ((canonicalArmStreamHistoryAlgorithm hK c sigma2 nu).initialAction)) (canonicalArmStreamHistoryEnvironment hK c sigma2 nu).initialFeedback nu