BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardRealizedBehaviorRegret

The sampled policy-value fluctuation at one complete episode coordinate.

noncomputable def initialPolicyValueDeviation (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (trajectory : State × RewardStepTrace Action State mdp.horizon) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_initialPolicyValueDeviation (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) : Measurable (mdp.initialPolicyValueDeviation policy initialState)

Hoeffding proxy for the policy value of one sampled initial state.

noncomputable def initialPolicyValueVarianceProxy (mdp : MDP State Action) (rewardBound : NNReal) : NNReal

The generated complete trajectory has the exact supplied initial marginal.

theorem stochasticTrajectoryMeasure_map_fst (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : (source.stochasticTrajectoryMeasure policy initialState).map Prod.fst = initialState

The initial-state policy-value fluctuation is sub-Gaussian.

theorem stochasticTrajectoryMeasure_initialPolicyValueDeviation_hasSubgaussianMGF (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) : ProbabilityTheory.HasSubgaussianMGF (mdp.initialPolicyValueDeviation policy initialState) (mdp.initialPolicyValueVarianceProxy rewardBound) (source.stochasticTrajectoryMeasure policy initialState)

Initial-state value fluctuation at one coordinate of an iid episode family.

noncomputable def initialPolicyValueDeviationAtEpisode (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) {episodes : Nat} (episode : Fin episodes) (trajectories : StochasticEpisodeBatch mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_initialPolicyValueDeviationAtEpisode (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) {episodes : Nat} (episode : Fin episodes) : Measurable (mdp.initialPolicyValueDeviationAtEpisode policy initialState episode)

Sum of initial-state policy-value fluctuations in one iid batch.

noncomputable def initialPolicyValueDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (episodes : Nat) (trajectories : StochasticEpisodeBatch mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_initialPolicyValueDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (episodes : Nat) : Measurable (mdp.initialPolicyValueDeviationSum policy initialState episodes)

Episode-linear proxy for the initial-state value fluctuation sum.

noncomputable def iidInitialPolicyValueDeviationVarianceProxy (mdp : MDP State Action) (episodes : Nat) (rewardBound : NNReal) : NNReal

Sum of all sampled rewards in one complete stochastic episode batch.

def sampledCumulativeRewardSum (mdp : MDP State Action) (episodes : Nat) (trajectories : StochasticEpisodeBatch mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_sampledCumulativeRewardSum (mdp : MDP State Action) (episodes : Nat) : Measurable (mdp.sampledCumulativeRewardSum episodes)

One batch's sampled return centered by the selected policy's global initial-law value.

noncomputable def globalSampledCumulativeReturnDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (episodes : Nat) (trajectories : StochasticEpisodeBatch mdp episodes) : Real

The global batch deviation is actual sampled return minus its policy mean.

theorem globalSampledCumulativeReturnDeviationSum_eq (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (episodes : Nat) (trajectories : StochasticEpisodeBatch mdp episodes) : mdp.globalSampledCumulativeReturnDeviationSum policy initialState episodes trajectories = mdp.sampledCumulativeRewardSum episodes trajectories - (episodes : Real) * integral initialState (policy.valueAt 0 (Nat.zero_le mdp.horizon))

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_globalSampledCumulativeReturnDeviationSum (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) (episodes : Nat) : Measurable (mdp.globalSampledCumulativeReturnDeviationSum policy initialState episodes)

Honest same-space proxy for the two globally centered batch components.

noncomputable def iidGlobalSampledCumulativeReturnDeviationVarianceProxy (mdp : MDP State Action) (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal

No declaration docstring is present; use the chapter context and exact statement below.

theorem iIndepFun_initialPolicyValueDeviationAtEpisode (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.iIndepFun (fun episode trajectories => mdp.initialPolicyValueDeviationAtEpisode policy initialState episode trajectories) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

No declaration docstring is present; use the chapter context and exact statement below.

theorem initialPolicyValueDeviationAtEpisode_hasSubgaussianMGF (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) {episodes : Nat} (episode : Fin episodes) : ProbabilityTheory.HasSubgaussianMGF (mdp.initialPolicyValueDeviationAtEpisode policy initialState episode) (mdp.initialPolicyValueVarianceProxy rewardBound) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

No declaration docstring is present; use the chapter context and exact statement below.

theorem iidStochasticTrajectoryFamilyMeasure_initialPolicyValueDeviationSum_hasSubgaussianMGF (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardBound : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) : ProbabilityTheory.HasSubgaussianMGF (mdp.initialPolicyValueDeviationSum policy initialState episodes) (mdp.iidInitialPolicyValueDeviationVarianceProxy episodes rewardBound) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

No declaration docstring is present; use the chapter context and exact statement below.

theorem iidStochasticTrajectoryFamilyMeasure_globalSampledCumulativeReturnDeviationSum_hasSubgaussianMGF [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] (source : MeanCompatibleRewardKernel mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.UniformSubgaussianRewardLaw rewardVarianceProxy) : ProbabilityTheory.HasSubgaussianMGF (mdp.globalSampledCumulativeReturnDeviationSum policy initialState episodes) (mdp.iidGlobalSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy) (source.iidStochasticTrajectoryFamilyMeasure policy initialState episodes)

Explicit measurability of the history-selected globally centered batch return.

class GlobalReturnMeasurability {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : Prop where

Dynamic globally centered return on a prefix/next-batch pair.

noncomputable def successorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (pair : StochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : Measurable (source.successorGlobalReturnDeviation n)

Selected conditional law of the globally centered next-batch return.

noncomputable def successorGlobalReturnDeviationKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : ProbabilityTheory.Kernel (StochasticEpisodeBatchPrefix mdp episodes n) Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorGlobalReturnDeviationKernel_apply {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : source.successorGlobalReturnDeviationKernel n history = (source.rewardSource.iidStochasticTrajectoryFamilyMeasure (source.successorPolicy n history) initialState episodes).map (mdp.globalSampledCumulativeReturnDeviationSum (source.successorPolicy n history) initialState episodes)

Trajectory-level globally centered return at successor coordinate `n + 1`.

noncomputable def successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : Measurable (source.successorGlobalReturnDeviationAt n)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_condDistrib_successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : ProbabilityTheory.condDistrib (source.successorGlobalReturnDeviationAt n) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.successorGlobalReturnDeviationKernel n

No declaration docstring is present; use the chapter context and exact statement below.

theorem condExpKernel_map_successorGlobalReturnDeviationAt_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : Filter.Eventually (fun trajectory : StochasticEpisodeBatchTrajectory mdp episodes => Measure.map (source.successorGlobalReturnDeviationAt n) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (StochasticEpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = source.successorGlobalReturnDeviationKernel n (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Prefix process that deliberately leaves coordinate zero uncharged.

noncomputable def successorGlobalReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : (round : Nat) → StochasticEpisodeBatchPrefix mdp episodes round → Real | 0, _history => 0 | n + 1, history => source.successorGlobalReturnDeviation n (Preorder.frestrictLe₂ (π

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_successorGlobalReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (round : Nat) : Measurable (source.successorGlobalReturnPrefixIncrement round)

No declaration docstring is present; use the chapter context and exact statement below.

noncomputable def successorGlobalReturnIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorGlobalReturnIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] : StronglyAdapted (Filtration.piLE (X

No declaration docstring is present; use the chapter context and exact statement below.

theorem successorGlobalReturnIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : ProbabilityTheory.HasCondSubgaussianMGF (Filtration.piLE (X

Zero plus `rounds` successor proxies.

noncomputable def cumulativeSuccessorGlobalReturnVarianceProxy (mdp : MDP State Action) (rounds episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal

No declaration docstring is present; use the chapter context and exact statement below.

theorem cumulativeSuccessorGlobalReturnVarianceProxy_eq (mdp : MDP State Action) (rounds episodes : Nat) (rewardBound rewardVarianceProxy : NNReal) : cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy = (rounds : NNReal) * mdp.iidGlobalSampledCumulativeReturnDeviationVarianceProxy episodes rewardBound rewardVarianceProxy

Cumulative globally centered deviation over successor coordinates only.

noncomputable def cumulativeSuccessorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) delta ≤ |source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory|} ≤ ENNReal.ofReal delta

The selected successor policy after observing coordinates through `n`.

noncomputable def successorPolicyAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) : MarkovPolicy mdp

Optimal expected return under the supplied initial-state law.

noncomputable def optimalInitialExpectedReturn [Nonempty Action] (mdp : MDP State Action) (initialState : Measure State) : Real

Sum of selected successor-policy expected regrets.

noncomputable def successorExpectedCumulativeRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

Average selected successor-policy expected regret per adaptive round.

noncomputable def successorExpectedAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

Realized regret of all sampled successor batches.

noncomputable def realizedSuccessorCumulativeRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (_source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

Realized successor regret averaged over sampled episodes and rounds.

noncomputable def realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

The adaptive successor increment is actual batch return minus policy mean.

theorem successorGlobalReturnIncrement_succ_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) : source.successorGlobalReturnIncrement (n + 1) trajectory = mdp.sampledCumulativeRewardSum episodes (trajectory (n + 1)) - (episodes : Real) * integral initialState ((source.successorPolicyAt trajectory n).valueAt 0 (Nat.zero_le mdp.horizon))

The cumulative deviation is the finite sum over successor coordinates.

theorem cumulativeSuccessorGlobalReturnDeviation_eq_fin_sum {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory = ∑ round : Fin rounds, source.successorGlobalReturnIncrement ((round : Nat) + 1) trajectory

Exact realized equals expected minus globally centered return deviation.

theorem realizedSuccessorCumulativeRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.realizedSuccessorCumulativeRegret trajectory rounds = (episodes : Real) * source.successorExpectedCumulativeRegret trajectory rounds - source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory

Exact averaged form of the stochastic realized-regret decomposition.

theorem realizedSuccessorAverageRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] [Nonempty Action] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : StochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) : source.realizedSuccessorAverageRegret trajectory rounds = source.successorExpectedAverageRegret trajectory rounds - source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory / ((episodes : Real) * (rounds : Real))

Return-deviation event used by fixed-window stochastic regret transport.

noncomputable def successorGlobalReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : Set (StochasticEpisodeBatchTrajectory mdp episodes)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurable_cumulativeSuccessorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) : Measurable (source.cumulativeSuccessorGlobalReturnDeviation rounds)

No declaration docstring is present; use the chapter context and exact statement below.

theorem measurableSet_successorGlobalReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : MeasurableSet (source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy delta)

No declaration docstring is present; use the chapter context and exact statement below.

theorem trajectoryMeasure_successorGlobalReturnDeviationBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty Action] [StandardBorelSpace (StochasticEpisodeBatch mdp episodes)] [Nonempty (StochasticEpisodeBatch mdp episodes)] [StandardBorelSpace (StochasticEpisodeBatchTrajectory mdp episodes)] (source : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) : source.trajectoryMeasure (source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy delta) ≤ ENNReal.ofReal delta

Combine a caller-supplied count/optimism event with the stochastic return event.

theorem trajectoryMeasure_expected_to_realized_successor_average_regret_transport {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [Nonempty 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 : ∀ state action, |mdp.reward state action| ≤ (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta ≤ 1) (countBadEvent : Set (StochasticEpisodeBatchTrajectory mdp episodes)) (expectedBound : Real) (Good : StochasticEpisodeBatchTrajectory mdp episodes → Prop) (hcountMeasurable : MeasurableSet countBadEvent) (hcountTail : source.trajectoryMeasure countBadEvent ≤ ENNReal.ofReal delta) (hcountGood : ∀ trajectory, trajectory ∉ countBadEvent → Good trajectory ∧ source.successorExpectedAverageRegret trajectory rounds ≤ expectedBound) : let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent ∧ source.trajectoryMeasure combinedBadEvent ≤ ENNReal.ofReal delta + ENNReal.ofReal delta ∧ ∀ trajectory, trajectory ∉ combinedBadEvent → Good trajectory ∧ source.realizedSuccessorAverageRegret trajectory rounds ≤ expectedBound + Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorGlobalReturnVarianceProxy mdp rounds episodes rewardBound rewardVarianceProxy) delta / ((episodes : Real) * (rounds : Real))