Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticRealizedBehaviorRegret
# Concrete stochastic empirical-optimistic realized behavior regret This module combines the concrete stochastic known-mean empirical-transition source with the global sampled-return transport. The count/optimism event and the sampled-return event retain separate confidence budgets. The expected regret of the exploratory behavior is charged explicitly against the projected recommended policy before the realized-return deviation is added. The result remains a fixed-window theorem for successor batches. It does not estimate stochastic reward means, include the initial batch in realized regret, or claim an anytime, minimax, or complete UCB-VI result.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticProjection, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardRealizedBehaviorRegret, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeExploratoryBehaviorRegret, BanditRLProof.RL.FiniteHorizonAdaptiveEmpiricalOptimisticOccupancyEnvelope
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationConsistency, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticRealizedBehaviorRegret
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_expected_to_realized_successor_average_regret_transport_two_delta
Compiled
Generic two-budget version of the expected-to-realized successor-regret transport. The caller's event keeps `countDelta`, while the return event uses `returnDelta`.
theorem trajectoryMeasure_expected_to_realized_successor_average_regret_transport_two_delta {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (countDelta returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) (countBadEvent : Set (StochasticEpisodeBatchTrajectory mdp episodes)) (expectedBound : Real) (Good : StochasticEpisodeBatchTrajectory mdp episodes -> Prop) (hcountMeasurable : MeasurableSet countBadEvent) (hcountTail : source.trajectoryMeasure countBadEvent <= ENNReal.ofReal countDelta) (hcountGood : forall trajectory, trajectory ∉ countBadEvent -> Good trajectory /\ source.successorExpectedAverageRegret trajectory rounds <= expectedBound) : let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy returnDelta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= ENNReal.ofReal countDelta + ENNReal.ofReal returnDelta /\ forall trajectory, trajectory ∉ combinedBadEvent -> Good trajectory /\ source.realizedSuccessorAverageRegret trajectory rounds <= expectedBound + Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) returnDelta / ((episodes : Real) * (rounds : Real))
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.projectedExploratoryBehaviorExpectedRegret
Compiled
Sum of expected regrets of the projected empirical-optimistic exploratory behaviors.
noncomputable def projectedExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) : Real
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.projectedAverageExploratoryBehaviorExpectedRegret
Compiled
Average expected regret of the projected exploratory behaviors.
noncomputable def projectedAverageExploratoryBehaviorExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rounds : Nat) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.projectedExploratoryBehaviorExpectedRegret_le
Compiled
Exploratory behavior regret is recommendation regret plus one charge per round.
theorem projectedExploratoryBehaviorExpectedRegret_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) : projectedExploratoryBehaviorExpectedRegret (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.projectedAverageExploratoryBehaviorExpectedRegret_le
Compiled
Averaging removes the repeated-round exploration factor.
theorem projectedAverageExploratoryBehaviorExpectedRegret_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) (rounds : Nat) (hrounds : 0 < rounds) : projectedAverageExploratoryBehaviorExpectedRegret (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.measurable_selectedExploratoryGlobalReturnDeviation
Compiled
Dynamic global-return measurability for any finite exploratory table selector.
theorem measurable_selectedExploratoryGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} {episodes : Nat} {History : Type*} [MeasurableSpace History] (selector : History -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : Measurable fun pair : History × StochasticEpisodeBatch mdp episodes => mdp.globalSampledCumulativeReturnDeviationSum ((selector pair.1).exploratoryPolicy explorationRate hexplorationRate) initialState episodes pair.2
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.exploratorySource_successorExpectedCumulativeRegret_eq_projected
Compiled
The concrete source's successor policies are the projected exploratory policies.
theorem exploratorySource_successorExpectedCumulativeRegret_eq_projected {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).successorExpectedCumulativeRegret trajectory rounds = projectedExploratoryBehaviorExpectedRegret (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.exploratorySource_successorExpectedAverageRegret_eq_projected
Compiled
Average form of the projected successor-policy identity.
theorem exploratorySource_successorExpectedAverageRegret_eq_projected {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : (exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate).successorExpectedAverageRegret trajectory rounds = projectedAverageExploratoryBehaviorExpectedRegret (initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_projectedAllCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret
Compiled
Concrete fixed-window route endpoint: projected count confidence and optimism, exploratory behavior charge, and stochastic realized-return concentration hold simultaneously with separate confidence budgets.
theorem exploratorySource_trajectoryMeasure_projectedAllCoordinateConfidence_optimism_and_realizedSuccessorAverageRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (EpisodeBatch mdp episodes)] [Nonempty (EpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (htransitionBonus_nonneg : 0 <= transitionBonus) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (countDelta returnDelta : Real) (hcountDelta : 0 < countDelta) (hcountDelta_le_one : countDelta <= 1) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) (htotal : 0 < ((AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (calibration : let deterministicSource := AdaptiveEmpiricalOptimisticSource.exploratorySource mdp initialState episodes initialTable defaultState transitionBonus explorationRate hexplorationRate AdaptiveEmpiricalOptimisticSource.SourceCalibration deterministicSource rounds countDelta (rewardBound : Real) transitionBonus) : let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState transitionBonus explorationRate hexplorationRate let projection := MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp