Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticRealizedBehaviorRegret
# Realized successor regret for actual sampled empirical optimism This module combines the actual sampled-model confidence and exploratory successor-policy route with the existing globally centered stochastic return tail. Model count, model reward, and realized-return failures retain three separate confidence shares. The result covers successor batches `1..rounds`; the initial batch and explicit occupancy-radius rates remain downstream.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticCumulativeExploratoryBehaviorRegret, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticRealizedBehaviorRegret
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticExplicitBudgetRealizedBehaviorRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_successorExpectedCumulativeRegret_eq_sampledPlanExploratoryBehaviorExpectedRegret
Compiled
The generic source cumulative expected regret is the named sampled-plan sum.
theorem exploratorySource_successorExpectedCumulativeRegret_eq_sampledPlanExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate).successorExpectedCumulativeRegret trajectory rounds = adaptiveStochasticSampledEmpiricalOptimisticSuccessorExploratoryBehaviorExpectedRegret (mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_successorExpectedAverageRegret_eq_sampledPlanExploratoryBehaviorExpectedRegret
Compiled
Average form of the exact sampled-plan successor-policy identity.
theorem exploratorySource_successorExpectedAverageRegret_eq_sampledPlanExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate).successorExpectedAverageRegret trajectory rounds = adaptiveStochasticSampledEmpiricalOptimisticSuccessorExploratoryBehaviorExpectedRegret (mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret_of_pathSupport_explicitCalibration
Compiled
Concrete three-share fixed-window endpoint for actual sampled-model planning and realized successor behavior regret.
theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret_of_pathSupport_explicitCalibration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (hmodelTotal : 0 < ((((episodes : NNReal) * varianceProxy : NNReal) : Real))) (countDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (rewardDelta : Real) (hrewardDelta : 0 < rewardDelta) (hrewardDelta_le_one : rewardDelta <= 1) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) (defaultState : State) (rewardBound : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds countDelta) < (episodes : Real) * visitFloor) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor * (mdp.horizon : Real) <= 1 / 2) (hreturnTotal : 0 < ((AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound varianceProxy : NNReal) : Real)) : let localCountDelta := multiBatchLocalDelta rounds countDelta let localRewardDelta := multiBatchLocalDelta rounds rewardDelta let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy localCountDelta localRewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget (rewardBound : Real) rewardBudget let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let modelBadEvent := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds rewardBound varianceProxy returnDelta let combinedBadEvent := modelBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent ∧ source.trajectoryMeasure combinedBadEvent <= (ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta) + ENNReal.ofReal returnDelta ∧ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round).upperValueRemaining mdp.horizon le_rfl state) ∧ source.realizedSuccessorAverageRegret trajectory rounds <= (adaptiveStochasticSampledEmpiricalOptimisticOccupancyRadiusSum (mdp