BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticCumulativeRecommendedRegret

Empirical optimistic plan built from one actual sampled-reward batch.

noncomputable def adaptiveStochasticSampledEmpiricalOptimisticPlanAt {mdp : MDP State Action} {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (round : Nat) : mdp.EstimatedModelPlan

Sum of the recommended policies' expected regrets over the sampled window.

noncomputable def adaptiveStochasticSampledEmpiricalOptimisticRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (rounds : Nat) : Real

Sum of the occupancy selected-radius bounds over the sampled window.

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

Finite summation of pointwise sampled-model optimism and regret bounds.

theorem adaptiveStochasticSampledEmpiricalOptimistic_optimism_and_cumulativeRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) (hround : forall round : Fin rounds, let plan := adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= plan.upperValueRemaining mdp.horizon le_rfl state) ∧ plan.optimisticPolicy.expectedRegret initialState <= plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState) : (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) ∧ adaptiveStochasticSampledEmpiricalOptimisticRecommendedExpectedRegret (mdp

Finite-round actual-sampled-model confidence, optimism, and cumulative recommended-policy expected regret under explicit path-support calibration.

theorem exploratorySource_trajectoryMeasure_finiteRound_allCoordinateConfidence_optimism_and_cumulativeRecommendedExpectedRegret_of_pathSupport_explicitCalibration [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) (hcontraction : (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds countDelta) visitFloor * (mdp.horizon : Real) <= 1 / 2) : let localCountDelta := multiBatchLocalDelta rounds countDelta let localRewardDelta := multiBatchLocalDelta rounds rewardDelta let rewardBudget := uniformFloorStochasticRewardCoordinateRadius mdp episodes varianceProxy localCountDelta localRewardDelta visitFloor let transitionBudget := uniformFloorStochasticTransitionBudget 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) ∧ adaptiveStochasticSampledEmpiricalOptimisticRecommendedExpectedRegret (mdp