BanditRLProof.RL.FiniteHorizonExploratoryPathSupportEpisodeThreshold

Dimension factor sufficient to turn a radius margin into the half contraction.

noncomputable def exploratoryPathCalibrationDimensionFactor (mdp : MDP State Action) : Real

The calibration dimension factor is at least one.

theorem one_le_exploratoryPathCalibrationDimensionFactor (mdp : MDP State Action) : 1 <= exploratoryPathCalibrationDimensionFactor mdp

Closed-form Real episode threshold for the local simultaneous-count budget. Its denominator is positive when `visitFloor` is positive.

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

Above the explicit episode threshold, the simultaneous count radius is less than the common expected-count floor divided by the calibration dimension factor.

theorem simultaneousCountConfidenceRadius_lt_episodes_mul_visitFloor_div_dimensionFactor_of_threshold (mdp : MDP State Action) (witnessState : State) {rounds episodes : Nat} {delta visitFloor : Real} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : exploratoryPathCalibrationEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor / exploratoryPathCalibrationDimensionFactor mdp

The episode threshold simultaneously discharges the strict count margin and the half-contraction premise of the explicit path-support calibration route.

theorem episodeThreshold_countMargin_and_halfContraction (mdp : MDP State Action) (witnessState : State) {rounds episodes : Nat} {delta visitFloor : Real} (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hvisitFloor : 0 < visitFloor) (hthreshold : exploratoryPathCalibrationEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta) < (episodes : Real) * visitFloor /\ (Fintype.card State : Real) * uniformFloorTransitionCoordinateRadius mdp episodes (multiBatchLocalDelta rounds delta) visitFloor * (mdp.horizon : Real) <= 1 / 2

The closed-form episode threshold constructs the source-wide transition cover.

theorem exploratorySource_sourceTransitionBonusCover_of_pathSupport_episodeThreshold {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hthreshold : exploratoryPathCalibrationEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) (hrewardBound_nonneg : 0 <= rewardBound) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate SourceTransitionBonusCover behaviorSource rounds (multiBatchLocalDelta rounds delta) rewardBound rewardBound

The closed-form episode threshold constructs the full source calibration.

theorem exploratorySource_sourceCalibration_of_pathSupport_episodeThreshold {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound delta : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hthreshold : exploratoryPathCalibrationEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) (hrewardBound_nonneg : 0 <= rewardBound) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate SourceCalibration behaviorSource rounds delta rewardBound rewardBound

Route endpoint: path support and one explicit episode threshold imply global adaptive count confidence, roundwise optimism, and recommended expected regret.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret_of_pathSupport_episodeThreshold {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBound : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) (hhorizon : 0 < mdp.horizon) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (support : ExploratoryPathSupport mdp initialState) (visitFloor : Real) (hvisitFloor : 0 < visitFloor) (hfloor : ExploratoryPathUniformVisitFloor support explorationRate visitFloor) (hthreshold : exploratoryPathCalibrationEpisodeThreshold mdp rounds delta visitFloor < (episodes : Real)) : let behaviorSource := exploratorySource mdp initialState episodes initialTable defaultState rewardBound explorationRate hexplorationRate let bad := behaviorSource.adaptiveSimultaneousCountBadEvent rounds delta MeasurableSet bad /\ behaviorSource.trajectoryMeasure bad <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ bad -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp