BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtAverageConsistency

Real-valued batch-size target that clears both normalized calibration and the one-batch logarithmic visit-mass requirement.

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

Explicit positive natural batch size associated with the scheduled target.

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

The inverse-square-root envelope for the scheduled average bound.

noncomputable def normalizedCumulativeInverseSqrtScheduledAverageEnvelope (mdp : MDP State Action) (rounds : Nat) (visitFloor : Real) : Real

The valid global confidence budget makes the shared logarithm strict.

theorem cumulativeInverseSqrtLogFactor_pos (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 0 < cumulativeInverseSqrtLogFactor mdp rounds delta

The scheduled real-valued target is nonnegative under valid parameters.

theorem normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_nonneg (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : 0 <= normalizedCumulativeInverseSqrtScheduledEpisodeThreshold mdp rounds delta visitFloor

Every scheduled batch size is positive.

theorem normalizedCumulativeInverseSqrtScheduledEpisodes_pos (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : 0 < normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor

The real-valued target is strictly below the scheduled natural batch size.

theorem normalizedCumulativeInverseSqrtScheduledEpisodeThreshold_lt_episodes (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : normalizedCumulativeInverseSqrtScheduledEpisodeThreshold mdp rounds delta visitFloor < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real)

The schedule strictly clears the parent normalized calibration threshold.

theorem normalizedCumulativeInverseSqrtEpisodeThreshold_lt_scheduledEpisodes (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real)

One scheduled batch has strictly more visit mass than the log factor.

theorem cumulativeInverseSqrtLogFactor_lt_scheduledEpisodeVisitMass (mdp : MDP State Action) (rounds : Nat) (delta : Real) {visitFloor : Real} (hvisitFloor : 0 < visitFloor) : cumulativeInverseSqrtLogFactor mdp rounds delta < (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor : Real) * visitFloor / 2

The normalized scheduled average bound is nonnegative.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_nonneg (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : 0 <= normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor) rounds delta visitFloor

The scheduled average bound is controlled by a pure inverse-square-root rate.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_le_envelope (mdp : MDP State Action) {rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor) rounds delta visitFloor <= normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp rounds visitFloor

The deterministic inverse-square-root envelope tends to zero.

theorem normalizedCumulativeInverseSqrtScheduledAverageEnvelope_tendsto_zero (mdp : MDP State Action) (visitFloor : Real) : Tendsto (fun n : Nat => normalizedCumulativeInverseSqrtScheduledAverageEnvelope mdp (n + 1) visitFloor) atTop (nhds 0)

The scheduled scalar average recommendation-regret bound tends to zero.

theorem normalizedCumulativeInverseSqrtScheduledAverageBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (delta visitFloor : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : Tendsto (fun n : Nat => normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp (normalizedCumulativeInverseSqrtScheduledEpisodes mdp (n + 1) delta visitFloor) (n + 1) delta visitFloor) atTop (nhds 0)

At every positive finite window, the explicit schedule discharges calibration and preserves the parent's measurable event, delta tail, optimism, and average recommended-policy expected-regret conclusion.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_scheduledAverageRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rounds : Nat) (delta visitFloor : Real) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor))] [StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta 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) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) : let episodes := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtScheduledEpisodes mdp rounds delta visitFloor let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate MeasurableSet (source.adaptiveCumulativeCountBadEvent rounds delta) /\ source.trajectoryMeasure (source.adaptiveCumulativeCountBadEvent rounds delta) <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ source.adaptiveCumulativeCountBadEvent rounds delta -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticAverageRecommendedExpectedRegret (initialState := initialState) trajectory defaultState countRadius rounds <= AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtAverageRecommendedExpectedRegretBound mdp episodes rounds delta visitFloor