BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtNormalizedRate

Canonical statistical scale for rewards and zero-count budget bounded by one.

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

One sufficient episode threshold for the normalized scale choice.

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

The normalized capped count radius used by the concrete source.

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

Closed recommendation-regret bound after fixing budget and scale.

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

The normalized scale is nonnegative without additional scalar premises.

theorem normalizedCumulativeInverseSqrtScale_nonneg (mdp : MDP State Action) (rounds : Nat) (delta visitFloor : Real) : 0 <= normalizedCumulativeInverseSqrtScale mdp rounds delta visitFloor

The normalized scale exactly covers the explicit two-scale coefficient.

theorem normalizedCumulativeInverseSqrtScale_cover (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) : (cumulativeInverseSqrtCoverCoefficient mdp 1 1) ^ 2 * cumulativeInverseSqrtLogFactor mdp rounds delta <= (normalizedCumulativeInverseSqrtScale mdp rounds delta visitFloor) ^ 2 * visitFloor

The old max threshold is bounded by the single normalized threshold.

theorem cumulativeInverseSqrtCalibrationEpisodeThreshold_le_normalized (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) : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor 1 1 <= normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor

A strict normalized threshold implies the exact parent threshold.

theorem cumulativeInverseSqrtCalibrationEpisodeThreshold_lt_of_normalizedThreshold (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : cumulativeInverseSqrtCalibrationEpisodeThreshold mdp rounds delta visitFloor 1 1 < (episodes : Real)

The single normalized threshold constructs the complete parent calibration.

theorem normalizedCumulativeInverseSqrtPathCalibration_of_episodeThreshold (mdp : MDP State Action) {episodes rounds : Nat} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) {delta visitFloor : Real} (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : CumulativeInverseSqrtPathCalibration mdp episodes rounds delta visitFloor 1 1 (normalizedCumulativeInverseSqrtScale mdp rounds delta visitFloor)

Explicit expansion of the normalized recommendation-regret bound.

theorem normalizedCumulativeInverseSqrtRecommendedExpectedRegretBound_eq (mdp : MDP State Action) (episodes rounds : Nat) (delta visitFloor : Real) : normalizedCumulativeInverseSqrtRecommendedExpectedRegretBound mdp episodes rounds delta visitFloor = 2 * (mdp.horizon : Real) * min (rounds : Real) (8 * (Fintype.card State : Real) * (mdp.horizon : Real) * Real.sqrt (cumulativeInverseSqrtLogFactor mdp rounds delta) / Real.sqrt visitFloor * Real.sqrt (rounds : Real) / Real.sqrt ((episodes : Real) * visitFloor / 2))

Normalized deterministic-reward endpoint with one episode threshold and no caller-visible budget or statistical scale.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_normalizedRecommendedExpectedRegret (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) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : 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) /\ adaptiveCumulativeEmpiricalOptimisticRecommendedExpectedRegret (initialState