Lean module · UCB
BanditRLProof.Algorithms.UCBRealLMLCompat
# Native Real UCB LML field compatibility surface The pinned LML source currently uses a newer Lean/mathlib toolchain, so ABRL cannot import its `IsAlgEnvSeq` declaration directly. This module packages the exact measurable action/feedback and split conditional-law consequences used by the local UCB trajectory and regret route. It is a local compatibility structure, not an imported LML proof.
Module map
Imports
BanditRLProof.Algorithms.UCBArmStreamExpectedPullCount
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCBRealStationaryFiniteArmRewardLaws
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
structure
BanditRLProof.UCB.RealStationaryUCBSequence
Compiled
The exact `IsAlgEnvSeq`-shaped fields consumed by the local stationary Real UCB route. The law fields correspond to the pinned source's initial action law, initial feedback law, successor action law given finite observable history, and successor feedback law given history and the new action. They are stated as Mathlib `condDistrib` equalities because LML's `HasCondDistrib` symbol is not a local dependency.
structure RealStationaryUCBSequence {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) : Prop where
theorem
BanditRLProof.UCB.realStationaryUCBSequence_armStream
Compiled
The canonical arm-stream process satisfies the local UCB field bundle.
theorem realStationaryUCBSequence_armStream {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : RealStationaryUCBSequence (armStreamMeasure nu) hK c sigma2 nu (armStreamAction hK (c * (sigma2 : Real))) (armStreamReward hK (c * (sigma2 : Real)))
theorem
BanditRLProof.UCB.identDistrib_actionRewardTrace_of_realStationaryUCBSequence
Compiled
The complete external observable trajectory has the canonical arm-stream UCB law whenever the local stationary sequence field bundle holds.
theorem identDistrib_actionRewardTrace_of_realStationaryUCBSequence {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (h : RealStationaryUCBSequence mu hK c sigma2 nu action reward) : IdentDistrib (fun omega t => (action omega t, reward omega t)) (fun stream t => (armStreamAction hK (c * (sigma2 : Real)) stream t, armStreamReward hK (c * (sigma2 : Real)) stream t)) mu (armStreamMeasure nu)
theorem
BanditRLProof.UCB.regret_le_of_realStationaryUCBSequence
Compiled
Exact native Real UCB regret from the bundled stationary sequence fields. This is the local theorem corresponding to the mathematical route of pinned LML `Bandits.UCB.regret_le`. A theorem about the imported LML `IsAlgEnvSeq` symbol still requires a common Lean/mathlib toolchain.
theorem regret_le_of_realStationaryUCBSequence {Omega : Type u} {K : Nat} [NeZero K] [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (h : RealStationaryUCBSequence mu hK c sigma2 nu action reward) (n : Nat) (hc : 0 < c) (hsigma2 : sigma2 ≠ 0) (hsubG : forall arm : Fin K, HasSubgaussianMGF (fun x => x - realKernelMean nu arm) sigma2 (nu arm)) : integral mu (fun omega => realKernelRegret nu (action omega) n) <= (Finset.univ : Finset (Fin K)).sum (fun arm => 8 * c * (sigma2 : Real) * Real.log ((n + 1 : Nat) : Real) / realKernelGap nu arm + realKernelGap nu arm * (2 + 2 * (constSum c n).toReal))