BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtExplicitRate

The logarithmic factor shared by every queried cumulative prefix.

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

The deterministic coefficient multiplying each cumulative count radius.

noncomputable def cumulativeInverseSqrtCoverCoefficient (mdp : MDP State Action) (rewardBound budget : Real) : Real

A sufficient episode threshold for both a half expected-visit margin and the budget branch of the capped transition-radius cover.

noncomputable def cumulativeInverseSqrtCalibrationEpisodeThreshold (mdp : MDP State Action) (rounds : Nat) (delta visitFloor rewardBound budget : Real) : Real

Exact square of one cumulative coordinate confidence radius.

theorem cumulativeCoordinateConfidenceRadius_sq_eq (mdp : MDP State Action) {episodes rounds prefixRounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (cumulativeCoordinateConfidenceRadius episodes prefixRounds (cumulativeCountLocalDelta mdp rounds delta)) ^ 2 = (prefixRounds : Real) * (episodes : Real) / 2 * cumulativeInverseSqrtLogFactor mdp rounds delta

The shared logarithmic factor is nonnegative at a valid global delta.

theorem cumulativeInverseSqrtLogFactor_nonneg (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 episode threshold leaves at least half of the predictable expected visits after subtracting the cumulative confidence radius, uniformly over prefixes.

theorem half_cumulativePathVisitExpectedFloor_lt_lowerMargin_of_episodeThreshold (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) {delta visitFloor rewardBound budget : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor rewardBound budget < (episodes : Real)) (round : Fin rounds) : (round + 1 : Real) * (episodes : Real) * visitFloor / 2 < cumulativePathVisitLowerMargin mdp episodes rounds delta visitFloor round

The explicit episode threshold and scale-square condition construct the full two-scale path calibration; no roundwise cover premise remains.

theorem cumulativeInverseSqrtPathCalibration_of_episodeThreshold (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) {delta visitFloor rewardBound budget scale : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hrewardBound : 0 <= rewardBound) (hbudget : 0 < budget) (hscale : 0 <= scale) (hscaleCover : (cumulativeInverseSqrtCoverCoefficient mdp rewardBound budget) ^ 2 * cumulativeInverseSqrtLogFactor mdp rounds delta <= scale ^ 2 * visitFloor) (hthreshold : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor rewardBound budget < (episodes : Real)) : CumulativeInverseSqrtPathCalibration mdp episodes rounds delta visitFloor rewardBound budget scale

Closed-form cap-versus-square-root bound for the complete round sum.

noncomputable def cumulativeInverseSqrtEnvelopeSumBound (episodes rounds : Nat) (visitFloor budget scale : Real) : Real

The round-indexed capped inverse-square-root envelopes sum to the minimum of the linear cap and an explicit square-root-in-rounds bound.

theorem sum_cumulativeInverseSqrtRadiusEnvelope_le_explicit (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) {delta visitFloor rewardBound budget scale : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hscale : 0 <= scale) (hthreshold : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor rewardBound budget < (episodes : Real)) : (∑ round : Fin rounds, cumulativeInverseSqrtRadiusEnvelope mdp episodes rounds delta visitFloor budget scale round) <= cumulativeInverseSqrtEnvelopeSumBound episodes rounds visitFloor budget scale

Explicit closed form replacing the terminal's unsimplified round sum.

noncomputable def cumulativeInverseSqrtRecommendedExpectedRegretBound (mdp : MDP State Action) (episodes rounds : Nat) (visitFloor budget scale : Real) : Real

The terminal's horizon-weighted finite sum is bounded by the closed form.

theorem sum_horizon_mul_two_cumulativeInverseSqrtRadiusEnvelope_le_explicit (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) {delta visitFloor rewardBound budget scale : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hscale : 0 <= scale) (hthreshold : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor rewardBound budget < (episodes : Real)) : (∑ round : Fin rounds, (mdp.horizon : Real) * (2 * cumulativeInverseSqrtRadiusEnvelope mdp episodes rounds delta visitFloor budget scale round)) <= cumulativeInverseSqrtRecommendedExpectedRegretBound mdp episodes rounds visitFloor budget scale

Closed-form route endpoint: deterministic episode and scale inequalities construct the capped calibration and replace the round sum by an explicit minimum of a linear cap and a square-root-in-rounds rate.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_closedFormRecommendedExpectedRegret (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) (hbudget : 0 < budget) (hscale : 0 <= scale) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hscaleCover : (AdaptiveEpisodeBatchSource.cumulativeInverseSqrtCoverCoefficient mdp rewardBound budget) ^ 2 * AdaptiveEpisodeBatchSource.cumulativeInverseSqrtLogFactor mdp rounds delta <= scale ^ 2 * visitFloor) (hthreshold : AdaptiveEpisodeBatchSource.cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor rewardBound budget < (episodes : Real)) : let countRadius := TransitionCountRadius.cappedInverseSqrt budget scale hbudget.le hscale 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