BanditRLProof.RL.FiniteHorizonNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingTimeL1AverageRealizedBehaviorRegretConsistency

The first natural prefix in the double-linear raw window whose observed average regret is at most the deterministic threshold, with right-end fallback.

noncomputable def selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat (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) -> Nat

The `WithTop Nat` surface consumed by Mathlib stopped-process APIs.

noncomputable def selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix (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

A specified first threshold hit is exactly the Mathlib finite hitting time.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat_eq_of_first_hit (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 candidate : Nat) (trajectory) (hcandidateLower : explicitHighProbabilityRounds scheduleIndex <= candidate) (hcandidateUpper : candidate <= explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1)) (hhit : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor candidate trajectory <= threshold scheduleIndex) (hfirst : forall earlier, explicitHighProbabilityRounds scheduleIndex <= earlier -> earlier < candidate -> threshold scheduleIndex < selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor earlier trajectory) : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory = candidate

If the base observation crosses the threshold, first passage is immediate.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat_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) : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory = explicitHighProbabilityRounds scheduleIndex

Without an earlier crossing, the capped first-passage rule returns the right endpoint.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat_eq_right_of_forall_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) (hbefore : forall earlier, explicitHighProbabilityRounds scheduleIndex <= earlier -> earlier < explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) -> threshold scheduleIndex < selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor earlier trajectory) : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory = explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1)

Every strict pre-stopping prefix in the window is above the threshold.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat_before_gt (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 earlier : Nat) (trajectory) (hlower : explicitHighProbabilityRounds scheduleIndex <= earlier) (hearlier : earlier < selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory) : threshold scheduleIndex < selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor earlier trajectory

A strict stop before the cap is an actual threshold hit.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat_le_threshold_of_lt_right (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) (hstopping : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory < explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1)) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory) trajectory <= threshold scheduleIndex

The capped first-passage rule is an exact natural-filtration stopping time.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix_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) (selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex)

The capped first-passage rule never stops before its fourth-power base.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix_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) <= selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory

The capped first-passage rule never exceeds its double-linear endpoint.

theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix_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) : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) : WithTop Nat)

The capped first-passage rule never exceeds its double-linear endpoint. -/ theorem selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix_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) : selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor threshold scheduleIndex trajectory <= (explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) : WithTop Nat) := by have hbaseRight : explicitHighProbabilityRounds scheduleIndex <= explicitHighProbabilityRounds scheduleIndex + (2 * scheduleIndex + 1) := Nat.le_add_right _ _ have hbound := (MeasureTheory.hittingBtwn_mem_Icc (u := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (s := Set.Iic (threshold scheduleIndex)) hbaseRight trajectory).2 unfold selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix unfold selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassagePrefixNat exact_mod_cast hbound /- Terminal L1 theorem for the genuine first-passage scan of the fourth-power base through its `2*n+1`-wider raw endpoint.

theorem selfConsistentScheduledCausalSource_cappedDoubleLinearRawWindowFirstPassageStoppingTimeNaturalAverageRealizedBehaviorRegret_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 := selfConsistentScheduledNaturalCausalCappedDoubleLinearRawWindowFirstPassageStoppingPrefix 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)