BanditRLProof.RL.FiniteHorizonAdaptiveEmpiricalOptimisticOccupancyEnvelope

A probability occupancy sum evaluates a constant stage cost exactly.

theorem MarkovPolicy.occupancySumRemaining_const {mdp : MDP State Action} (policy : MarkovPolicy mdp) (c : Real) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : policy.occupancySumRemaining (fun _remaining _hremaining _state => c) remaining hremaining mu = (remaining : Real) * c

The concrete known-reward empirical plan selects its fixed transition bonus.

theorem adaptiveEmpiricalOptimisticPlanAt_selectedRadiusRemaining {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (round remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (adaptiveEmpiricalOptimisticPlanAt (mdp := mdp) (episodes := episodes) trajectory defaultState transitionBonus round).selectedRadiusRemaining remaining hremaining state = transitionBonus

Each round's selected-radius occupancy term is the horizon times the fixed cost.

theorem adaptiveEmpiricalOptimisticPlanAt_occupancySelectedRadiusRemaining_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (round : Nat) : let plan := adaptiveEmpiricalOptimisticPlanAt (mdp := mdp) (episodes := episodes) trajectory defaultState transitionBonus round plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState = (mdp.horizon : Real) * (2 * transitionBonus)

The complete adaptive selected-radius occupancy sum has a closed form.

theorem adaptiveEmpiricalOptimisticOccupancyRadiusSum_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (rounds : Nat) : adaptiveEmpiricalOptimisticOccupancyRadiusSum (mdp := mdp) (initialState := initialState) (episodes := episodes) trajectory defaultState transitionBonus rounds = (rounds : Real) * ((mdp.horizon : Real) * (2 * transitionBonus))

Route endpoint: the path-support episode threshold now yields a fully explicit fixed-bonus bound for the recommended optimistic policies.

theorem exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_explicitRecommendedExpectedRegret_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 := mdp) (episodes := episodes) trajectory defaultState rewardBound round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveEmpiricalOptimisticRecommendedExpectedRegret (mdp := mdp) (initialState := initialState) (episodes := episodes) trajectory defaultState rewardBound rounds <= (rounds : Real) * ((mdp.horizon : Real) * (2 * rewardBound))