BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtHighProbabilityAverageConsistency

The confidence budget used at finite window `n`.

noncomputable def vanishingAverageConfidenceDelta (n : Nat) : Real

The scheduled batch size at finite window `n`, with `n + 1` rounds.

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

The finite-window average recommendation-regret certificate.

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

Every confidence budget in the schedule is strictly positive.

theorem vanishingAverageConfidenceDelta_pos (n : Nat) : 0 < vanishingAverageConfidenceDelta n

Every confidence budget in the schedule is at most one.

theorem vanishingAverageConfidenceDelta_le_one (n : Nat) : vanishingAverageConfidenceDelta n <= 1

The real-valued confidence budget tends to zero.

theorem vanishingAverageConfidenceDelta_tendsto_zero : Tendsto vanishingAverageConfidenceDelta atTop (nhds 0)

The `ENNReal` failure budget used by measure bounds tends to zero.

theorem vanishingAverageConfidenceDelta_ennreal_tendsto_zero : Tendsto (fun n => ENNReal.ofReal (vanishingAverageConfidenceDelta n)) atTop (nhds 0)

The varying-delta finite-window certificate is nonnegative.

theorem vanishingDeltaScheduledAverageBound_nonneg (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (n : Nat) {visitFloor : Real} (hvisitFloor : 0 < visitFloor) : 0 <= vanishingDeltaScheduledAverageRecommendedExpectedRegretBound mdp n visitFloor

The varying-delta certificate is controlled by the same pure rate.

theorem vanishingDeltaScheduledAverageBound_le_envelope (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (n : Nat) {visitFloor : Real} (hvisitFloor : 0 < visitFloor) : vanishingDeltaScheduledAverageRecommendedExpectedRegretBound mdp n visitFloor <= normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp (n + 1) visitFloor

The varying-delta average recommendation-regret certificate tends to zero.

theorem vanishingDeltaScheduledAverageBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) : Tendsto (fun n => vanishingDeltaScheduledAverageRecommendedExpectedRegretBound mdp n visitFloor) atTop (nhds 0)

Failure budget and deterministic certificate jointly tend to `(0, 0)`.

theorem vanishingDeltaAndScheduledAverageBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) : Tendsto (fun n => (ENNReal.ofReal (vanishingAverageConfidenceDelta n), vanishingDeltaScheduledAverageRecommendedExpectedRegretBound mdp n visitFloor)) atTop (nhds (0, 0))

The trajectories whose average recommendation-regret exceeds the vanishing-delta finite-window certificate.

noncomputable def vanishingDeltaScheduledAverageRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (n : Nat) (visitFloor : Real) : Set (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))

At one finite window, the average-regret violation set is contained in the measurable simultaneous count bad event and inherits its vanishing confidence budget as an outer-measure bound. No measurability claim is made for the violation set itself. Outside the measurable bad event, optimism and the explicit average certificate both hold.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_vanishingDeltaScheduledAverageRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (n : Nat) (visitFloor : Real) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hvisitFloor : 0 < visitFloor) : let episodes := AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp (n + 1) delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate let violationSet := vanishingDeltaScheduledAverageRegretViolationSet mdp initialState defaultState n visitFloor MeasurableSet (source.adaptiveCumulativeCountBadEvent (n + 1) delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent (n + 1) delta) <= ENNReal.ofReal delta /\ violationSet ⊆ source.adaptiveCumulativeCountBadEvent (n + 1) delta /\ source.trajectoryMeasure violationSet <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ source.adaptiveCumulativeCountBadEvent (n + 1) delta -> (forall round : Fin (n + 1), forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticAverageRecommendedExpectedRegret (initialState

Dependent family of all finite-window high-probability certificates. The two standard-Borel assumptions are themselves indexed by the changing scheduled sample space.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_vanishingDeltaScheduledAverageRecommendedExpectedRegret_allWindows (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (visitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hvisitFloor : 0 < visitFloor) : forall n, letI : StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.vanishingDeltaScheduledEpisodes mdp n visitFloor))