BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · UCB

BanditRLProof.Algorithms.UCBRealStationaryCanonicalKernelTrajectory

# Canonical-kernel trajectory source for stationary UCB This module packages the canonical arm-stream UCB split conditional laws as a history algorithm and environment, then independently regenerates their observable action/reward pair process with Mathlib's Ionescu-Tulcea `Kernel.trajMeasure`. The resulting coordinate process supplies every field of `RealStationaryUCBSequence` without a caller-provided sample space or law.

Module map

Declarations
9
Placeholders
0

Imports

BanditRLProof.Algorithms.ThompsonCanonicalTrajectory, BanditRLProof.Algorithms.UCBRealStationaryFiniteArmRewardLaws

Imported by

BanditRLProof, BanditRLProof.Algorithms.UCBRealStationaryExplicitPolicy

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.UCB.canonicalArmStreamHistoryAlgorithm Compiled

Canonical arm-stream initial and successor action laws as a history algorithm.

noncomputable def canonicalArmStreamHistoryAlgorithm {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Thompson.HistoryAlgorithm (Fin K) Real where
Source line 22 Chapter context: UCB
def BanditRLProof.UCB.canonicalArmStreamHistoryEnvironment Compiled

Canonical arm-stream initial and successor reward laws as a history environment.

noncomputable def canonicalArmStreamHistoryEnvironment {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Thompson.HistoryEnvironment (Fin K) Real where
Source line 43 Chapter context: UCB
def BanditRLProof.UCB.canonicalKernelTrajectoryMeasure Compiled

Independently regenerated pair trajectory from the canonical UCB split kernels.

noncomputable def canonicalKernelTrajectoryMeasure {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : Measure ((n : Nat) -> Fin K × Real)
Source line 65 Chapter context: UCB
def BanditRLProof.UCB.finiteArmCanonicalKernelTrajectoryMeasure Compiled

Finite-arm-law specialization of the canonical-kernel trajectory measure.

noncomputable def finiteArmCanonicalKernelTrajectoryMeasure {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (armLaw : Fin K -> Measure Real) (hprob : forall arm, IsProbabilityMeasure (armLaw arm)) : Measure ((n : Nat) -> Fin K × Real)
Source line 84 Chapter context: UCB
def BanditRLProof.UCB.canonicalKernelTrajectoryAction Compiled

Action coordinates of the canonical-kernel pair trajectory.

def canonicalKernelTrajectoryAction {K : Nat} : ((n : Nat) -> Fin K × Real) -> ActionTrace (Fin K)
Source line 109 Chapter context: UCB
def BanditRLProof.UCB.canonicalKernelTrajectoryReward Compiled

Reward coordinates of the canonical-kernel pair trajectory.

def canonicalKernelTrajectoryReward {K : Nat} : ((n : Nat) -> Fin K × Real) -> RewardTrace Real
Source line 114 Chapter context: UCB
theorem BanditRLProof.UCB.realStationaryUCBSequence_canonicalKernelTrajectory Compiled

The independently generated canonical-kernel trajectory satisfies all local stationary UCB split conditional-law fields.

theorem realStationaryUCBSequence_canonicalKernelTrajectory {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : RealStationaryUCBSequence (canonicalKernelTrajectoryMeasure hK c sigma2 nu) hK c sigma2 nu canonicalKernelTrajectoryAction canonicalKernelTrajectoryReward
Source line 122 Chapter context: UCB
theorem BanditRLProof.UCB.canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le Compiled

Armwise-bounded laws give the logarithmic expected-regret envelope on the independently regenerated canonical-kernel trajectory.

theorem canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le {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))) (n : Nat) : let sigma2 := Concentration.finiteArmPositiveVarianceProxy (fun arm => Concentration.intervalVarianceProxy (lo arm) (hi arm)) 0 <= realStationaryArmwiseBoundedFiniteArmExpectedRegret (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob) armLaw canonicalKernelTrajectoryAction n /\ realStationaryArmwiseBoundedFiniteArmExpectedRegret (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob) armLaw canonicalKernelTrajectoryAction n <= realStationaryArmwiseBoundedFiniteArmModelCoefficient armLaw hprob lo hi * (1 + Real.log ((n + 1 : Nat) : Real))
Source line 168 Chapter context: UCB
theorem BanditRLProof.UCB.canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero Compiled

The expected regret per round of the independently regenerated canonical-kernel UCB trajectory tends to zero.

theorem canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero {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)
Source line 218 Chapter context: UCB