BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationCommonSpaceConsistency

Stochastic realized cumulative successor regret is trajectory-measurable.

theorem measurable_realizedSuccessorCumulativeRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.realizedSuccessorCumulativeRegret trajectory rounds)

Stochastic realized average successor regret is trajectory-measurable.

theorem measurable_realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.realizedSuccessorAverageRegret trajectory rounds)

A finite sum of selected stochastic-policy expected regrets is nonnegative.

theorem successorExpectedCumulativeRegret_nonneg {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : 0 <= source.successorExpectedCumulativeRegret trajectory rounds

The average selected stochastic-policy expected regret is nonnegative.

theorem successorExpectedAverageRegret_nonneg {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : 0 <= source.successorExpectedAverageRegret trajectory rounds

An expected-regret upper bound and a two-sided global return-deviation bound control the absolute stochastic realized average regret.

theorem abs_realizedSuccessorAverageRegret_le_of_expected_le_of_deviation_abs_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (expectedBound deviationBound : Real) (hexpected : source.successorExpectedAverageRegret trajectory rounds <= expectedBound) (hdeviation : |source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory| <= deviationBound) : |source.realizedSuccessorAverageRegret trajectory rounds| <= expectedBound + deviationBound / ((episodes : Real) * (rounds : Real))

The stochastic finite-window certificate upgraded to absolute realized regret. This is the exact finite-window input consumed by convergence in probability.

theorem exploratorySource_trajectoryMeasure_projectedCumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageAbsoluteRealizedBehaviorConsistency_of_standardBorel (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let projection := MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes let countBadEvent := projectedAdaptiveCumulativeCountBadEvent (mdp := mdp) (initialState := initialState) (episodes := episodes) initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) rounds delta let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds 1 rewardVarianceProxy delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticRealizedFailureBudget n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt (projection trajectory) defaultState countRadius round ).upperValueRemaining mdp.horizon le_rfl state) /\ |source.realizedSuccessorAverageRegret trajectory rounds| <= AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n

One complete scheduled stochastic experiment at every product coordinate.

abbrev DecayingExplorationStochasticWindowSpace (mdp : MDP State Action) (baseVisitFloor : Real)

The stochastic adaptive source used at schedule coordinate `n`.

noncomputable def decayingExplorationStochasticWindowSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : AdaptiveStochasticEpisodeBatchSource mdp initialState (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n)

The scheduled stochastic trajectory law at product coordinate `n`.

noncomputable def decayingExplorationStochasticWindowMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Measure (StochasticEpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))

Independent product coupling of the complete scheduled stochastic laws.

noncomputable def decayingExplorationStochasticCommonMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) : Measure (DecayingExplorationStochasticWindowSpace mdp baseVisitFloor)

Each common-space coordinate has exactly its scheduled stochastic law.

theorem decayingExplorationStochasticCommonMeasure_map_eval (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor).map (fun omega => omega n) = decayingExplorationStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor n

Scheduled stochastic realized successor-average regret on the common space.

noncomputable def decayingExplorationStochasticRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) (omega : DecayingExplorationStochasticWindowSpace mdp baseVisitFloor) : Real

Every scheduled stochastic regret coordinate is measurable.

theorem measurable_decayingExplorationStochasticRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Measurable (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n)

Pull the finite projected-count/global-return union to the common space.

noncomputable def decayingExplorationStochasticCommonBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (rewardVarianceProxy : NNReal) (n : Nat) : Set (DecayingExplorationStochasticWindowSpace mdp baseVisitFloor)

The pulled-back stochastic bad event inherits the finite-window budget.

theorem decayingExplorationStochasticCommonMeasure_badEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor (decayingExplorationStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState baseVisitFloor rewardVarianceProxy n) <= AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticRealizedFailureBudget n

Outside the pulled-back bad event, coordinate `n` has the absolute bound.

theorem abs_decayingExplorationStochasticRealizedBehaviorRegretProcess_le_of_not_mem_badEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) (omega : DecayingExplorationStochasticWindowSpace mdp baseVisitFloor) (homega : omega ∉ decayingExplorationStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState baseVisitFloor rewardVarianceProxy n) : |decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n omega| <= AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n

Terminal theorem: exact stochastic schedule marginals and convergence in probability of realized successor-average behavior regret to zero.

theorem exploratorySource_decayingExplorationStochasticCommonMeasure_marginals_and_realizedBehaviorRegret_tendstoInMeasure_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, Measurable (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor n)) /\ (forall n, (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor).map (fun omega => omega n) = decayingExplorationStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor n) /\ TendstoInMeasure (decayingExplorationStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState baseVisitFloor) (decayingExplorationStochasticRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState baseVisitFloor) atTop (fun _ => 0)