BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityExplicitSchedule

Each positive-count normalized successor coordinate contributes at most one copy of the one-episode global return proxy.

theorem naturalCumulativeSuccessorAverageReturnVarianceProxy_le_rounds_mul (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hepisodes : forall n, 0 < episodes n) : naturalCumulativeSuccessorAverageReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy <= (rounds : NNReal) * mdp.globalReturnDeviationPerEpisodeVarianceProxy rewardBound rewardVarianceProxy

Positive scale used by the explicit prefix schedule.

def explicitHighProbabilityScale (n : Nat) : Nat

The model-tail burn-in is linear in the schedule scale.

def explicitHighProbabilityBurnin (n : Nat) : Nat

Natural successor prefixes are sampled along a fourth-power subsequence.

def explicitHighProbabilityRounds (n : Nat) : Nat

Exponentially vanishing fixed-prefix return failure share.

noncomputable def explicitHighProbabilityReturnDelta (n : Nat) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityScale_pos (n : Nat) : 0 < explicitHighProbabilityScale n

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityBurnin_le_rounds (n : Nat) : explicitHighProbabilityBurnin n <= explicitHighProbabilityRounds n

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityRounds_pos (n : Nat) : 0 < explicitHighProbabilityRounds n

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityReturnDelta_pos (n : Nat) : 0 < explicitHighProbabilityReturnDelta n

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityReturnDelta_le_one (n : Nat) : explicitHighProbabilityReturnDelta n <= 1

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityScale_tendsto_atTop : Tendsto explicitHighProbabilityScale atTop atTop

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityScale_real_tendsto_atTop : Tendsto (fun n => (explicitHighProbabilityScale n : Real)) atTop atTop

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityRounds_tendsto_atTop : Tendsto explicitHighProbabilityRounds atTop atTop

No declaration docstring is present; use the chapter context and exact statement below.

theorem explicitHighProbabilityReturnDelta_tendsto_zero : Tendsto explicitHighProbabilityReturnDelta atTop (nhds 0)

Self-consistent specialization of the generic own-count proxy bound.

theorem selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy_le_rounds_mul (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy mdp varianceProxy baseVisitFloor rounds <= (rounds : NNReal) * mdp.globalReturnDeviationPerEpisodeVarianceProxy 1 varianceProxy

Return-confidence contribution after division by the scheduled prefix.

noncomputable def explicitPolynomialPrefixAverageReturnRadius (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Real

A coarse `O(1 / scale)` envelope for the scheduled average radius.

theorem explicitPolynomialPrefixAverageReturnRadius_le (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : explicitPolynomialPrefixAverageReturnRadius mdp varianceProxy baseVisitFloor n <= 2 * (((mdp.globalReturnDeviationPerEpisodeVarianceProxy 1 varianceProxy : NNReal) : Real) + 1) / (explicitHighProbabilityScale n : Real)

The explicit fixed-prefix return confidence contribution vanishes.

theorem explicitPolynomialPrefixAverageReturnRadius_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (explicitPolynomialPrefixAverageReturnRadius mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Exact tail-model plus return-share budget along the explicit schedule.

noncomputable def explicitPolynomialPrefixTailModelReturnFailureBudget (mdp : MDP State Action) (n : Nat) : ENNReal

Scheduled positive-prefix average realized behavior-regret envelope.

noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretRate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Real

The exact union-bound failure budget vanishes along the schedule.

theorem explicitPolynomialPrefixTailModelReturnFailureBudget_tendsto_zero (mdp : MDP State Action) : Tendsto (explicitPolynomialPrefixTailModelReturnFailureBudget mdp) atTop (nhds 0)

The full scheduled average realized-regret envelope vanishes.

theorem explicitPolynomialPrefixAverageRealizedBehaviorRegretRate_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Scheduled model-tail/normalized-return union event.

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

Scheduled one-sided average realized behavior-regret violation set.

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

Scheduled one-sided average realized behavior-regret violation set. -/ noncomputable def explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) := selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityBurnin n) (explicitHighProbabilityRounds n) (explicitHighProbabilityReturnDelta n) /- Terminal scheduled-prefix high-probability average realized behavior-regret consistency certificate. It packages every fixed-prefix event and pathwise certificate together with the two vanishing deterministic envelopes.

theorem selfConsistentScheduledCausalSource_explicitPolynomialPrefixHighProbabilityAverageRealizedBehaviorRegretConsistency (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 source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := fun n => explicitPolynomialPrefixTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n let averageViolation := fun n => explicitPolynomialPrefixAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n Tendsto (explicitPolynomialPrefixTailModelReturnFailureBudget mdp) atTop (nhds 0) ∧ Tendsto (explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor) atTop (nhds 0) ∧ (∀ᶠ n in atTop, explicitPolynomialPrefixTailModelReturnFailureBudget mdp n < 1) ∧ forall n, MeasurableSet (event n) ∧ MeasurableSet (averageViolation n) ∧ source.trajectoryMeasure (event n) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n ∧ averageViolation n ⊆ event n ∧ source.trajectoryMeasure (averageViolation n) <= explicitPolynomialPrefixTailModelReturnFailureBudget mdp n ∧ (explicitPolynomialPrefixTailModelReturnFailureBudget mdp n < 1 -> source.trajectoryMeasure (event n) < 1 ∧ source.trajectoryMeasure (averageViolation n) < 1) ∧ forall trajectory, trajectory ∉ event n -> selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (explicitHighProbabilityRounds n) trajectory <= explicitPolynomialPrefixAverageRealizedBehaviorRegretRate mdp varianceProxy baseVisitFloor n