Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveEmpiricalOptimisticOccupancyEnvelope
# Explicit occupancy envelope for the fixed-bonus adaptive empirical plan The current known-reward empirical optimistic plan uses zero reward radius and one fixed transition bonus at every coordinate. This module evaluates its recursive occupancy-radius sum exactly and attaches that explicit envelope to the compiled path-support episode-threshold event. The result is linear in rounds and horizon because the bonus is fixed. It is not a count-dependent statistical regret rate.
Module map
Imports
BanditRLProof.RL.FiniteHorizonExploratoryPathSupportEpisodeThreshold
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEmpiricalOptimisticRegret, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticRealizedBehaviorRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_const
Compiled
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
theorem
BanditRLProof.FiniteHorizonRL.adaptiveEmpiricalOptimisticPlanAt_selectedRadiusRemaining
Compiled
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
theorem
BanditRLProof.FiniteHorizonRL.adaptiveEmpiricalOptimisticPlanAt_occupancySelectedRadiusRemaining_eq
Compiled
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
theorem
BanditRLProof.FiniteHorizonRL.adaptiveEmpiricalOptimisticOccupancyRadiusSum_eq
Compiled
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
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_allCoordinateConfidence_optimism_and_explicitRecommendedExpectedRegret_of_pathSupport_episodeThreshold
Compiled
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