BanditRLProof.RL.FiniteHorizonNaturalCausalRateControlledRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

Sum of all coordinate L1 envelopes in a parameterized raw window.

noncomputable def selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (baseRounds windowWidth : Nat -> Nat) (scheduleIndex : Nat) : Real

Candidate-count times inverse-square-root rate for a raw window.

noncomputable def selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate (mdp : MDP State Action) (varianceProxy : NNReal) (baseRounds windowWidth : Nat -> Nat) (scheduleIndex : Nat) : Real

Adding a natural offset cannot decrease the square root of a base prefix.

theorem sqrt_baseRounds_le_sqrt_add (baseRounds offset : Nat) : Real.sqrt (baseRounds : Real) <= Real.sqrt (baseRounds + offset : Nat)

Every candidate envelope is controlled by the inverse square root of its base.

theorem selfConsistentScheduledNaturalCausalRawWindowInverseSqrtL1Envelope_add_le_base (mdp : MDP State Action) (varianceProxy : NNReal) (baseRounds offset : Nat) (hbaseRounds : 0 < baseRounds) : selfConsistentScheduledNaturalCausalRawWindowInverseSqrtL1Envelope mdp varianceProxy (baseRounds + offset) <= selfConsistentScheduledNaturalCausalRawWindowL1Coefficient mdp varianceProxy / Real.sqrt (baseRounds : Real)

A parameterized finite raw-window L1 budget is nonnegative.

theorem selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (baseRounds windowWidth : Nat -> Nat) (scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor baseRounds windowWidth scheduleIndex

The candidate sum is bounded by candidate count times the base envelope.

theorem selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget_le_rate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor baseRounds windowWidth scheduleIndex <= selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate mdp varianceProxy baseRounds windowWidth scheduleIndex

A vanishing candidate-count/base-square-root ratio gives a vanishing rate.

theorem selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseRounds windowWidth : Nat -> Nat) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) : Tendsto (selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate mdp varianceProxy baseRounds windowWidth) atTop (nhds 0)

The parameterized raw-window L1 budget tends to zero under the rate contract.

theorem selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) : Tendsto (selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor baseRounds windowWidth) atTop (nhds 0)

WithTop bounds select one candidate in a parameterized raw window.

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

The fourth-power base with width `n` satisfies the generic rate contract.

theorem explicitHighProbabilityRawWindowCandidateRate_tendsto_zero : Tendsto (fun scheduleIndex => (((scheduleIndex + 1 : Nat) : Real) / Real.sqrt (explicitHighProbabilityRounds scheduleIndex : Real))) atTop (nhds 0)

The fourth-power base also supports the strictly wider raw width `2*n+1`.

theorem explicitHighProbabilityDoubleLinearRawWindowCandidateRate_tendsto_zero : Tendsto (fun scheduleIndex => ((((2 * scheduleIndex + 1) + 1 : Nat) : Real) / Real.sqrt (explicitHighProbabilityRounds scheduleIndex : Real))) atTop (nhds 0)

Expected absolute value of a rate-controlled raw-window stopped process.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret (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 rate-controlled raw-window stopped coordinate belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingAverageRealizedBehaviorRegret (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) (baseRounds windowWidth : Nat -> Nat) (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 <= (baseRounds scheduleIndex + windowWidth 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 rate-controlled stopped regret is nonnegative.

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

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

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (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, (baseRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (baseRounds scheduleIndex + windowWidth scheduleIndex : WithTop Nat)) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex <= selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor baseRounds windowWidth scheduleIndex

Expected absolute rate-controlled stopped regret tends to zero.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) (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, (baseRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (baseRounds scheduleIndex + windowWidth scheduleIndex : WithTop Nat)) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix) atTop (nhds 0)

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (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 <= (baseRounds scheduleIndex + windowWidth 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 (selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)

The rate-controlled stopped process converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) (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, (baseRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (baseRounds scheduleIndex + windowWidth 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 rate-controlled stopped process converges to zero in `L1`. -/ theorem eLpNorm_one_selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) (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, (baseRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (baseRounds scheduleIndex + windowWidth 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 := selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_tendsto_zero mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor baseRounds windowWidth hbaseRounds hcandidateRate 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 (selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)) := by funext scheduleIndex exact eLpNorm_one_selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingAverageRealizedBehaviorRegret_eq mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound baseRounds windowWidth 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 deterministic parameterized raw windows satisfying the candidate-count/base-square-root rate and natural-prefix growth contracts.

theorem selfConsistentScheduledCausalSource_rateControlledRawWindowStoppingTimeNaturalAverageRealizedBehaviorRegret_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) (baseRounds windowWidth : Nat -> Nat) (hbaseRounds : forall scheduleIndex, 0 < baseRounds scheduleIndex) (hindexBase : forall scheduleIndex, scheduleIndex <= baseRounds scheduleIndex) (hcandidateRate : Tendsto (fun scheduleIndex => (((windowWidth scheduleIndex + 1 : Nat) : Real) / Real.sqrt (baseRounds scheduleIndex : Real))) atTop (nhds 0)) (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, (baseRounds scheduleIndex : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= (baseRounds scheduleIndex + windowWidth 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 := selfConsistentScheduledNaturalCausalExpectedAbsoluteRateControlledRawWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let budget := selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Budget mdp varianceProxy baseVisitFloor baseRounds windowWidth let rate := selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate mdp varianceProxy baseRounds windowWidth 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)