BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCommonSpaceConsistency

Actual-sampled optimism and an absolute realized-regret explicit rate.

theorem exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_absoluteRealizedSuccessorAverageRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (n : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (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 episodes := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let rewardBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor n let transitionBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor n let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let modelBadEvent := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy delta delta let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds 1 varianceProxy delta let combinedBadEvent := modelBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (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) /\ |source.realizedSuccessorAverageRegret trajectory rounds| <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n

One complete actual-sampled self-consistent experiment at each coordinate.

abbrev SelfConsistentScheduledStochasticWindowSpace (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real)

The actual-sampled self-consistent source at schedule coordinate `n`.

noncomputable def selfConsistentScheduledStochasticWindowSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : AdaptiveStochasticEpisodeBatchSource mdp initialState (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n)

The actual-sampled self-consistent trajectory law at coordinate `n`.

noncomputable def selfConsistentScheduledStochasticWindowMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Measure (StochasticEpisodeBatchTrajectory mdp (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n))

Independent product coupling of the complete self-consistent window laws.

noncomputable def selfConsistentScheduledStochasticCommonMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : Measure (SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor)

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

theorem selfConsistentScheduledStochasticCommonMeasure_map_eval (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).map (fun omega => omega n) = selfConsistentScheduledStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n

Scheduled actual-sampled realized successor-average regret.

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

Every coordinate of the scheduled actual-sampled regret is measurable.

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

Pull the model/global-return union at coordinate `n` to the common space.

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

The pulled-back bad event inherits the explicit finite-window failure rate.

theorem selfConsistentScheduledStochasticCommonMeasure_badEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (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) : selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope n

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

theorem abs_selfConsistentScheduledStochasticRealizedRegretProcess_le_of_not_mem_badEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (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 : SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor) (homega : omega ∉ selfConsistentScheduledStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) : |selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n omega| <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n

Terminal theorem: exact scheduled marginals and convergence in probability of actual-sampled realized successor-average regret to zero.

theorem exploratorySource_selfConsistentScheduledStochasticCommonMeasure_marginals_and_realizedRegret_tendstoInMeasure_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (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 (selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)) /\ (forall n, (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ).map (fun omega => omega n) = selfConsistentScheduledStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) /\ TendstoInMeasure (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)