BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityBurninLogRate

This module repairs the nonvanishing finite-prefix model budget in the fixed-prefix logarithmic realized-regret route. Model failures before a deterministic burnin are paid for by the uniform 2 * horizon behavior regret bound. Only the infinite model tail from burnin onward enters the probability event. The return component remains the fixed-prefix sum of successor-batch-average deviations, with each batch divided by its own positive scheduled episode count.

Module map

Declarations
16
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityLogRate

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityExplicitSchedule

Declarations

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

def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeBehaviorExpectedRegretLogarithmicRate Compiled

Uniform burn-in charge plus the compiled full logarithmic planning sum.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeBehaviorExpectedRegretLogarithmicRate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninCumulativeBehaviorExpectedRegretLogarithmicRate (mdp : MDP State Action) (burnin rounds : Nat) : Real
Source line 38 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelBadEvent Compiled

Outside the infinite model tail, only the first `burnin` natural rounds need the uniform `2 * horizon` charge. Every later round uses its actual coordinate model certificate.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelBadEvent (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (htrajectory : trajectory ∉ selfConsistentScheduledCausalTailModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin) : selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalBurninCumulativeBehaviorExpectedRegretLogarithmicRate mdp burnin rounds
Source line 50 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent Compiled

Infinite model tail after `burnin`, union the fixed-prefix normalized return deviation event.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 183 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninTailModelReturnFailureBudget Compiled

Exact infinite-tail model share plus caller-supplied return share.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninTailModelReturnFailureBudget

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninTailModelReturnFailureBudget (mdp : MDP State Action) (burnin : Nat) (returnDelta : Real) : ENNReal
Source line 201 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_naturalBurninTailModelReturnBadEvent_le Compiled

The joint burn-in tail event is measurable and has its exact union budget.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_naturalBurninTailModelReturnBadEvent_le

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_naturalBurninTailModelReturnBadEvent_le (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) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (burnin rounds : Nat) (hrounds : 0 < rounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta MeasurableSet event ∧ source.trajectoryMeasure event <= selfConsistentScheduledNaturalCausalBurninTailModelReturnFailureBudget mdp burnin returnDelta
Source line 208 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninRealizedCumulativeLogarithmicRate Compiled

Burn-in expected-regret envelope plus normalized return radius.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninRealizedCumulativeLogarithmicRate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninRealizedCumulativeLogarithmicRate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : Real
Source line 281 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninRealizedAverageLogarithmicRate Compiled

Positive-round average form of the burn-in realized rate.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninRealizedAverageLogarithmicRate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninRealizedAverageLogarithmicRate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : Real
Source line 293 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent Compiled

Outside the tail-model/return union, cumulative successor-batch-average realized behavior regret obeys the burn-in logarithmic envelope.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (returnDelta : Real) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta) : selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalBurninRealizedCumulativeLogarithmicRate mdp varianceProxy baseVisitFloor burnin rounds returnDelta
Source line 306 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent Compiled

Joint-good paths also obey the positive-round average burn-in rate.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_burnin_logarithmic_of_not_mem_tailModelReturnBadEvent (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) (returnDelta : Real) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalBurninRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor burnin rounds returnDelta
Source line 405 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet Compiled

One-sided cumulative burn-in realized-regret violation set.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 450 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet Compiled

One-sided average burn-in realized-regret violation set.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t))
Source line 470 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet Compiled

The cumulative burn-in violation set is measurable.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurableSet_selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : MeasurableSet (selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta)
Source line 490 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet Compiled

The average burn-in violation set is measurable.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurableSet_selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (burnin rounds : Nat) (returnDelta : Real) : MeasurableSet (selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta)
Source line 510 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent Compiled

Every cumulative burn-in violation belongs to the joint tail event.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (returnDelta : Real) : selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta ⊆ selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta
Source line 530 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent Compiled

Every average burn-in violation belongs to the joint tail event.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_tailModelReturnBadEvent (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) (returnDelta : Real) : selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta ⊆ selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta
Source line 564 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_burninTailHighProbabilityLogarithmicCumulativeAverageRealizedBehaviorRegret Compiled

Terminal burn-in tail high-probability logarithmic cumulative and average realized behavior-regret certificate.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_burninTailHighProbabilityLogarithmicCumulativeAverageRealizedBehaviorRegret

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem selfConsistentScheduledCausalSource_burninTailHighProbabilityLogarithmicCumulativeAverageRealizedBehaviorRegret (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) (burnin rounds : Nat) (hburnin : burnin <= rounds) (hrounds : 0 < rounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBurninTailModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta let cumulativeViolation := selfConsistentScheduledNaturalCausalBurninCumulativeRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta let averageViolation := selfConsistentScheduledNaturalCausalBurninAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor burnin rounds returnDelta let failureBudget := selfConsistentScheduledNaturalCausalBurninTailModelReturnFailureBudget mdp burnin returnDelta MeasurableSet event ∧ MeasurableSet cumulativeViolation ∧ MeasurableSet averageViolation ∧ source.trajectoryMeasure event <= failureBudget ∧ cumulativeViolation ⊆ event ∧ averageViolation ⊆ event ∧ source.trajectoryMeasure cumulativeViolation <= failureBudget ∧ source.trajectoryMeasure averageViolation <= failureBudget ∧ (failureBudget < 1 -> source.trajectoryMeasure event < 1 ∧ source.trajectoryMeasure cumulativeViolation < 1 ∧ source.trajectoryMeasure averageViolation < 1) ∧ forall trajectory, trajectory ∉ event -> selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalBurninRealizedCumulativeLogarithmicRate mdp varianceProxy baseVisitFloor burnin rounds returnDelta ∧ selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalBurninRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor burnin rounds returnDelta
Source line 601 Chapter context: Finite-horizon RL