Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentRealizedBehaviorRegret
# Self-consistent-budget realized successor regret for actual sampled optimism This module replaces the coarse transition budget `rewardBound + 2 * rewardBudget` by the exact fixed point generated by a contraction coefficient `q < 1`. It retains actual sampled rewards, adaptive policy selection, three independent confidence shares, and the globally centered successor-return transport. The endpoint is fixed-window and excludes the initial batch. It does not claim an anytime, minimax, or complete UCB-VI rate; schedule-level control of the contraction, reward radius, exploration charge, and return radius remains downstream.
Module map
Imports
BanditRLProof.RL.FiniteHorizonStochasticRewardIIDSelfConsistentCalibration, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticExplicitBudgetRealizedBehaviorRegret
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentSchedule
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_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport_selfConsistentCalibration
Compiled
Finite-round actual-sampled confidence under the exact self-consistent transition budget. Every selected model is built from its observed batch.
theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport_selfConsistentCalibration [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (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) (htotal : 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) (defaultState : State) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds countDelta) < (episodes : Real) * visitFloor) (hq : uniformFloorStochasticTransitionContraction mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor < 1) : let localCountDelta := multiBatchLocalDelta rounds countDelta let localRewardDelta := multiBatchLocalDelta rounds rewardDelta let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy localCountDelta localRewardDelta visitFloor let transitionBudget := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes localCountDelta visitFloor rewardBound rewardBudget let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let event := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta MeasurableSet event ∧ source.trajectoryMeasure event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta ∧ forall trajectory, trajectory ∉ event -> forall round : Fin rounds, let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes (mdp.sampledEpisodeBatchOfStochasticTrajectories episodes (trajectory round)) defaultState rewardBudget transitionBudget (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) ∧ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_cumulativeSuccessorExploratoryBehaviorExpectedRegret_of_pathSupport_selfConsistentCalibration
Compiled
The self-consistent per-round certificate sums to the successor exploratory behavior expected-regret bound, including the explicit exploration charge.
theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_cumulativeSuccessorExploratoryBehaviorExpectedRegret_of_pathSupport_selfConsistentCalibration [StandardBorelSpace State] [StandardBorelSpace Action] {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (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) (htotal : 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) (defaultState : State) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hmargin : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds countDelta) < (episodes : Real) * visitFloor) (hq : uniformFloorStochasticTransitionContraction mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor < 1) : let localCountDelta := multiBatchLocalDelta rounds countDelta let localRewardDelta := multiBatchLocalDelta rounds rewardDelta let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy localCountDelta localRewardDelta visitFloor let transitionBudget := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes localCountDelta visitFloor rewardBound rewardBudget let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let event := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy countDelta rewardDelta MeasurableSet event ∧ source.trajectoryMeasure event <= ENNReal.ofReal countDelta + ENNReal.ofReal rewardDelta ∧ forall trajectory, trajectory ∉ event -> (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) ∧ adaptiveStochasticSampledEmpiricalOptimisticSuccessorExploratoryBehaviorExpectedRegret (mdp
def
BanditRLProof.FiniteHorizonRL.adaptiveStochasticSampledEmpiricalOptimisticSelfConsistentBudgetAverageBound
Compiled
Planning part of the self-consistent realized average-regret certificate.
noncomputable def adaptiveStochasticSampledEmpiricalOptimisticSelfConsistentBudgetAverageBound (mdp : MDP State Action) (episodes : Nat) (countDelta visitFloor : Real) (explorationRate : NNReal) (rewardBound rewardBudget : Real) : Real
theorem
BanditRLProof.FiniteHorizonRL.adaptiveStochasticSampledEmpiricalOptimistic_occupancyAndChargeAverage_eq_selfConsistentBudgetAverageBound
Compiled
The exact occupancy sum closes to the self-consistent average bound.
theorem adaptiveStochasticSampledEmpiricalOptimistic_occupancyAndChargeAverage_eq_selfConsistentBudgetAverageBound {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (countDelta visitFloor rewardBound rewardBudget : Real) (explorationRate : NNReal) (rounds : Nat) (hrounds : 0 < rounds) : (adaptiveStochasticSampledEmpiricalOptimisticOccupancyRadiusSum (mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_selfConsistentBudgetRealizedSuccessorAverageRegret_of_pathSupport_selfConsistentCalibration
Compiled
Actual sampled-model confidence and globally centered realized successor regret under the shrinking self-consistent transition budget.
theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_selfConsistentBudgetRealizedSuccessorAverageRegret_of_pathSupport_selfConsistentCalibration {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) (hq : uniformFloorStochasticTransitionContraction mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor < 1) (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 := uniformFloorStochasticSelfConsistentTransitionBudget mdp episodes localCountDelta visitFloor (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 <= adaptiveStochasticSampledEmpiricalOptimisticSelfConsistentBudgetAverageBound mdp episodes localCountDelta visitFloor explorationRate (rewardBound : Real) rewardBudget + Concentration.subGaussianSumConfidenceRadius (AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound varianceProxy) returnDelta / ((episodes : Real) * (rounds : Real))