BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticExplicitBudgetRealizedBehaviorRegret

An actual sampled empirical plan selects its two fixed model budgets.

theorem adaptiveStochasticSampledEmpiricalOptimisticPlanAt_selectedRadiusRemaining {mdp : MDP State Action} {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (round remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round).selectedRadiusRemaining remaining hremaining state = rewardBudget + transitionBudget

One sampled plan's selected-radius occupancy term has a closed form.

theorem adaptiveStochasticSampledEmpiricalOptimisticPlanAt_occupancySelectedRadiusRemaining_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (round : Nat) : let plan := adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState = (mdp.horizon : Real) * (2 * (rewardBudget + transitionBudget))

The complete actual-sampled occupancy-radius sum is deterministic.

theorem adaptiveStochasticSampledEmpiricalOptimisticOccupancyRadiusSum_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (rounds : Nat) : adaptiveStochasticSampledEmpiricalOptimisticOccupancyRadiusSum (mdp

Planning part of the calibrated realized average-regret certificate.

noncomputable def adaptiveStochasticSampledEmpiricalOptimisticExplicitBudgetAverageBound (mdp : MDP State Action) (explorationRate : NNReal) (rewardBound rewardBudget : Real) : Real

Uniform-floor budgets close the averaged occupancy and exploration charge.

theorem adaptiveStochasticSampledEmpiricalOptimistic_occupancyAndChargeAverage_eq_explicitBudgetAverageBound {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget rewardBound : Real) (explorationRate : NNReal) (rounds : Nat) (hrounds : 0 < rounds) : (adaptiveStochasticSampledEmpiricalOptimisticOccupancyRadiusSum (mdp

Actual sampled-model confidence and globally centered return concentration with a deterministic explicit-budget planning envelope.

theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_explicitBudgetRealizedSuccessorAverageRegret_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 <= adaptiveStochasticSampledEmpiricalOptimisticExplicitBudgetAverageBound mdp explorationRate (rewardBound : Real) rewardBudget + Concentration.subGaussianSumConfidenceRadius (AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound varianceProxy) returnDelta / ((episodes : Real) * (rounds : Real))