BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationConsistency

One-episode proxy underlying the globally centered stochastic batch proxy.

noncomputable def globalReturnDeviationPerEpisodeVarianceProxy (mdp : MDP State Action) (rewardBound rewardVarianceProxy : NNReal) : NNReal

The honest global iid proxy is exactly episode-linear.

theorem iidGlobalSampledCumulativeReturnDeviationVarianceProxy_eq (mdp : MDP State Action) (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : mdp.iidGlobalSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy = (episodes : NNReal) * mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy

Positive horizon and positive reward bound make the per-episode proxy positive.

theorem globalReturnDeviationPerEpisodeVarianceProxy_pos (mdp : MDP State Action) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : 0 < rewardBound) (hhorizon : 0 < mdp.horizon) : 0 < mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy

The successor proxy is exactly rounds times episodes times one base proxy.

theorem cumulativeSuccessorGlobalReturnVarianceProxy_coe (mdp : MDP State Action) (rounds episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : ((cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real) = (rounds : Real) * (episodes : Real) * (mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy : Real)

Globally centered stochastic return radius normalized by all successor samples.

noncomputable def normalizedSuccessorGlobalReturnConfidenceRadius (mdp : MDP State Action) (episodes rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_nonneg (mdp : MDP State Action) (episodes rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : 0 <= normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy delta

Exact normalized-radius formula after exposing episode and round scaling.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_eq (mdp : MDP State Action) (episodes rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) (hepisodes : 0 < episodes) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds rewardBound rewardVarianceProxy delta = Real.sqrt (2 * (mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy : Real) * Real.log (2 / delta) / ((episodes : Real) * (rounds : Real)))

A simple inverse-scale envelope for the scheduled stochastic radius.

noncomputable def decayingExplorationStochasticReturnRadiusEnvelope (mdp : MDP State Action) (rewardBound rewardVarianceProxy : NNReal) (n : Nat) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_le_decayingEnvelope (mdp : MDP State Action) (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) (n : Nat) (hepisodes : 0 < episodes) : normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) rewardBound rewardVarianceProxy (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n) <= decayingExplorationStochasticReturnRadiusEnvelope mdp rewardBound rewardVarianceProxy n

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationStochasticReturnRadiusEnvelope_tendsto_zero (mdp : MDP State Action) (rewardBound rewardVarianceProxy : NNReal) : Tendsto (decayingExplorationStochasticReturnRadiusEnvelope mdp rewardBound rewardVarianceProxy) atTop (nhds 0)

The exact scheduled stochastic return radius tends to zero.

theorem decayingExplorationNormalizedSuccessorGlobalReturnRadius_tendsto_zero (mdp : MDP State Action) (baseVisitFloor : Real) (rewardBound rewardVarianceProxy : NNReal) : Tendsto (fun n => normalizedSuccessorGlobalReturnConfidenceRadius mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n) (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) rewardBound rewardVarianceProxy (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)) atTop (nhds 0)

Stochastic realized-behavior certificate at schedule index `n`.

noncomputable def decayingExplorationStochasticAverageRealizedBehaviorRegretBound (mdp : MDP State Action) (baseVisitFloor : Real) (rewardVarianceProxy : NNReal) (n : Nat) : Real

Projected-count and stochastic-return deviations consume one share each.

noncomputable def decayingExplorationStochasticRealizedFailureBudget (n : Nat) : ENNReal

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationStochasticAverageRealizedBehaviorRegretBound_nonneg (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (rewardVarianceProxy : NNReal) (n : Nat) : 0 <= decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationStochasticAverageRealizedBehaviorRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (rewardVarianceProxy : NNReal) : Tendsto (decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy) atTop (nhds 0)

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationStochasticRealizedFailureBudget_tendsto_zero : Tendsto decayingExplorationStochasticRealizedFailureBudget atTop (nhds 0)

No declaration docstring is present; use the chapter context and exact statement below.

theorem decayingExplorationStochasticRealizedFailureAndRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (rewardVarianceProxy : NNReal) : Tendsto (fun n => (decayingExplorationStochasticRealizedFailureBudget n, decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n)) atTop (nhds (0, 0))

Stochastic-reward lift of the cumulative empirical-optimistic exploratory source. The cumulative table selector is evaluated only on projected history.

noncomputable def exploratorySource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes where

The initial policies of the stochastic lift and deterministic source agree.

theorem exploratorySource_initialPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).initialPolicy = (AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).initialPolicy

Every stochastic successor policy is the deterministic projected policy.

theorem exploratorySource_successorPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).successorPolicy n history = (AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).successorPolicy n (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n history)

The initial stochastic batch maps to the deterministic cumulative fiber.

theorem exploratorySource_initialBatch_map_knownRewardEpisodeBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : (rewardSource.iidStochasticTrajectoryFamilyMeasure (exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).initialPolicy initialState episodes).map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp := mdp) episodes) = (AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).initialPolicy.iidEpisodeBatchMeasure initialState episodes

Every selected stochastic successor batch maps to its deterministic fiber.

theorem exploratorySource_batchKernel_map_knownRewardEpisodeBatch {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : ((exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).batchKernel n history).map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp := mdp) episodes) = (AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).batchKernel n (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n history)

Projected prefix and next-batch joint law of the cumulative source.

theorem exploratorySource_trajectoryMeasure_map_projectedPrefix_next_eq_compProd {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate let deterministicSource := AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate stochasticSource.trajectoryMeasure.map (fun trajectory => (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n (Preorder.frestrictLe n trajectory), MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp := mdp) episodes (trajectory (n + 1)))) = stochasticSource.trajectoryMeasure.map (fun trajectory => MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n (Preorder.frestrictLe n trajectory)) ⊗ₘ deterministicSource.batchKernel n

Conditional projected next-batch law for the cumulative source.

theorem exploratorySource_trajectoryMeasure_condDistrib_projectedNext {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate let deterministicSource := AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate ProbabilityTheory.condDistrib (fun trajectory : StochasticEpisodeBatchTrajectory mdp episodes => MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatch (mdp := mdp) episodes (trajectory (n + 1))) (fun trajectory : StochasticEpisodeBatchTrajectory mdp episodes => MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n (Preorder.frestrictLe n trajectory)) stochasticSource.trajectoryMeasure =ᵐ[ stochasticSource.trajectoryMeasure.map (fun trajectory => MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchPrefix (mdp := mdp) episodes n (Preorder.frestrictLe n trajectory))] deterministicSource.batchKernel n

The complete known-reward projection equals the deterministic source law.

theorem exploratorySource_trajectoryMeasure_map_knownRewardEpisodeBatchTrajectory {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : let stochasticSource := exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate let deterministicSource := AdaptiveCumulativeEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate stochasticSource.trajectoryMeasure.map (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes) = deterministicSource.trajectoryMeasure

Pullback of the deterministic cumulative count event.

def projectedAdaptiveCumulativeCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (delta : Real) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

Stochastic successor expected regret is the projected cumulative quantity.

theorem exploratorySource_successorExpectedCumulativeRegret_eq_projected {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).successorExpectedCumulativeRegret trajectory rounds = adaptiveCumulativeEmpiricalOptimisticExploratoryBehaviorExpectedRegret (initialState := initialState) (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes trajectory) defaultState countRadius explorationRate hexplorationRate rounds

Average stochastic successor expected regret is the projected average.

theorem exploratorySource_successorExpectedAverageRegret_eq_projected {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate hexplorationRate).successorExpectedAverageRegret trajectory rounds = adaptiveCumulativeEmpiricalOptimisticAverageExploratoryBehaviorExpectedRegret (initialState := initialState) (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes trajectory) defaultState countRadius explorationRate hexplorationRate rounds

The projected stochastic source inherits the deterministic decaying count, optimism, and expected exploratory-behavior certificate for one window.

theorem exploratorySource_trajectoryMeasure_projectedCumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageExploratoryBehaviorExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [Nonempty (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] (rewardSource : mdp.MeanCompatibleRewardKernel) (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 MeasurableSet countBadEvent /\ source.trajectoryMeasure countBadEvent <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ countBadEvent -> (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.successorExpectedAverageRegret trajectory rounds <= AdaptiveEpisodeBatchSource.decayingExplorationAverageExploratoryBehaviorExpectedRegretBound mdp baseVisitFloor n

Stochastic realized-regret violation set for one scheduled window.

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

One stochastic finite window: projected counts and globally centered returns cover the realized-regret violation set under the two-share scheduled budget.

theorem exploratorySource_trajectoryMeasure_projectedCumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageRealizedBehaviorConsistency (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [Nonempty (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (StochasticEpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [Nonempty (StochasticEpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))] (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 let violationSet := decayingExplorationAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState baseVisitFloor rewardVarianceProxy n MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticRealizedFailureBudget n /\ violationSet ⊆ combinedBadEvent /\ source.trajectoryMeasure violationSet <= 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

All scheduled stochastic windows plus the joint scalar limit. The indexed Borel witnesses expose the changing deterministic and stochastic sample spaces.

theorem exploratorySource_trajectoryMeasure_projectedCumulativeInverseSqrtPathSupport_decayingExplorationAverageRealizedBehaviorConsistency_allWindows (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (hdetBatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (hdetTrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (hstochasticBatchBorel : forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (hstochasticTrajectoryBorel : forall n, StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (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) : Tendsto (fun n => (AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticRealizedFailureBudget n, AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n)) atTop (nhds (0, 0)) /\ forall n, letI : StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))