BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceConsistency

Realized successor cumulative regret is measurable on the causal space.

theorem measurable_realizedSuccessorCumulativeRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.realizedSuccessorCumulativeRegret trajectory rounds)

Realized successor average regret is measurable on the causal space.

theorem measurable_realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.realizedSuccessorAverageRegret trajectory rounds)

A positive-weight sum of selected-policy expected regrets is nonnegative.

theorem successorWeightedExpectedCumulativeRegret_nonneg {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : 0 <= source.successorWeightedExpectedCumulativeRegret trajectory rounds

The positive-weight successor expected average regret is nonnegative.

theorem successorWeightedExpectedAverageRegret_nonneg {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : 0 <= source.successorWeightedExpectedAverageRegret trajectory rounds

An expected-regret upper bound and a two-sided global return bound control the absolute realized regret under the exact heterogeneous successor mass.

theorem abs_realizedSuccessorAverageRegret_le_of_expected_le_of_deviation_abs_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hmass : 0 < successorEpisodeMass episodes rounds) (expectedBound deviationBound : Real) (hexpected : source.successorWeightedExpectedAverageRegret trajectory rounds <= expectedBound) (hdeviation : |source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory| <= deviationBound) : |source.realizedSuccessorAverageRegret trajectory rounds| <= expectedBound + deviationBound / successorEpisodeMass episodes rounds

The local count and reward share is an explicit shifted p-series term.

theorem selfConsistentScheduledLocalDelta_eq_inv_pow (mdp : MDP State Action) (t : Nat) : AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp t = 1 / (((t + 2 : Nat) : Real) ^ (mdp.horizon + 5))

Coordinatewise causal model confidence shares are summable.

theorem summable_selfConsistentScheduledLocalDelta (mdp : MDP State Action) : Summable (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp)

Two model-confidence shares are charged at every causal coordinate.

noncomputable def selfConsistentScheduledCausalCoordinateModelFailureBudget (mdp : MDP State Action) (t : Nat) : ENNReal

Infinite model-confidence budget after deleting a finite burn-in prefix.

noncomputable def selfConsistentScheduledCausalTailModelFailureBudget (mdp : MDP State Action) (burnin : Nat) : ENNReal

The full coordinatewise model-confidence budget is finite.

theorem tsum_selfConsistentScheduledCausalCoordinateModelFailureBudget_ne_top (mdp : MDP State Action) : ∑' t, selfConsistentScheduledCausalCoordinateModelFailureBudget mdp t ≠ ∞

Deleting a growing finite prefix makes the infinite model tail vanish.

theorem selfConsistentScheduledCausalTailModelFailureBudget_tendsto_zero (mdp : MDP State Action) : Tendsto (selfConsistentScheduledCausalTailModelFailureBudget mdp) atTop (nhds 0)

The actual sampled-model event at one coordinate of the causal source.

noncomputable def selfConsistentScheduledCausalModelRoundBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (t : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s))

Union of all actual sampled-model failures after a finite burn-in.

noncomputable def selfConsistentScheduledCausalTailModelBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s))

Every concrete causal coordinate model event is measurable.

theorem measurableSet_selfConsistentScheduledCausalModelRoundBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (t : Nat) : MeasurableSet (selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)

The infinite tail event is measurable by countable union.

theorem measurableSet_selfConsistentScheduledCausalTailModelBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin : Nat) : MeasurableSet (selfConsistentScheduledCausalTailModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin)

One causal coordinate receives its exact pair of local confidence shares.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_modelRoundBadEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (t : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) <= selfConsistentScheduledCausalCoordinateModelFailureBudget mdp t

The actual infinite tail event is controlled by the summable tail budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_tailModelBadEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (burnin : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledCausalTailModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin) <= selfConsistentScheduledCausalTailModelFailureBudget mdp burnin

Outside the tail event, every coordinate after burn-in is model-good.

theorem not_mem_selfConsistentScheduledCausalModelRoundBadEvent_of_not_mem_tail (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin t : Nat) (hburnin : burnin <= t) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (htrajectory : trajectory ∉ selfConsistentScheduledCausalTailModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin) : trajectory ∉ selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t

One model-good causal coordinate yields optimism and recommended regret.

theorem selfConsistentScheduledCausalSource_coordinateConfidence_of_not_mem_modelRoundBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (t : Nat) (hnot : trajectory ∉ selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) : let episodes := fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s let rewardBudget := fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor s let transitionBudget := fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor s let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) ∧ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState

The exact local planning budget is bounded by the named vanishing rate.

theorem selfConsistentScheduledCausalLocalPlanningBound_le_rateAt (mdp : MDP State Action) (varianceProxy : NNReal) {baseVisitFloor : Real} (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (t : Nat) : let rewardBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor let transitionBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor (mdp.horizon : Real) * (2 * (rewardBudget t + transitionBudget t)) + exploratoryBehaviorRegretCharge mdp (AdaptiveEpisodeBatchSource.decayingExplorationRate (t + 1)) 1 <= selfConsistentScheduledCausalPlanningRateAt mdp t

Burn-in regret plus the full weighted causal planning-rate average.

noncomputable def selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : Real

For fixed burn-in, early regret is diluted and the tail planning rate vanishes.

theorem selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin : Nat) : Tendsto (selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin) atTop (nhds 0)

Tail model confidence yields a burn-in-diluted weighted expected regret.

theorem selfConsistentScheduledCausalSource_weightedExpectedSuccessorAverageRegret_le_burninEnvelope (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ selfConsistentScheduledCausalTailModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.successorWeightedExpectedAverageRegret trajectory rounds <= selfConsistentScheduledCausalBurninExpectedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin rounds

Return confidence share adapted to the actual causal successor mass.

noncomputable def selfConsistentScheduledCausalVanishingReturnDelta (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

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

theorem selfConsistentScheduledCausalVanishingReturnDelta_pos (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : 0 < selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor rounds

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

theorem selfConsistentScheduledCausalVanishingReturnDelta_le_one (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor rounds <= 1

The mass-adapted return failure share tends to zero.

theorem selfConsistentScheduledCausalVanishingReturnDelta_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Explicit normalized return radius for the mass-adapted confidence share.

noncomputable def selfConsistentScheduledCausalVanishingReturnRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real

The mass-adapted normalized return radius has the explicit envelope.

theorem normalizedSuccessorGlobalReturnConfidenceRadius_vanishingDelta_eq (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (hrounds : 0 < rounds) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t HeterogeneousAdaptiveStochasticEpisodeBatchSource.normalizedSuccessorGlobalReturnConfidenceRadius mdp episodes rounds 1 varianceProxy (selfConsistentScheduledCausalVanishingReturnDelta mdp varianceProxy baseVisitFloor rounds) = selfConsistentScheduledCausalVanishingReturnRateEnvelope mdp varianceProxy baseVisitFloor rounds

The mass-adapted normalized return radius tends to zero.

theorem selfConsistentScheduledCausalVanishingReturnRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (selfConsistentScheduledCausalVanishingReturnRateEnvelope mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Tail model event combined with the mass-adapted two-sided return event.

noncomputable def selfConsistentScheduledCausalTailModelReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))

Exact tail-model plus mass-adapted return failure budget.

noncomputable def selfConsistentScheduledCausalTailModelReturnFailureBudget (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : ENNReal

Burn-in expected-regret envelope plus the mass-adapted return radius.

noncomputable def selfConsistentScheduledCausalBurninRealizedRegretRateEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) : Real

For fixed burn-in, the complete deterministic realized envelope vanishes.

theorem selfConsistentScheduledCausalBurninRealizedRegretRateEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin : Nat) : Tendsto (selfConsistentScheduledCausalBurninRealizedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin) atTop (nhds 0)

Tail optimism and absolute realized regret on the natural causal source.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_tail_optimism_and_absoluteRealizedRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds MeasurableSet event ∧ source.trajectoryMeasure event <= selfConsistentScheduledCausalTailModelReturnFailureBudget mdp varianceProxy baseVisitFloor burnin rounds ∧ forall trajectory, trajectory ∉ event -> (forall t, burnin <= t -> t < rounds -> forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t)).plan.upperValueRemaining mdp.horizon le_rfl state) ∧ |source.realizedSuccessorAverageRegret trajectory rounds| <= selfConsistentScheduledCausalBurninRealizedRegretRateEnvelope mdp varianceProxy baseVisitFloor burnin rounds

Realized successor-average regret process on one natural causal trajectory.

noncomputable def selfConsistentScheduledNaturalCausalRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real

Every coordinate of the natural causal regret process is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)

Natural causal realized successor-average regret converges in probability.

theorem selfConsistentScheduledCausalSource_realizedRegret_tendstoInMeasure_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)