BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

A finite `WithTop Nat` window selects one explicit natural offset.

theorem exists_window_offset_untopA_eq_of_withTop_bounds {Omega : Type*} (tau : Omega -> WithTop Nat) (start window : Nat) (htau_lower : forall omega, (start : WithTop Nat) <= tau omega) (htau_upper : forall omega, tau omega <= ((start + window : Nat) : WithTop Nat)) (omega : Omega) : exists offset, offset ∈ Finset.range (window + 1) /\ (tau omega).untopA = start + offset

Sum of the coordinate L1 envelopes over one fixed-width shifted window.

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

The fixed-window L1 budget is nonnegative.

theorem selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (window scheduleIndex : Nat) : 0 <= selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget mdp varianceProxy baseVisitFloor window scheduleIndex

Every fixed-width shifted finite sum of coordinate L1 envelopes vanishes.

theorem selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (window : Nat) : Tendsto (selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget mdp varianceProxy baseVisitFloor window) atTop (nhds 0)

Expected absolute value of the fixed-window stopped average process.

noncomputable def selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret (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 pointwise bounded stopped average process belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalBoundedWindowStoppingAverageRealizedBehaviorRegret (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)) (window scheduleIndex : Nat) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : WithTop Nat)) : MemLp (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure

Expected absolute stopped regret is nonnegative.

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

The selected stopped coordinate is bounded by the shifted finite L1 budget.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret_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)) (window scheduleIndex : Nat) (hstoppingLower : forall scheduleIndex trajectory, ((scheduleIndex + 1 : Nat) : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : WithTop Nat)) : selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex <= selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget mdp varianceProxy baseVisitFloor window scheduleIndex

Expected absolute stopped average regret tends to zero.

theorem selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret_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)) (window : Nat) (hstoppingLower : forall scheduleIndex trajectory, ((scheduleIndex + 1 : Nat) : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : WithTop Nat)) : Tendsto (selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret 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_selfConsistentScheduledNaturalCausalBoundedWindowStoppingAverageRealizedBehaviorRegret_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)) (window scheduleIndex : Nat) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : WithTop Nat)) : eLpNorm (selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex) 1 (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure = ENNReal.ofReal (selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)

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

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalBoundedWindowStoppingAverageRealizedBehaviorRegret_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)) (window : Nat) (hstoppingLower : forall scheduleIndex trajectory, ((scheduleIndex + 1 : Nat) : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : 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 stopped process converges to zero in the exponent-one extended norm. -/ theorem eLpNorm_one_selfConsistentScheduledNaturalCausalBoundedWindowStoppingAverageRealizedBehaviorRegret_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)) (window : Nat) (hstoppingLower : forall scheduleIndex trajectory, ((scheduleIndex + 1 : Nat) : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : 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 := selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret_tendsto_zero mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor stoppingPrefix hstopping window 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 (selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)) := by funext scheduleIndex exact eLpNorm_one_selfConsistentScheduledNaturalCausalBoundedWindowStoppingAverageRealizedBehaviorRegret_eq mdp initialState rewardSource varianceProxy law initialTable defaultState baseVisitFloor hrewardBound stoppingPrefix hstopping window scheduleIndex hstoppingUpper 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 fixed-window stopping-time L1 theorem for the exact per-batch-normalized, equal-round-weighted natural realized behavior-regret process.

theorem selfConsistentScheduledCausalSource_boundedWindowStoppingTimeNaturalAverageRealizedBehaviorRegret_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)) (window : Nat) (hstoppingLower : forall scheduleIndex trajectory, ((scheduleIndex + 1 : Nat) : WithTop Nat) <= stoppingPrefix scheduleIndex trajectory) (hstoppingUpper : forall scheduleIndex trajectory, stoppingPrefix scheduleIndex trajectory <= ((scheduleIndex + 1 + window : Nat) : 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 := selfConsistentScheduledNaturalCausalExpectedAbsoluteBoundedWindowStoppingAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let budget := selfConsistentScheduledNaturalCausalBoundedWindowStoppingL1Budget mdp varianceProxy baseVisitFloor window 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)