Lean module · UCB
BanditRLProof.Algorithms.UCBRealStationarySelectedRewardConsistency
# Selected reward laws and consistency for canonical stationary UCB This module transports the stationary selected-reward laws from the latent arm-stream process to the independently regenerated canonical kernel trajectory, then pairs those laws with the compiled explicit-policy expected-average result.
Module map
Imports
BanditRLProof.Algorithms.UCBArmStreamConditionalReward
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.UCB.canonicalKernelTrajectory_historyAction_map_eq_armStream
Compiled
The generated history/action condition marginal agrees with its canonical arm-stream counterpart.
theorem canonicalKernelTrajectory_historyAction_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, canonicalKernelTrajectoryAction trajectory (n + 1))) (canonicalKernelTrajectoryMeasure hK c sigma2 nu) = Measure.map (armStreamHistoryAction hK (c * (sigma2 : Real)) n) (armStreamMeasure nu)
theorem
BanditRLProof.UCB.canonicalKernelTrajectoryReward_zero_condDistrib_ae_eq_nu
Compiled
The generated initial reward has the stationary law of its selected arm.
theorem canonicalKernelTrajectoryReward_zero_condDistrib_ae_eq_nu {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] : condDistrib (fun trajectory => canonicalKernelTrajectoryReward trajectory 0) (fun trajectory => canonicalKernelTrajectoryAction trajectory 0) (canonicalKernelTrajectoryMeasure hK c sigma2 nu) =ᵐ[ (canonicalKernelTrajectoryMeasure hK c sigma2 nu).map (fun trajectory => canonicalKernelTrajectoryAction trajectory 0)] nu
theorem
BanditRLProof.UCB.canonicalKernelTrajectoryReward_succ_condDistrib_ae_eq_nu
Compiled
Every generated successor reward has the stationary law of the selected arm.
theorem canonicalKernelTrajectoryReward_succ_condDistrib_ae_eq_nu {K : Nat} [NeZero K] (hK : 0 < K) (c : Real) (sigma2 : NNReal) (nu : Kernel (Fin K) Real) [IsMarkovKernel nu] (n : Nat) : condDistrib (fun trajectory => canonicalKernelTrajectoryReward trajectory (n + 1)) (fun trajectory => (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n, canonicalKernelTrajectoryAction trajectory (n + 1))) (canonicalKernelTrajectoryMeasure hK c sigma2 nu) =ᵐ[ (canonicalKernelTrajectoryMeasure hK c sigma2 nu).map (fun trajectory => (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n, canonicalKernelTrajectoryAction trajectory (n + 1)))] armStreamSelectedRewardKernel n nu
theorem
BanditRLProof.UCB.canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero_and_explicitPolicy_and_selectedRewardLaws
Compiled
The fresh canonical trajectory simultaneously exposes its stationary selected reward laws, explicit UCB policy graph, and expected-average consistency.
theorem canonicalKernelTrajectoryArmwiseBoundedFiniteArmExpectedAverageRegret_tendsto_zero_and_explicitPolicy_and_selectedRewardLaws {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)) let nu := finiteArmRealRewardKernel armLaw 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)) /\ condDistrib (fun trajectory => canonicalKernelTrajectoryReward trajectory 0) (fun trajectory => canonicalKernelTrajectoryAction trajectory 0) (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob) =ᵐ[ (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob).map (fun trajectory => canonicalKernelTrajectoryAction trajectory 0)] nu /\ forall n : Nat, condDistrib (fun trajectory => canonicalKernelTrajectoryReward trajectory (n + 1)) (fun trajectory => (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n, canonicalKernelTrajectoryAction trajectory (n + 1))) (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob) =ᵐ[ (finiteArmCanonicalKernelTrajectoryMeasure hK 4 sigma2 armLaw hprob).map (fun trajectory => (History.finitePairHistoryOfTrace (canonicalKernelTrajectoryAction trajectory) (canonicalKernelTrajectoryReward trajectory) n, canonicalKernelTrajectoryAction trajectory (n + 1)))] armStreamSelectedRewardKernel n nu