BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedAverageSampledReturnExpectedOptimality

Observed sample mean in successor batch `t + 1`. Lean's division on `Real` is total, so a zero-size successor batch gives zero. The self-consistent scheduled source used below has positive batch sizes.

noncomputable def naturalSuccessorBatchAverageSampledReturn {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (_source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (t : Nat) : Real

Average of observed successor-batch sample means over a natural prefix. At the empty prefix it uses the optimal initial expected return.

noncomputable def naturalAverageSampledReturn {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

At every prefix, observed average return is optimal value minus realized regret. The empty-prefix convention makes the identity valid at zero.

theorem naturalAverageSampledReturn_eq_optimal_sub_naturalAverageRealizedBehaviorRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.naturalAverageSampledReturn trajectory rounds = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - source.naturalAverageRealizedBehaviorRegret trajectory rounds

A fixed-prefix average sampled-return coordinate is measurable.

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

A fixed-prefix average sampled return is measurable at its natural filtration level.

theorem measurable_naturalAverageSampledReturn_naturalTrajectoryFiltration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : @Measurable (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) Real (source.naturalTrajectoryFiltration rounds) inferInstance (fun trajectory => source.naturalAverageSampledReturn trajectory rounds)

The natural average sampled-return process is strongly adapted.

theorem naturalAverageSampledReturn_stronglyAdapted_naturalTrajectoryFiltration {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : StronglyAdapted source.naturalTrajectoryFiltration (fun rounds trajectory => source.naturalAverageSampledReturn trajectory rounds)

Natural-prefix average of the observed successor-batch sample means for the self-consistent causal source.

noncomputable def selfConsistentScheduledNaturalCausalAverageSampledReturnProcess (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

The project-specific sampled-return process is exactly the complement of the average realized-regret process.

theorem selfConsistentScheduledNaturalCausalAverageSampledReturnProcess_eq_optimal_sub_realized (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (trajectory) : selfConsistentScheduledNaturalCausalAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory

The self-consistent sampled-return process is strongly adapted to the exact natural trajectory filtration.

theorem selfConsistentScheduledNaturalCausalAverageSampledReturnProcess_stronglyAdapted (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : StronglyAdapted (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (selfConsistentScheduledNaturalCausalAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor)

Average sampled return evaluated at a `WithTop Nat` stopping prefix.

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

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

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess_apply (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory = selfConsistentScheduledNaturalCausalAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (stoppingPrefix scheduleIndex trajectory).untopA trajectory

Stopping preserves the exact sampled-return/realized-regret complement.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess_eq_optimal_sub_realized (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory

Mathlib stopped-value measurability for the sampled-return process.

theorem measurable_selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (hstopping : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) : Measurable (selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)

Integrability of stopped realized regret transfers to stopped sampled return under any finite measure.

theorem integrable_selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess_of_integrable_realized {Omega : Type w} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (optimal : Real) (sampledReturn realizedRegret : Omega -> Real) (hpoint : forall omega, sampledReturn omega = optimal - realizedRegret omega) (hrealized : Integrable realizedRegret mu) : Integrable sampledReturn mu

The corresponding Bochner expectation is the optimal constant minus the expected realized regret.

theorem integral_selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess_eq_optimal_sub_realized {Omega : Type w} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (optimal : Real) (sampledReturn realizedRegret : Omega -> Real) (hpoint : forall omega, sampledReturn omega = optimal - realizedRegret omega) (hrealized : Integrable realizedRegret mu) : integral mu sampledReturn = optimal - integral mu realizedRegret

The capped inverse-sqrt first-passage sampled-return coordinate is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturn (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Integrable (sampledReturn scheduleIndex) source.trajectoryMeasure

The genuine uncapped `hittingAfter` sampled-return coordinate is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturn (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Integrable (sampledReturn scheduleIndex) source.trajectoryMeasure

For the capped prefix, expected sampled return is exactly optimal value minus expected realized regret.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnIntegral_eq_optimal_sub_realized (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let realizedRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (sampledReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (realizedRegret scheduleIndex)

For the uncapped prefix, expected sampled return is exactly optimal value minus expected realized regret.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnIntegral_eq_optimal_sub_realized (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let realizedRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (sampledReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (realizedRegret scheduleIndex)

Expected sampled return at the capped prefix converges to the optimal initial expected return.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnIntegral_tendsto_optimal (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (sampledReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState))

Expected sampled return at the genuine uncapped `hittingAfter` prefix converges to the optimal initial expected return.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnIntegral_tendsto_optimal (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (sampledReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState))

Terminal sampled-return semantics and expected-optimality package for the capped approximation and the genuine uncapped stopping prefix.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedAverageSampledReturn_expected_optimality (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 : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let cappedStoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let uncappedStoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let cappedSampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedSampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedRealizedRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedRealizedRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix (forall scheduleIndex trajectory, cappedSampledReturn scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - cappedRealizedRegret scheduleIndex trajectory /\ uncappedSampledReturn scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - uncappedRealizedRegret scheduleIndex trajectory) /\ (forall scheduleIndex, Integrable (cappedSampledReturn scheduleIndex) source.trajectoryMeasure /\ Integrable (uncappedSampledReturn scheduleIndex) source.trajectoryMeasure) /\ (forall scheduleIndex, integral source.trajectoryMeasure (cappedSampledReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (cappedRealizedRegret scheduleIndex) /\ integral source.trajectoryMeasure (uncappedSampledReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (uncappedRealizedRegret scheduleIndex)) /\ Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (cappedSampledReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState)) /\ Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (uncappedSampledReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState))