BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

# Threshold-triggered double-linear raw-window stopping-time L1 consistency At schedule index `n`, this module observes the compiled natural average realized behavior-regret process at the fourth-power prefix `(n+1)^4`. It stops at that prefix when the observation is at most a deterministic threshold and otherwise waits exactly `2*n+1` additional raw prefixes. The early-stop event is measurable in the exact natural filtration at the base prefix, so Mathlib's piecewise-constant constructor yields a genuine stopping time. The rate-controlled raw-window parent then gives the full L1, in-measure, and almost-everywhere consistency package. No optional-stopping identity or independence assumption is used.

Module map

Declarations
9
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalRateControlledRawWindowStoppingTimeL1AverageRealizedBehaviorRegretConsistency

Imported by

BanditRLProof

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowEarlyStopSet Compiled

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))
Source line 35 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix Compiled

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
Source line 56 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_eq_base_of_le Compiled

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)
Source line 80 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_eq_right_of_lt Compiled

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)
Source line 105 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowEarlyStopSet Compiled

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)
Source line 136 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_isStoppingTime Compiled

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)
Source line 173 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_lower Compiled

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
Source line 210 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalThresholdTriggeredDoubleLinearRawWindowStoppingPrefix_upper Compiled

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)
Source line 233 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_thresholdTriggeredDoubleLinearRawWindowStoppingTimeNaturalAverageRealizedBehaviorRegret_L1_consistency Compiled

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)
Source line 260 Chapter context: Finite-horizon RL