BanditRLProof.RL.FiniteHorizonNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

Event on which the observed base-prefix average regret triggers early stopping.

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

Stop at the observed fourth-power prefix, or wait exactly `2*n+1` more prefixes.

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

The threshold-success branch stops at the observed base prefix.

theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_eq_base_of_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) (trajectory) (hthreshold : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityRounds scheduleIndex) trajectory <= threshold scheduleIndex) : selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory = (explicitHighProbabilityRounds scheduleIndex : WithTop Nat)

The threshold-failure branch waits to the right endpoint.

theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_eq_right_of_lt (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) (trajectory) (hthreshold : threshold scheduleIndex < selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityRounds scheduleIndex) trajectory) : selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory = (explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) : WithTop Nat)

The early-stop event is known at the fourth-power base prefix.

theorem measurableSet_selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowEarlyStopSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) : MeasurableSet[ selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityRounds scheduleIndex)] (selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowEarlyStopSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex)

The threshold-triggered two-endpoint rule is an exact natural-filtration stopping time.

theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_isStoppingTime (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex)

The threshold rule never stops before its observed base prefix.

theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_lower (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) (trajectory) : (explicitHighProbabilityRounds scheduleIndex : WithTop Nat) <= selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory

The threshold rule never exceeds the double-linear right endpoint.

theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_upper (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) : WithTop Nat)

The threshold rule never exceeds the double-linear right endpoint. -/ theorem selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_upper (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (threshold : Nat -> Real) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) : WithTop Nat) := by classical unfold selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix by_cases htrajectory : trajectory ∈ selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowEarlyStopSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex · simp [htrajectory] · simp [htrajectory] /- Terminal L1 theorem for the threshold-triggered choice between the fourth-power base prefix and its `2*n+1`-wider right endpoint.

theorem selfConsistentScheduledCausalSource_thresholdTriggeredDoubleLinearRawWindowStoppingTimeNaturalAverageRealizedBehaviorRegret_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) (threshold : Nat -> Real) : let stoppingPrefix := selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold 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 explicitHighProbabilityRounds (fun scheduleIndex => 2 * scheduleIndex + 1) let rate := selfConsistentScheduledNaturalCausalRateControlledRawWindowStoppingL1Rate mdp varianceProxy explicitHighProbabilityRounds (fun scheduleIndex => 2 * scheduleIndex + 1) 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)