Lean module · UCB

BanditRLProof.Algorithms.UCBRealStationaryCanonicalKernelTrajectory

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

Source: BanditRLProof/Algorithms/UCBRealStationaryCanonicalKernelTrajectory.lean
Teaching chapter: 4. UCB: confidence events to regret
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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalArmStreamHistoryAlgorithm

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalArmStreamHistoryEnvironment

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalKernelTrajectoryMeasure

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.finiteArmCanonicalKernelTrajectoryMeasure

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalKernelTrajectoryAction

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalKernelTrajectoryReward

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.realStationaryUCBSequence_canonicalKernelTrajectory

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedRegret_nonneg_and_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

4. UCB: confidence events to regret

Canonical node identity

declaration:BanditRLProof.UCB.canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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