BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeDecayingExplorationRealizedBehaviorConsistency

The coarse bounded-return proxy is exactly the square of the batch range.

theorem batchReturnVarianceProxy_coe (mdp : MDP State Action) (episodes : Nat) : ((batchReturnVarianceProxy mdp episodes : NNReal) : Real) = ((episodes : Real) * (mdp.horizon : Real)) ^ 2

The successor-return proxy contains exactly `rounds` nonzero batch terms.

theorem cumulativeSuccessorReturnVarianceProxy_coe (mdp : MDP State Action) (episodes rounds : Nat) : ((cumulativeSuccessorReturnVarianceProxy mdp episodes rounds : NNReal) : Real) = (rounds : Real) * ((episodes : Real) * (mdp.horizon : Real)) ^ 2

Return-deviation radius after normalization by all successor episodes.

noncomputable def normalizedSuccessorReturnConfidenceRadius (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) : Real

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

theorem normalizedSuccessorReturnConfidenceRadius_nonneg (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) : 0 <= normalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta

The scheduled batch size cancels exactly from the normalized radius.

theorem normalizedSuccessorReturnConfidenceRadius_eq (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) (hepisodes : 0 < episodes) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : normalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta = (mdp.horizon : Real) * Real.sqrt (2 * Real.log (2 / delta) / (rounds : Real))

Elementary deterministic envelope for the normalized return radius.

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

The decaying schedule dominates the normalized logarithmic return radius.

theorem normalizedSuccessorReturnConfidenceRadius_le_decayingEnvelope (mdp : MDP State Action) (episodes : Nat) (n : Nat) (hepisodes : 0 < episodes) : normalizedSuccessorReturnConfidenceRadius mdp episodes (decayingExplorationRounds mdp n) (vanishingAverageConfidenceDelta n) <= decayingExplorationReturnRadiusEnvelope mdp n

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

theorem decayingExplorationScheduledEpisodes_pos (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : 0 < decayingExplorationScheduledEpisodes mdp baseVisitFloor n

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

theorem decayingExplorationReturnRadiusEnvelope_tendsto_zero (mdp : MDP State Action) : Tendsto (decayingExplorationReturnRadiusEnvelope mdp) atTop (nhds 0)

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

theorem decayingExplorationNormalizedReturnRadius_tendsto_zero (mdp : MDP State Action) (baseVisitFloor : Real) : Tendsto (fun n => normalizedSuccessorReturnConfidenceRadius mdp (decayingExplorationScheduledEpisodes mdp baseVisitFloor n) (decayingExplorationRounds mdp n) (vanishingAverageConfidenceDelta n)) atTop (nhds 0)

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

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

Count and return deviations each consume one scheduled confidence share.

noncomputable def decayingExplorationRealizedFailureBudget (n : Nat) : ENNReal

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

theorem decayingExplorationAverageRealizedBehaviorRegretBound_nonneg (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : 0 <= decayingExplorationAverageRealizedBehaviorRegretBound mdp baseVisitFloor n

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

theorem decayingExplorationAverageRealizedBehaviorRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (decayingExplorationAverageRealizedBehaviorRegretBound mdp baseVisitFloor) atTop (nhds 0)

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

theorem decayingExplorationRealizedFailureBudget_tendsto_zero : Tendsto decayingExplorationRealizedFailureBudget atTop (nhds 0)

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

theorem decayingExplorationRealizedFailureAndRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => (decayingExplorationRealizedFailureBudget n, decayingExplorationAverageRealizedBehaviorRegretBound mdp baseVisitFloor n)) atTop (nhds (0, 0))

Realized-regret violation set for one decaying-exploration window.

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

One finite window: the realized violation set is covered by the measurable count/return union, whose tail is the two-share scheduled budget.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationAverageRealizedBehaviorConsistency (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.successorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent let violationSet := decayingExplorationAverageRealizedBehaviorRegretViolationSet mdp initialState initialTable defaultState baseVisitFloor n MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n /\ violationSet ⊆ combinedBadEvent /\ source.trajectoryMeasure violationSet <= 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.decayingExplorationAverageRealizedBehaviorRegretBound mdp baseVisitFloor n

All finite windows plus the joint scalar limit. The indexed Borel witnesses make the changing sample spaces explicit and prevent a common-space reading.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_decayingExplorationAverageRealizedBehaviorConsistency_allWindows (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) : Tendsto (fun n => (AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n, AdaptiveEpisodeBatchSource.decayingExplorationAverageRealizedBehaviorRegretBound mdp baseVisitFloor n)) atTop (nhds (0, 0)) /\ forall n, letI : StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))