BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtAverageRate

Total exploratory episodes in `rounds` batches of size `episodes`.

def cumulativeExploratoryEpisodeCount (episodes rounds : Nat) : Nat

The normalized cumulative recommendation-regret bound per recommendation.

noncomputable def normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound (mdp : MDP State Action) (episodes rounds : Nat) (delta visitFloor : Real) : Real

The normalized average bound exposes the square-root rate in the total number of exploratory episodes.

theorem normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound_eq_totalEpisodes (mdp : MDP State Action) {episodes rounds : Nat} (hepisodes : 0 < episodes) (hrounds : 0 < rounds) (delta : Real) {visitFloor : Real} (hvisitFloor : 0 < visitFloor) : normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp episodes rounds delta visitFloor = 2 * (mdp.horizon : Real) * min 1 (8 * (Fintype.card State : Real) * (mdp.horizon : Real) * Real.sqrt (cumulativeInverseSqrtLogFactor mdp rounds delta) / Real.sqrt visitFloor / Real.sqrt ((cumulativeExploratoryEpisodeCount episodes rounds : Nat) * visitFloor / 2))

Average expected regret of the cumulative empirical recommendations.

noncomputable def adaptiveCumulativeEmpiricalOptimisticAverageRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (rounds : Nat) : Real

Normalized average-recommendation endpoint expressed through all exploratory episodes, with the exact parent event and optimism conclusion unchanged.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_normalizedAverageRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate MeasurableSet (source.adaptiveCumulativeCountBadEvent rounds delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent rounds delta) <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ source.adaptiveCumulativeCountBadEvent rounds delta -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticAverageRecommendedExpectedRegret (initialState := initialState) trajectory defaultState countRadius rounds <= AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp episodes rounds delta visitFloor