Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceAlmostSureBehaviorExpectedRegretConsistency
# Natural-causal almost-sure behavior expected-regret consistency This module proves that the actual exploratory successor policy's expected regret tends to zero along almost every trajectory of the one heterogeneous causal source. The key project-local leaf extracts a pointwise behavior- policy rate from the existing coordinate confidence proof. First Borel-Cantelli supplies eventual model-goodness, and the deterministic causal planning rate then squeezes the nonnegative behavior regret to zero. Regularity is unchanged from the almost-sure realized-regret parent: finite nonempty Standard Borel State/Action, probability initial law, positive horizon, reward proxy and base visit floor, bounded stored means, uniform mean-compatible selected-reward sub-Gaussianity, and full-exploration path support. Failure policy: preserve the one dependent source, actual sampled coordinates, `n`-prefix to `n+1` behavior selection, scheduled budgets, and the distinction between the empirical model's recommended policy and the source's exploratory successor policy. The behavior expected-regret process is not claimed measurable here, so this route proves an a.e. pathwise limit but no new in-measure or `Lp` statement. It also gives no every-trajectory, anytime, reachability, minimax, or complete-UCB-VI result.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretInMeasureConsistency, BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureConsistency
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_successorPolicyAt_expectedRegret_le_rateAt_of_not_mem_modelRoundBadEvent
Compiled
A model-good coordinate bounds the actual successor policy by the causal rate.
theorem selfConsistentScheduledCausalSource_successorPolicyAt_expectedRegret_le_rateAt_of_not_mem_modelRoundBadEvent (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) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (t : Nat) (hnot : trajectory ∉ selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (source.successorPolicyAt trajectory t).expectedRegret initialState <= selfConsistentScheduledCausalPlanningRateAt mdp t
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess
Compiled
Expected regret of the actual exploratory successor policy at one coordinate.
noncomputable def selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (t : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s) -> Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_nonneg
Compiled
Every actual successor-policy expected-regret coordinate is nonnegative.
theorem selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (t : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) : 0 <= selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t trajectory
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_successorPolicyExpectedRegret_tendstoAlmostEverywhere_zero
Compiled
Actual successor-policy expected regret converges to zero almost surely.
theorem selfConsistentScheduledCausalSource_successorPolicyExpectedRegret_tendstoAlmostEverywhere_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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun t => selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t trajectory) atTop (nhds 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_eventually_modelOptimistic_and_behaviorExpected_and_realizedRegret_tendstoAlmostEverywhere_zero
Compiled
Eventual optimism and expected/realized behavior consistency hold jointly a.e.
theorem selfConsistentScheduledCausalSource_eventually_modelOptimistic_and_behaviorExpected_and_realizedRegret_tendstoAlmostEverywhere_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) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, (∀ᶠ t in atTop, let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) ∧ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState) ∧ Tendsto (fun t => selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t trajectory) atTop (nhds 0) ∧ Tendsto (fun rounds => selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)