BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticRealizedBehaviorRegret

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))

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

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

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 := initialState) trajectory defaultState transitionBonus explorationRate hexplorationRate rounds <= adaptiveEmpiricalOptimisticRecommendedExpectedRegret (initialState := initialState) trajectory defaultState transitionBonus rounds + (rounds : Real) * exploratoryBehaviorRegretCharge mdp explorationRate rewardBound

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 := initialState) trajectory defaultState transitionBonus explorationRate hexplorationRate rounds <= adaptiveEmpiricalOptimisticRecommendedExpectedRegret (initialState := initialState) trajectory defaultState transitionBonus rounds / (rounds : Real) + exploratoryBehaviorRegretCharge mdp explorationRate rewardBound

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

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 := initialState) (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes trajectory) defaultState transitionBonus explorationRate hexplorationRate rounds

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 := initialState) (MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp := mdp) episodes trajectory) defaultState transitionBonus explorationRate hexplorationRate rounds

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 := mdp) episodes let countBadEvent := projectedAdaptiveSimultaneousCountBadEvent (mdp := mdp) (initialState := initialState) (episodes := episodes) initialTable defaultState transitionBonus explorationRate hexplorationRate rounds countDelta 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 -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveEmpiricalOptimisticPlanAt (mdp := mdp) (episodes := episodes) (projection trajectory) defaultState transitionBonus round).upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= (mdp.horizon : Real) * (2 * transitionBonus) + exploratoryBehaviorRegretCharge mdp explorationRate (rewardBound : Real) + Concentration.subGaussianSumConfidenceRadius (AdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) returnDelta / ((episodes : Real) * (rounds : Real))