BanditRLProof.RL.FiniteHorizonNaturalCausalPolynomialBaseGrowingRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

A positive real number satisfies `1 + log x <= 2 * sqrt x`.

theorem one_add_log_le_two_mul_sqrt {x : Real} (hx : 0 < x) : 1 + Real.log x <= 2 * Real.sqrt x

The compiled logarithmic average rate admits an inverse-square-root bound.

theorem selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate_le_inverseSqrt (mdp : MDP State Action) (rounds : Nat) (hrounds : 0 < rounds) : selfConsistentScheduledNaturalCausalLogarithmicAverageIntegratedBehaviorExpectedRegretRate mdp rounds <= 2 * selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient mdp / Real.sqrt (rounds : Real)

Coefficient of the common inverse-square-root all-prefix L1 envelope.

noncomputable def selfConsistentScheduledNaturalCausalRawWindowL1Coefficient (mdp : MDP State Action) (varianceProxy : NNReal) : Real

Common inverse-square-root envelope used on every raw candidate prefix.

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

The common raw-window L1 coefficient is nonnegative.

theorem selfConsistentScheduledNaturalCausalRawWindowL1Coefficient_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) : 0 <= selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy

The exact all-prefix L1 envelope is bounded by the common inverse square root.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope_le_rawWindowInverseSqrtL1Envelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (hrounds : 0 < rounds) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretL1Envelope mdp varianceProxy baseVisitFloor rounds <= selfConsistentScheduledNaturalCausalRawWindowInverseSqrtL1Envelope mdp varianceProxy rounds

A raw prefix after the fourth-power base has square root at least `(n+1)^2`.

theorem explicitHighProbabilityScale_sq_le_sqrt_rounds_add (scheduleIndex offset : Nat) : (explicitHighProbabilityScale scheduleIndex : Real) ^ 2 <= Real.sqrt (explicitHighProbabilityRounds scheduleIndex + offset : Nat)

Every candidate in the raw window costs at most one inverse-square term.

theorem selfConsistentScheduledNaturalCausalRawWindowInverseSqrtL1Envelope_add_le_inverseSquare (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex offset : Nat) : selfConsistentScheduledNaturalCausalRawWindowInverseSqrtL1Envelope mdp varianceProxy (explicitHighProbabilityRounds scheduleIndex + offset) <= selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy / (explicitHighProbabilityScale scheduleIndex : Real) ^ 2

L1 budget over all raw prefixes from `(n+1)^4` through `(n+1)^4+n`.

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

The finite raw-window L1 budget is nonnegative.

theorem selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor scheduleIndex

The `n+1` raw candidates have total budget at most `D/(n+1)`.

theorem selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget_le_rate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor scheduleIndex <= selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy / (explicitHighProbabilityScale scheduleIndex : Real)

The explicit `D/(n+1)` raw-window budget rate tends to zero.

theorem selfConsistentScheduledNaturalCausalRawWindowL1Rate_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (fun scheduleIndex => selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy / (explicitHighProbabilityScale scheduleIndex : Real)) atTop (nhds 0)

The finite growing raw-window L1 budget tends to zero.

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

The WithTop bounds select one raw natural prefix in the growing window.

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

Expected absolute value of the polynomial-base raw-window stopped process.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret (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 polynomial-base raw-window stopped coordinate belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret (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)) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : 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 polynomial-base raw-window stopped regret is nonnegative.

theorem selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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 <= selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex

The selected raw coordinate is bounded by the finite candidate L1 budget.

theorem selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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)) (hstoppingLower : forall scheduleIndex trajectory, (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : WithTop Nat)) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex <= selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor scheduleIndex

Expected absolute raw-window stopped regret tends to zero.

theorem selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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)) (hstoppingLower : forall scheduleIndex trajectory, (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : WithTop Nat)) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix) atTop (nhds 0)

At exponent one, the raw-window stopped norm is its expected absolute value.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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)) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : 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 (selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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)) (hstoppingLower : forall scheduleIndex trajectory, (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : 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 raw-window stopped process converges to zero in the exponent-one norm. -/ theorem eLpNorm_one_selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_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)) (hstoppingLower : forall scheduleIndex trajectory, (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : 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 := selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_tendsto_zero mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor stoppingPrefix hstopping hstoppingLower hstoppingUpper 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 (selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)) := by funext scheduleIndex exact eLpNorm_one_selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret_eq mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound stoppingPrefix hstopping hstoppingUpper 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 the contiguous raw window from `(n+1)^4` through `(n+1)^4+n` on the exact natural causal source.

theorem selfConsistentScheduledCausalSource_explicitPolynomialBaseGrowingRawWindowStoppingTimeNaturalAverageRealizedBehaviorRegret_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)) (hstoppingLower : forall scheduleIndex trajectory, (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + scheduleIndex : 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 := selfConsistentScheduledNaturalCausalExpectedAbsolutePolynomialBaseGrowingRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let budget := selfConsistentScheduledNaturalCausalPolynomialBaseGrowingRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor let rate := fun scheduleIndex => selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy / (explicitHighProbabilityScale scheduleIndex : Real) Tendsto (fun scheduleIndex : Nat => scheduleIndex) 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) /\ (forall scheduleIndex, budget scheduleIndex <= rate 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)