BanditRLProof.RL.FiniteHorizonNaturalCausalGrowingWindowGridStoppingTimeL1AverageRealizedBehaviorRegretConsistency

The explicit fourth-power prefix grid is monotone in its index.

theorem explicitHighProbabilityRounds_mono {left right : Nat} (hle : left <= right) : explicitHighProbabilityRounds left <= explicitHighProbabilityRounds right

Every explicit fourth-power prefix at index `n + offset` dominates `n`.

theorem scheduleIndex_le_explicitHighProbabilityRounds_add (scheduleIndex offset : Nat) : scheduleIndex <= explicitHighProbabilityRounds (scheduleIndex + offset)

A grid-valued stopping prefix selects one finite window offset after `untopA`.

theorem exists_growingWindowGrid_offset_untopA_eq {Omega : Type*} (stoppingPrefix : Nat -> Omega -> WithTop Nat) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) (scheduleIndex : Nat) (trajectory : Omega) : exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ (stoppingPrefix scheduleIndex trajectory).untopA = explicitHighProbabilityRounds (scheduleIndex + offset)

Every grid-valued stopping prefix has a pointwise finite upper bound.

theorem growingWindowGrid_stoppingPrefix_le {Omega : Type*} (stoppingPrefix : Nat -> Omega -> WithTop Nat) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) (scheduleIndex : Nat) (trajectory : Omega) : stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds (scheduleIndex + windowAt scheduleIndex) : WithTop Nat)

Finite L1 budget for a window of fourth-power grid candidates.

noncomputable def selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget (mdp : MDP State Action) (varianceProxy : NNReal) (windowAt : Nat -> Nat) (scheduleIndex : Nat) : Real

Infinite shifted tail controlling every finite grid window.

noncomputable def selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Tail (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Real

Every finite growing-window grid budget is nonnegative.

theorem selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (windowAt : Nat -> Nat) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget mdp varianceProxy windowAt scheduleIndex

Every finite grid-window budget is bounded by the full shifted tail.

theorem selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget_le_tail (mdp : MDP State Action) (varianceProxy : NNReal) (windowAt : Nat -> Nat) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget mdp varianceProxy windowAt scheduleIndex <= selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Tail mdp varianceProxy scheduleIndex

The infinite shifted grid-envelope tail tends to zero.

theorem selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Tail_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Tail mdp varianceProxy) atTop (nhds 0)

Any finite grid-window budget vanishes, even when its width grows.

theorem selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (windowAt : Nat -> Nat) : Tendsto (selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget mdp varianceProxy windowAt) atTop (nhds 0)

Expected absolute value of the growing-window grid-stopped process.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret (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) : Real

Every grid-window stopped coordinate belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingAverageRealizedBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) (scheduleIndex : Nat) : MemLp (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

Expected absolute growing-window grid-stopped regret is nonnegative.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret_nonneg (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) : 0 <= selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex

The selected grid coordinate is bounded by the finite candidate budget.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret_le_budget (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) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex <= selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget mdp varianceProxy windowAt scheduleIndex

Expected absolute growing-window grid-stopped regret tends to zero.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret_tendsto_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) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix) atTop (nhds 0)

At exponent one, the stopped norm is its lifted expected absolute value.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingAverageRealizedBehaviorRegret_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) (scheduleIndex : Nat) : eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)

The grid-stopped process converges to zero in the exponent-one norm.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingAverageRealizedBehaviorRegret_sub_zero_tendsto_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) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) : Tendsto (fun scheduleIndex => eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex - (fun _ => 0)) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0)

The grid-stopped process converges to zero in the exponent-one norm. -/ theorem eLpNorm_one_selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingAverageRealizedBehaviorRegret_sub_zero_tendsto_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) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) : Tendsto (fun scheduleIndex => eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex - (fun _ => 0)) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0) := by have hexpected := selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret_tendsto_zero mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor stoppingPrefix hstopping windowAt hgrid have hofReal := (ENNReal.continuous_ofReal.tendsto 0).comp hexpected have hnorm : Tendsto (fun scheduleIndex => eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) atTop (nhds 0) := by have hnormEq : (fun scheduleIndex => eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure) = (fun scheduleIndex => ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)) := by funext scheduleIndex exact eLpNorm_one_selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingAverageRealizedBehaviorRegret_eq mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound stoppingPrefix hstopping windowAt hgrid scheduleIndex rw [hnormEq] simpa only [Function.comp_apply, ENNReal.ofReal_zero] using hofReal convert hnorm using 1 funext scheduleIndex apply eLpNorm_congr_ae exact Filter.Eventually.of_forall fun trajectory => by simp /- Terminal L1 theorem for an arbitrarily growing finite candidate window on the explicit fourth-power natural-prefix grid.

theorem selfConsistentScheduledCausalSource_growingWindowGridStoppingTimeNaturalAverageRealizedBehaviorRegret_L1_consistency (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) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (hstopping : forall scheduleIndex, IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) (windowAt : Nat -> Nat) (hwindowAt : Tendsto windowAt atTop atTop) (hgrid : forall scheduleIndex trajectory, exists offset, offset ∈ Finset.range (windowAt scheduleIndex + 1) /\ stoppingPrefix scheduleIndex trajectory = (explicitHighProbabilityRounds (scheduleIndex + offset) : WithTop Nat)) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let process := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppedProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let expectedAbsolute := selfConsistentScheduledNaturalCausalExpectedAbsoluteGrowingWindowGridStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let budget := selfConsistentScheduledNaturalCausalGrowingWindowGridStoppingL1Budget mdp varianceProxy windowAt Tendsto windowAt atTop atTop /\ StronglyAdapted (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) process /\ (forall scheduleIndex, Measurable (stoppedProcess scheduleIndex)) /\ (forall scheduleIndex, MemLp (stoppedProcess scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, expectedAbsolute scheduleIndex <= budget scheduleIndex) /\ Tendsto budget atTop (nhds 0) /\ Tendsto expectedAbsolute atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (stoppedProcess scheduleIndex - (fun _ => 0)) 1 source.trajectoryMeasure) atTop (nhds 0) /\ TendstoInMeasure source.trajectoryMeasure stoppedProcess atTop (fun _ => 0) /\ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun scheduleIndex => stoppedProcess scheduleIndex trajectory) atTop (nhds 0)