BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtCalibration

A concrete count radius: the supplied budget at zero visits and inverse-square root decay after the first visit.

noncomputable def inverseSqrt (budget : Real) (hbudget : 0 <= budget) : TransitionCountRadius where

The inverse-square-root radius exposes its supplied zero-count budget.

@[simp] theorem inverseSqrt_radius_zero (budget : Real) (hbudget : 0 <= budget) : (inverseSqrt budget hbudget).radius 0 = budget

Positive counts use the genuine inverse-square-root branch.

theorem inverseSqrt_radius_of_pos (budget : Real) (hbudget : 0 <= budget) {count : Nat} (hcount : 0 < count) : (inverseSqrt budget hbudget).radius count = budget / Real.sqrt count

A usable capped inverse-square-root radius. `budget` controls the zero-count value envelope, while `scale` controls the statistical decay after enough visits; the cap preserves antitonicity across the first visit.

noncomputable def cappedInverseSqrt (budget scale : Real) (hbudget : 0 <= budget) (hscale : 0 <= scale) : TransitionCountRadius where

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

@[simp] theorem cappedInverseSqrt_radius_zero (budget scale : Real) (hbudget : 0 <= budget) (hscale : 0 <= scale) : (cappedInverseSqrt budget scale hbudget hscale).radius 0 = budget

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

theorem cappedInverseSqrt_radius_of_pos (budget scale : Real) (hbudget : 0 <= budget) (hscale : 0 <= scale) {count : Nat} (hcount : 0 < count) : (cappedInverseSqrt budget scale hbudget hscale).radius count = min budget (scale / Real.sqrt count)

Predictable cumulative visit floor supplied by one path-support batch floor.

def cumulativePathVisitExpectedFloor (episodes prefixRounds : Nat) (visitFloor : Real) : Real

Predictable visit floor after subtracting the cumulative confidence radius.

noncomputable def cumulativePathVisitLowerMargin (mdp : MDP State Action) (episodes rounds : Nat) (delta visitFloor : Real) (round : Fin rounds) : Real

Deterministic selected-radius envelope obtained from the lower visit margin.

noncomputable def cumulativeInverseSqrtRadiusEnvelope (mdp : MDP State Action) (episodes rounds : Nat) (delta visitFloor budget scale : Real) (round : Fin rounds) : Real

Scalar regularity needed to fit all transition-coordinate errors under the inverse-square-root planner radius. It is deterministic and roundwise; path support and the martingale event supply the corresponding realized counts.

structure CumulativeInverseSqrtPathCalibration (mdp : MDP State Action) (episodes rounds : Nat) (delta visitFloor rewardBound budget scale : Real) : Prop where

Every adaptive exploratory batch retains the common path-support visit floor.

theorem exploratorySource_coordinateMeanAt_visit_ge_pathFloor (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : (episodes : Real) * visitFloor <= (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).coordinateMeanAt (.visit stage state action) round trajectory

The common batch floor sums to a predictable cumulative visit floor.

theorem exploratorySource_cumulativeCoordinateMean_visit_ge_pathFloor (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (prefixRounds : Nat) (trajectory : EpisodeBatchTrajectory mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : AdaptiveEpisodeBatchSource.cumulativePathVisitExpectedFloor episodes prefixRounds visitFloor <= (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).cumulativeCoordinateMean (.visit stage state action) prefixRounds trajectory

Outside the global count event, every cumulative visit count exceeds its lower margin.

theorem exploratorySource_cumulativePathVisitLowerMargin_lt_visitCount (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor delta : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) {trajectory : EpisodeBatchTrajectory mdp episodes} (htrajectory : trajectory ∉ (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).adaptiveCumulativeCountBadEvent rounds delta) (round : Fin rounds) (stage : Fin mdp.horizon) (state : State) (action : Action) : AdaptiveEpisodeBatchSource.cumulativePathVisitLowerMargin mdp episodes rounds delta visitFloor round < ((cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action : Real)

Path support and the two-scale calibration discharge the full capped inverse-sqrt cover.

theorem exploratorySource_adaptiveCumulativeCountMartingaleCover_of_pathSupport_inverseSqrtCalibration (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor delta : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (rewardBound budget scale : Real) (calibration : AdaptiveEpisodeBatchSource.CumulativeInverseSqrtPathCalibration mdp episodes rounds delta visitFloor rewardBound budget scale) : AdaptiveEpisodeBatchSource.AdaptiveCumulativeCountMartingaleCover (rounds := rounds) (exploratorySource mdp initialState episodes initialTable defaultState (TransitionCountRadius.cappedInverseSqrt budget scale calibration.budget_nonneg calibration.scale_nonneg) explorationRate hexplorationRate) (TransitionCountRadius.cappedInverseSqrt budget scale calibration.budget_nonneg calibration.scale_nonneg) delta rewardBound

The selected capped inverse-sqrt radius is controlled by the lower-margin envelope.

theorem adaptiveCumulativeEmpiricalOptimisticPlanAt_selectedRadiusRemaining_le_inverseSqrtEnvelope (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor delta : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (rewardBound budget scale : Real) (calibration : AdaptiveEpisodeBatchSource.CumulativeInverseSqrtPathCalibration mdp episodes rounds delta visitFloor rewardBound budget scale) {trajectory : EpisodeBatchTrajectory mdp episodes} (htrajectory : trajectory ∉ (exploratorySource mdp initialState episodes initialTable defaultState (TransitionCountRadius.cappedInverseSqrt budget scale calibration.budget_nonneg calibration.scale_nonneg) explorationRate hexplorationRate).adaptiveCumulativeCountBadEvent rounds delta) (round : Fin rounds) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState (TransitionCountRadius.cappedInverseSqrt budget scale calibration.budget_nonneg calibration.scale_nonneg) round).selectedRadiusRemaining remaining hremaining state <= AdaptiveEpisodeBatchSource.cumulativeInverseSqrtRadiusEnvelope mdp episodes rounds delta visitFloor budget scale round

Concrete route endpoint: path support and capped inverse-sqrt calibration produce one measurable cumulative count event, optimism, and a round-indexed finite-sum bound for recommended-policy expected regret.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_explicitRecommendedExpectedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes rounds : Nat) [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (rewardBound budget scale : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (calibration : AdaptiveEpisodeBatchSource.CumulativeInverseSqrtPathCalibration mdp episodes rounds delta visitFloor rewardBound budget scale) : let countRadius := TransitionCountRadius.cappedInverseSqrt budget scale calibration.budget_nonneg calibration.scale_nonneg 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) /\ adaptiveCumulativeEmpiricalOptimisticRecommendedExpectedRegret (initialState := initialState) trajectory defaultState countRadius rounds <= ∑ round : Fin rounds, (mdp.horizon : Real) * (2 * AdaptiveEpisodeBatchSource.cumulativeInverseSqrtRadiusEnvelope mdp episodes rounds delta visitFloor budget scale round)