BanditRLProof.Algorithms.UCBRealStationaryExplicitPolicy

The explicit finite-history selector encoded by the canonical arm-stream policy.

noncomputable def canonicalRealUCBHistorySelector {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (n : Nat) : History.FinitePairHistory (Fin K) Real n -> Fin K

The explicit deterministic successor-action kernel for stationary Real UCB.

noncomputable def canonicalRealUCBPolicyKernel {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (n : Nat) : Kernel (History.FinitePairHistory (Fin K) Real n) (Fin K)

The explicit canonical selector is measurable on every finite history.

theorem measurable_canonicalRealUCBHistorySelector {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (n : Nat) : Measurable (canonicalRealUCBHistorySelector hK c sigma2 n)

Every explicit policy-kernel section is the corresponding Dirac law.

theorem canonicalRealUCBPolicyKernel_apply {K : Nat} (hK : 0 < K) (c : Real) (sigma2 : NNReal) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : canonicalRealUCBPolicyKernel hK c sigma2 n history = Measure.dirac (canonicalRealUCBHistorySelector hK c sigma2 n history)

The canonical arm-stream initial-action package is the fixed initial arm.

theorem canonicalArmStreamHistoryAlgorithm_initialAction_eq_dirac {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : (canonicalArmStreamHistoryAlgorithm hK c sigma2 nu).initialAction = Measure.dirac (initializationArm hK 0)

The canonical arm-stream successor action conditional law is the explicit deterministic UCB policy kernel on its finite-history marginal.

theorem canonicalArmStreamHistoryAlgorithm_policy_ae_eq_explicitPolicyKernel {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 (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) n))) ((canonicalArmStreamHistoryAlgorithm hK c sigma2 nu).policy n) (canonicalRealUCBPolicyKernel hK c sigma2 n)

Every generated finite-pair-history marginal agrees with the corresponding canonical arm-stream history marginal.

theorem canonicalKernelTrajectory_finitePairHistory_map_eq_armStream {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Measure.map (fun trajectory => History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n) (canonicalKernelTrajectoryMeasure hK c sigma2 nu) = Measure.map (fun stream : ArmRewardStream K => History.finitePairHistoryOfTrace (armStreamAction hK (c * (sigma2 : Real)) stream) (armStreamReward hK (c * (sigma2 : Real)) stream) n) (armStreamMeasure nu)

The generated successor action conditional law is the explicit deterministic UCB policy kernel on the generated finite-history marginal.

theorem canonicalKernelTrajectoryAction_condDistrib_ae_eq_explicitPolicyKernel {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : condDistrib (fun trajectory => canonicalKernelTrajectoryAction trajectory (n + 1)) (fun trajectory => History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n) (canonicalKernelTrajectoryMeasure hK c sigma2 nu) =ᵐ[ (canonicalKernelTrajectoryMeasure hK c sigma2 nu).map (fun trajectory => History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n)] canonicalRealUCBPolicyKernel hK c sigma2 n

The generated initial action is almost surely the canonical initial arm.

theorem canonicalKernelTrajectoryAction_zero_ae_eq_initializationArm {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.EventuallyEq (ae (canonicalKernelTrajectoryMeasure hK c sigma2 nu)) (fun trajectory => canonicalKernelTrajectoryAction trajectory 0) (fun _trajectory => initializationArm hK 0)

Every generated successor action follows the explicit UCB selector a.s.

theorem canonicalKernelTrajectoryAction_succ_ae_eq_realHistoryNextArm {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : Filter.Eventually (fun trajectory => canonicalKernelTrajectoryAction trajectory (n + 1) = canonicalRealUCBHistorySelector hK c sigma2 n (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n)) (ae (canonicalKernelTrajectoryMeasure hK c sigma2 nu))

One full-measure event carries every successor explicit-policy equality.

theorem canonicalKernelTrajectoryAction_succ_ae_eq_realHistoryNextArm_all {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.Eventually (fun trajectory => forall n : Nat, canonicalKernelTrajectoryAction trajectory (n + 1) = canonicalRealUCBHistorySelector hK c sigma2 n (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n)) (ae (canonicalKernelTrajectoryMeasure hK c sigma2 nu))

The complete generated action trace follows the explicit UCB policy a.s.

theorem canonicalKernelTrajectoryAction_follows_realHistoryNextArm_ae {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Filter.Eventually (fun trajectory => canonicalKernelTrajectoryAction trajectory 0 = initializationArm hK 0 /\ forall n : Nat, canonicalKernelTrajectoryAction trajectory (n + 1) = canonicalRealUCBHistorySelector hK c sigma2 n (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n)) (ae (canonicalKernelTrajectoryMeasure hK c sigma2 nu))

Armwise-bounded finite-arm laws give one fixed generated process whose actions follow explicit Real UCB almost surely and whose expected average pseudo-regret tends to zero.

theorem canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero_and_explicitPolicy {K : Nat} [NeZero K] (hK : 0 < K) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) (lo hi : Fin K -> Real) (hbound : forall arm, Filter.Eventually (fun x : Real => Set.Icc (lo arm) (hi arm) x) (ae (armLaw arm))) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm)) Tendsto (realStationaryArmwiseBoundedFiniteArmExpectedAverageRegret (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob) armLaw canonicalKernelTrajectoryAction) atTop (nhds 0) /\ Filter.Eventually (fun trajectory => canonicalKernelTrajectoryAction trajectory 0 = initializationArm hK 0 /\ forall n : Nat, canonicalKernelTrajectoryAction trajectory (n + 1) = realHistoryNextArm hK (4 * (sigma2 : Real)) n (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n)) (ae (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob))