Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalCommonSpaceBehaviorExpectedRegretInMeasureConsistency
# Natural-causal behavior expected-regret convergence in measure 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. Regularity is unchanged from the a.e. parent: finite nonempty Standard Borel State/Action, probability initial law, positive horizon/base visit floor/reward proxy, bounded stored means, uniform mean-compatible selected-reward sub- Gaussianity, and full-exploration path support. The generic selector lemma uses only finite measurable State/Action, measurable singletons, and a probability initial law. Failure policy: preserve the actual exploratory `source.successorPolicyAt`, the sampled-model recommendation/behavior distinction, the one dependent causal measure, `n`-prefix to `n+1` selection, and the existing a.e. route. This module proves coordinate measurability and convergence in measure, but does not derive `Lp`, expected-value, every-trajectory, anytime, reachability, minimax, optimal-rate, or complete-UCB-VI control.
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.
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.
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.
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.
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))