BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEpisodewiseCommonSpaceConsistency

Realized cumulative successor regret is measurable in the finite trajectory.

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

Realized average successor regret is measurable in the finite trajectory.

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

A finite sum of policy expected regrets is nonnegative.

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

The average of successor policy expected regrets is nonnegative.

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

An expected-regret upper bound and a two-sided return-deviation bound control the absolute 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 : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (expectedBound deviationBound : Real) (hexpected : source.successorExpectedAverageRegret trajectory rounds <= expectedBound) (hdeviation : |source.cumulativeSuccessorReturnDeviation rounds trajectory| <= deviationBound) : |source.realizedSuccessorAverageRegret trajectory rounds| <= expectedBound + deviationBound / ((episodes : Real) * (rounds : Real))

The sharp finite-window certificate controls the absolute realized regret, not only its upper tail. This is the finite-window input needed by convergence in probability.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationEpisodewiseAverageAbsoluteRealizedBehaviorConsistency (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] (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 initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let countBadEvent := source.adaptiveCumulativeCountBadEvent rounds delta let returnBadEvent := source.episodewiseSuccessorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ |source.realizedSuccessorAverageRegret trajectory rounds| <= AdaptiveEpisodeBatchSource.decayingExplorationEpisodewiseAverageRealizedBehaviorRegretBound mdp baseVisitFloor n

The dependent sample space containing one complete scheduled experiment per coordinate.

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

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

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

The scheduled adaptive trajectory law at common-space coordinate `n`.

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

Independent-coordinate coupling of all scheduled finite-window trajectory laws.

noncomputable def decayingExplorationEpisodewiseCommonMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) : Measure (DecayingExplorationEpisodewiseWindowSpace mdp baseVisitFloor)

Every common-space coordinate has exactly its scheduled adaptive law.

theorem decayingExplorationEpisodewiseCommonMeasure_map_eval (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor).map (fun omega => omega n) = decayingExplorationEpisodewiseWindowMeasure mdp initialState initialTable defaultState baseVisitFloor n

Scheduled realized successor-average regret as one common-space process.

noncomputable def decayingExplorationEpisodewiseRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) (omega : DecayingExplorationEpisodewiseWindowSpace mdp baseVisitFloor) : Real

Every scheduled regret coordinate is a measurable real random variable.

theorem measurable_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Measurable (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n)

Pull the sharp count/return union at coordinate `n` to the common space.

noncomputable def decayingExplorationEpisodewiseCommonBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Set (DecayingExplorationEpisodewiseWindowSpace mdp baseVisitFloor)

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

theorem decayingExplorationEpisodewiseCommonMeasure_badEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (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) : decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor (decayingExplorationEpisodewiseCommonBadEvent mdp initialState initialTable defaultState baseVisitFloor n) <= AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n

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

theorem abs_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess_le_of_not_mem_badEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (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 : DecayingExplorationEpisodewiseWindowSpace mdp baseVisitFloor) (homega : omega ∉ decayingExplorationEpisodewiseCommonBadEvent mdp initialState initialTable defaultState baseVisitFloor n) : |decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n omega| <= AdaptiveEpisodeBatchSource.decayingExplorationEpisodewiseAverageRealizedBehaviorRegretBound mdp baseVisitFloor n

Terminal common-space theorem: measurable regret coordinates, exact scheduled marginals, and convergence in probability of the process to zero.

theorem exploratorySource_decayingExplorationEpisodewiseCommonMeasure_marginals_and_realizedBehaviorRegret_tendstoInMeasure_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (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 (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n)) /\ (forall n, (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor).map (fun omega => omega n) = decayingExplorationEpisodewiseWindowMeasure mdp initialState initialTable defaultState baseVisitFloor n) /\ TendstoInMeasure (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor) (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor) atTop (fun _ => 0)