BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentExplicitRate

Three times the compiled contraction envelope controls the fixed-point budget.

noncomputable def selfConsistentScheduledTransitionBudgetRateEnvelope (mdp : MDP State Action) (n : Nat) : Real

The explicit transition-budget envelope is `12 * |State| * horizon / scale^2`.

theorem selfConsistentScheduledTransitionBudgetRateEnvelope_eq (mdp : MDP State Action) (n : Nat) : selfConsistentScheduledTransitionBudgetRateEnvelope mdp n = (12 * (Fintype.card State : Real) * (mdp.horizon : Real)) / (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2

The exact fixed-point transition budget has an explicit scale-squared rate.

theorem selfConsistentScheduledTransitionBudget_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledTransitionBudgetRateEnvelope mdp n

Explicit planning envelope: scale-squared model error plus the exploration charge.

noncomputable def selfConsistentScheduledPlanningAverageRegretRateEnvelope (mdp : MDP State Action) (n : Nat) : Real

The scheduled planning certificate is bounded by the explicit rate envelope.

theorem selfConsistentScheduledPlanningAverageRegretBound_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledPlanningAverageRegretBound mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledPlanningAverageRegretRateEnvelope mdp n

Closed full realized-rate envelope, including the global return fluctuation.

noncomputable def selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : Real

The original realized-regret certificate is bounded by the closed rate envelope.

theorem selfConsistentScheduledRealizedSuccessorAverageRegretBound_le_rateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledRealizedSuccessorAverageRegretBound mdp varianceProxy baseVisitFloor n <= selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n

The three confidence shares equal the explicit `3 / (n + 2)` envelope.

noncomputable def selfConsistentScheduledRealizedFailureRateEnvelope (n : Nat) : ENNReal

The old three-share budget is exactly the explicit failure-rate envelope.

theorem selfConsistentScheduledRealizedFailureBudget_eq_rateEnvelope (n : Nat) : selfConsistentScheduledRealizedFailureBudget n = selfConsistentScheduledRealizedFailureRateEnvelope n

The explicit planning-rate envelope tends to zero.

theorem selfConsistentScheduledPlanningAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledPlanningAverageRegretRateEnvelope mdp) atTop (nhds 0)

The full explicit realized-regret envelope tends to zero.

theorem selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy) atTop (nhds 0)

The explicit `3 / (n + 2)` failure envelope tends to zero.

theorem selfConsistentScheduledRealizedFailureRateEnvelope_tendsto_zero : Tendsto selfConsistentScheduledRealizedFailureRateEnvelope atTop (nhds 0)

Explicit failure and realized-regret rates vanish jointly.

theorem selfConsistentScheduledExplicitRateEnvelopes_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (fun n => (selfConsistentScheduledRealizedFailureRateEnvelope n, selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n)) atTop (nhds (0, 0))

Actual-sampled optimism and realized regret with explicit finite-window rates.

theorem exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret (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