BanditRLProof.RL.FiniteHorizonNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageVanishingDelayProbabilityAndL1Consistency

Reciprocal threshold `1/(n+1)` for the scheduled first-passage scan.

noncomputable def selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold (scheduleIndex : Nat) : Real

Every reciprocal first-passage threshold is strictly positive.

theorem selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold_pos (scheduleIndex : Nat) : 0 < selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold scheduleIndex

The reciprocal first-passage threshold tends to zero.

theorem selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold_tendsto_zero : Tendsto selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold atTop (nhds 0)

The capped first-passage stopping rule at the reciprocal threshold.

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

Event that reciprocal-threshold first passage does not stop at its base.

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

Probability of failing to stop at the first prefix in the scan window.

noncomputable def selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : ENNReal

Deterministic Markov rate for reciprocal-threshold first-passage delay.

noncomputable def selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : Real

Delay is exactly strict one-sided threshold violation at the base prefix.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet_eq (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex = {trajectory | selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold scheduleIndex < explicitPolynomialPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory}

The reciprocal-threshold delay event is measurable.

theorem measurableSet_selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : MeasurableSet (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex)

Delayed first passage is contained in the scheduled distance violation.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet_subset_distanceViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex ⊆ explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold scheduleIndex) scheduleIndex

Dividing the scheduled L1 envelope by the reciprocal threshold exposes an inverse-square plus inverse-linear delay rate.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate_eq (mdp : MDP State Action) (varianceProxy : NNReal) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate mdp varianceProxy scheduleIndex = 4 * selfConsistentScheduledNaturalCausalLogarithmicRateCoefficient mdp / (explicitHighProbabilityScale scheduleIndex : Real) ^ 2 + (2 * Real.sqrt (mdp.globalReturnDeviationPerEpisodeVarianceProxy 1 varianceProxy : Real) * Real.exp (1 / 2 : Real)) / (explicitHighProbabilityScale scheduleIndex : Real)

The scheduled expected absolute base process divided by the reciprocal threshold is bounded by the explicit delay rate.

theorem explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret_div_reciprocalFirstPassageThreshold_le_delayRate (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) (scheduleIndex : Nat) : explicitPolynomialPrefixExpectedAbsoluteAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex / selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold scheduleIndex <= selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate mdp varianceProxy scheduleIndex

The reciprocal-threshold delay rate tends to zero.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate mdp varianceProxy) atTop (nhds 0)

Markov control of the reciprocal-threshold first-passage delay event.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability_le_rate (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) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex <= ENNReal.ofReal (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate mdp varianceProxy scheduleIndex)

The probability of delaying beyond the first prefix tends to zero.

theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability_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) : Tendsto (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0)

The probability of delaying beyond the first prefix tends to zero. -/ theorem selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability_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) : Tendsto (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (nhds 0) := by exact tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds (by simpa only [ENNReal.ofReal_zero] using ENNReal.tendsto_ofReal (selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate_tendsto_zero mdp varianceProxy)) (Filter.Eventually.of_forall fun _ => bot_le) (Filter.Eventually.of_forall fun scheduleIndex => selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability_le_rate mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor scheduleIndex) /- The calibrated first-passage probability and complete stopped L1 terminal.

theorem selfConsistentScheduledCausalSource_reciprocalThresholdCappedDoubleLinearRawWindowFirstPassage_vanishingDelayProbability_and_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) : let threshold := selfConsistentScheduledNaturalCausalReciprocalFirstPassageThreshold let stoppingPrefix := selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor 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) let delayedSet := selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let delayedProbability := selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayedProbability mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let delayRate := selfConsistentScheduledNaturalCausalReciprocalThresholdCappedDoubleLinearRawWindowFirstPassageDelayRate mdp varianceProxy (forall scheduleIndex, 0 < threshold scheduleIndex) /\ Tendsto threshold atTop (nhds 0) /\ (forall scheduleIndex, MeasurableSet (delayedSet scheduleIndex)) /\ (forall scheduleIndex, delayedSet scheduleIndex ⊆ explicitPolynomialPrefixAverageRealizedBehaviorRegretDistanceViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (threshold scheduleIndex) scheduleIndex) /\ (forall scheduleIndex, delayedProbability scheduleIndex <= ENNReal.ofReal (delayRate scheduleIndex)) /\ Tendsto delayRate atTop (nhds 0) /\ Tendsto delayedProbability atTop (nhds 0) /\ 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)