Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretInMeasureConsistency
This module closes the regularity boundary left by the a.e. behavior route. For a measurable finite policy-table selector, expected regret of the selected exploratory policy is measurable by a finite indicator-sum representation. The heterogeneous trajectory coordinate selector is already measurable, so every actual successor-policy expected-regret coordinate is measurable. Mathlib then transports the compiled a.e. limit to TendstoInMeasure on the same genuine dependent causal trajectory measure.
Module map
Imports
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretL1Consistency
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.DeterministicMarkovPolicyTable.measurable_exploratoryPolicy_expectedRegret_comp
Compiled
Expected regret after a measurable finite table selection is measurable.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.DeterministicMarkovPolicyTable.measurable_exploratoryPolicy_expectedRegret_compReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_exploratoryPolicy_expectedRegret_comp {Omega : Type w} [MeasurableSpace Omega] {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] (selector : Omega -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : Measurable fun omega => ((selector omega).exploratoryPolicy explorationRate hexplorationRate).expectedRegret initialState
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess
Compiled
Every actual causal successor-policy expected-regret coordinate is measurable.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcessReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measurable_selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (t : Nat) : Measurable (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_successorPolicyExpectedRegret_tendstoInMeasure_zero
Compiled
Actual successor-policy expected regret converges in measure to zero.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_successorPolicyExpectedRegret_tendstoInMeasure_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledCausalSource_successorPolicyExpectedRegret_tendstoInMeasure_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 (forall t, Measurable (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)) ∧ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_tendstoInMeasure_zero
Compiled
Actual behavior expected and realized regret both converge in measure.
Used in these reading views: Bandit Book · Reinforcement Learning Book
9. Finite-horizon reinforcement learning
Canonical node identity
declaration:BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_tendstoInMeasure_zeroReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem selfConsistentScheduledCausalSource_behaviorExpected_and_realizedRegret_tendstoInMeasure_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 ((forall t, Measurable (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t)) ∧ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalSuccessorPolicyExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)) ∧ ((forall rounds, Measurable (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ TendstoInMeasure source.trajectoryMeasure (selfConsistentScheduledNaturalCausalRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0))