BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentSchedule

Explicit episode threshold making the normalized count radius smaller than `scale⁻²`.

noncomputable def selfConsistentCountShrinkEpisodeThreshold (mdp : MDP State Action) (rounds : Nat) (delta visitFloor scale : Real) : Real

Explicit episode threshold making the uniform sampled-reward radius smaller than `scale⁻²`.

noncomputable def selfConsistentRewardShrinkEpisodeThreshold (mdp : MDP State Action) (rounds : Nat) (varianceProxy : NNReal) (delta visitFloor scale : Real) : Real

The count threshold gives a scale-squared normalized count-radius bound.

theorem simultaneousCountConfidenceRadius_lt_episodes_mul_visitFloor_div_scale_sq_of_threshold (mdp : MDP State Action) {rounds episodes : Nat} {delta visitFloor scale : Real} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hscale : 0 < scale) (hthreshold : selfConsistentCountShrinkEpisodeThreshold mdp rounds delta visitFloor scale < (episodes : Real)) : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor / scale ^ 2

The reward threshold gives a half-scale-squared sampled-reward-sum bound.

theorem simultaneousRewardSumConfidenceRadius_lt_episodes_mul_visitFloor_div_two_scale_sq_of_threshold (mdp : MDP State Action) {rounds episodes : Nat} (varianceProxy : NNReal) {delta visitFloor scale : Real} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hscale : 0 < scale) (hthreshold : selfConsistentRewardShrinkEpisodeThreshold mdp rounds varianceProxy delta visitFloor scale < (episodes : Real)) : MDP.MeanCompatibleRewardKernel.simultaneousRewardSumConfidenceRadius mdp episodes varianceProxy (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor / (2 * scale ^ 2)

Maximum of calibration, count-shrinkage, and reward-shrinkage thresholds.

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

Positive natural episode count one step above the explicit maximum threshold.

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

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

theorem selfConsistentScheduledEpisodes_pos (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : 0 < selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n

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

theorem selfConsistentScheduledEpisodeThreshold_lt_episodes (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : selfConsistentScheduledEpisodeThreshold mdp varianceProxy baseVisitFloor n < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real)

The scheduled episode count strictly exceeds the path-calibration threshold.

theorem exploratoryPathCalibrationEpisodeThreshold_lt_selfConsistentScheduledEpisodes (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : exploratoryPathCalibrationEpisodeThreshold mdp (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n) (AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real)

The scheduled episode count strictly exceeds the count-shrink threshold.

theorem selfConsistentCountShrinkEpisodeThreshold_lt_scheduledEpisodes (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : selfConsistentCountShrinkEpisodeThreshold mdp (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n) (AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n) (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real)

The scheduled episode count strictly exceeds the sampled-reward shrink threshold.

theorem selfConsistentRewardShrinkEpisodeThreshold_lt_scheduledEpisodes (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : selfConsistentRewardShrinkEpisodeThreshold mdp (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) varianceProxy (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n) (AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n) (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real)

The explicit schedule discharges the strict count margin and half contraction.

theorem selfConsistentScheduled_countMargin_and_halfContraction (mdp : MDP State Action) (witnessState : State) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : simultaneousCountConfidenceRadius mdp (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) (multiBatchLocalDelta (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real) * AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n /\ uniformFloorStochasticTransitionContraction mdp (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) (multiBatchLocalDelta (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)) (AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n) <= 1 / 2

Shared per-round confidence share for the self-consistent schedule.

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

Actual sampled-reward coordinate budget under the explicit schedule.

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

Actual transition contraction under the explicit schedule.

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

Exact fixed-point transition budget under the explicit schedule.

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

Scheduled count confidence is smaller than visit mass divided by `scale^2`.

theorem selfConsistentScheduledCountRadius_lt_mass_div_scale_sq (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : simultaneousCountConfidenceRadius mdp (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) (selfConsistentScheduledLocalDelta mdp n) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real) * AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n / (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2

Scheduled reward-sum confidence is smaller than visit mass divided by `2*scale^2`.

theorem selfConsistentScheduledRewardSumRadius_lt_mass_div_two_scale_sq (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : MDP.MeanCompatibleRewardKernel.simultaneousRewardSumConfidenceRadius mdp (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) varianceProxy (selfConsistentScheduledLocalDelta mdp n) < (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n : Real) * AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n / (2 * (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2)

A simple deterministic envelope for the scheduled transition contraction.

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

The scheduled sampled-reward budget is nonnegative.

theorem selfConsistentScheduledRewardBudget_nonneg (mdp : MDP State Action) (witnessState : State) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : 0 <= selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor n

The scheduled sampled-reward budget is strictly below `scale^-2`.

theorem selfConsistentScheduledRewardBudget_lt_inv_scale_sq (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor n < 1 / (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2

The scheduled transition contraction is nonnegative.

theorem selfConsistentScheduledTransitionContraction_nonneg (mdp : MDP State Action) (witnessState : State) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : 0 <= selfConsistentScheduledTransitionContraction mdp varianceProxy baseVisitFloor n

The scheduled transition contraction is bounded by its `scale^-2` envelope.

theorem selfConsistentScheduledTransitionContraction_lt_envelope (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledTransitionContraction mdp varianceProxy baseVisitFloor n < selfConsistentScheduledTransitionContractionEnvelope mdp n

The calibration half bound makes the scheduled contraction strictly smaller than one.

theorem selfConsistentScheduledTransitionContraction_lt_one (mdp : MDP State Action) (witnessState : State) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledTransitionContraction mdp varianceProxy baseVisitFloor n < 1

The exact scheduled transition budget is nonnegative.

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

The square of the decaying-exploration scale tends to infinity.

theorem decayingExplorationScale_sq_tendsto_atTop : Tendsto (fun n : Nat => (AdaptiveEpisodeBatchSource.decayingExplorationScale n : Real) ^ 2) atTop atTop

The deterministic contraction envelope tends to zero.

theorem selfConsistentScheduledTransitionContractionEnvelope_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledTransitionContractionEnvelope mdp) atTop (nhds 0)

The actual scheduled sampled-reward budget tends to zero.

theorem selfConsistentScheduledRewardBudget_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor) atTop (nhds 0)

The actual scheduled transition contraction tends to zero.

theorem selfConsistentScheduledTransitionContraction_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledTransitionContraction mdp varianceProxy baseVisitFloor) atTop (nhds 0)

The exact fixed-point transition budget tends to zero with its contraction.

theorem selfConsistentScheduledTransitionBudget_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Planning part of the scheduled self-consistent realized certificate.

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

Full realized successor-average regret bound under the explicit schedule.

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

Count, reward, and globally centered return events each consume one share.

noncomputable def selfConsistentScheduledRealizedFailureBudget (n : Nat) : ENNReal

The scheduled planning average-regret bound tends to zero.

theorem selfConsistentScheduledPlanningAverageRegretBound_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledPlanningAverageRegretBound mdp varianceProxy baseVisitFloor) atTop (nhds 0)

The scheduled globally centered return radius tends to zero.

theorem selfConsistentScheduledNormalizedSuccessorGlobalReturnRadius_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (fun n => normalizedSuccessorGlobalReturnConfidenceRadius mdp (selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) (AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n) 1 varianceProxy (AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n)) atTop (nhds 0)

The full scheduled realized successor-average bound tends to zero.

theorem selfConsistentScheduledRealizedSuccessorAverageRegretBound_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (selfConsistentScheduledRealizedSuccessorAverageRegretBound mdp varianceProxy baseVisitFloor) atTop (nhds 0)

The three-share failure budget tends to zero.

theorem selfConsistentScheduledRealizedFailureBudget_tendsto_zero : Tendsto selfConsistentScheduledRealizedFailureBudget atTop (nhds 0)

Failure probability and realized-regret certificates vanish together.

theorem selfConsistentScheduledFailureAndRealizedBound_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => (selfConsistentScheduledRealizedFailureBudget n, selfConsistentScheduledRealizedSuccessorAverageRegretBound mdp varianceProxy baseVisitFloor n)) atTop (nhds (0, 0))

At every schedule index, actual sampled count/reward confidence, optimism, and globally centered realized successor-average regret hold outside three finite bad-event shares. The episode and trajectory spaces may change with `n`.

theorem exploratorySource_trajectoryMeasure_selfConsistentScheduled_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 visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let localDelta := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp 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.selfConsistentScheduledRealizedFailureBudget 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.selfConsistentScheduledRealizedSuccessorAverageRegretBound mdp varianceProxy baseVisitFloor n