Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCommonSpaceConsistency
# Common-space consistency for actual-sampled self-consistent optimism Target theorem route: place the complete actual-sampled scheduled experiments on one exact-marginal dependent product space and prove that realized successor- average regret converges to zero in Mathlib `TendstoInMeasure`. Supporting obligations are: 1. strengthen the finite-window terminal from a one-sided realized bound to an absolute bound using the model-good expected-regret certificate and the return-good two-sided deviation certificate; 2. construct the scheduled window source/law and its `Measure.infinitePi` coupling; 3. transport the measurable bad event and regret bound through coordinate evaluation; and 4. squeeze the distance event by the explicit failure and regret envelopes. Local APIs/imports are the compiled self-consistent explicit-rate terminal, the self-consistent expected-regret occupancy identity, the stochastic realized decomposition, `Measure.infinitePi_map_eval`, `measurePreserving_eval_infinitePi`, and `tendstoInMeasure_iff_dist`. Retrieval found no existing actual-sampled self-consistent common-space route; the general evidence is project-local plus `MLIB-PROBABILITY-KERNEL`, `MLIB-MEASURE-INTEGRAL`, `MLIB-METRIC-TOPOLOGY`, and `MLIB-ASYMPTOTICS`. Regularity is unchanged from the finite terminal: finite nonempty measurable State/Action with equality and measurable singletons, Standard Borel State/Action, a probability initial law, positive horizon/base floor/reward proxy, a uniform selected-reward sub-Gaussian law, bounded means, and a full- exploration path floor. Failure policy: preserve actual sampled rewards, successor indexing, initial batch exclusion, all three confidence shares, global centering, and `episodes * rounds` normalization. The product coupling below has exact window marginals but is intentionally independent across complete windows. It is not a nested causal stream and proves no pathwise, almost-sure, anytime, minimax, state-reachability, or complete-UCB-VI claim.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentExplicitRate, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardCumulativeDecayingExplorationCommonSpaceConsistency
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_absoluteRealizedSuccessorAverageRegret
Compiled
Actual-sampled optimism and an absolute realized-regret explicit rate.
theorem exploratorySource_trajectoryMeasure_selfConsistentScheduledExplicitRate_allCoordinateConfidence_optimism_and_absoluteRealizedSuccessorAverageRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (n : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let episodes := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n let rewardBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor n let transitionBudget := AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor n let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let modelBadEvent := source.adaptiveAllCoordinateEmpiricalModelBadEvent rounds varianceProxy delta delta let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds 1 varianceProxy delta let combinedBadEvent := modelBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveStochasticSampledEmpiricalOptimisticPlanAt trajectory defaultState rewardBudget transitionBudget round).upperValueRemaining mdp.horizon le_rfl state) /\ |source.realizedSuccessorAverageRegret trajectory rounds| <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n
abbrev
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.SelfConsistentScheduledStochasticWindowSpace
Compiled
One complete actual-sampled self-consistent experiment at each coordinate.
abbrev SelfConsistentScheduledStochasticWindowSpace (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real)
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticWindowSource
Compiled
The actual-sampled self-consistent source at schedule coordinate `n`.
noncomputable def selfConsistentScheduledStochasticWindowSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : AdaptiveStochasticEpisodeBatchSource mdp initialState (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n)
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticWindowMeasure
Compiled
The actual-sampled self-consistent trajectory law at coordinate `n`.
noncomputable def selfConsistentScheduledStochasticWindowMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Measure (StochasticEpisodeBatchTrajectory mdp (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n))
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticCommonMeasure
Compiled
Independent product coupling of the complete self-consistent window laws.
noncomputable def selfConsistentScheduledStochasticCommonMeasure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) : Measure (SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticCommonMeasure_map_eval
Compiled
Each common-space coordinate has exactly its scheduled trajectory law.
theorem selfConsistentScheduledStochasticCommonMeasure_map_eval (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).map (fun omega => omega n) = selfConsistentScheduledStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticRealizedRegretProcess
Compiled
Scheduled actual-sampled realized successor-average regret.
noncomputable def selfConsistentScheduledStochasticRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) (omega : SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor) : Real
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledStochasticRealizedRegretProcess
Compiled
Every coordinate of the scheduled actual-sampled regret is measurable.
theorem measurable_selfConsistentScheduledStochasticRealizedRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Measurable (selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticCommonBadEvent
Compiled
Pull the model/global-return union at coordinate `n` to the common space.
noncomputable def selfConsistentScheduledStochasticCommonBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Set (SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor)
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledStochasticCommonMeasure_badEvent_le
Compiled
The pulled-back bad event inherits the explicit finite-window failure rate.
theorem selfConsistentScheduledStochasticCommonMeasure_badEvent_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedFailureRateEnvelope n
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.abs_selfConsistentScheduledStochasticRealizedRegretProcess_le_of_not_mem_badEvent
Compiled
Outside the pulled-back event, coordinate `n` has the absolute rate bound.
theorem abs_selfConsistentScheduledStochasticRealizedRegretProcess_le_of_not_mem_badEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) (omega : SelfConsistentScheduledStochasticWindowSpace mdp varianceProxy baseVisitFloor) (homega : omega ∉ selfConsistentScheduledStochasticCommonBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) : |selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n omega| <= AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRealizedSuccessorAverageRegretRateEnvelope mdp varianceProxy n
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_selfConsistentScheduledStochasticCommonMeasure_marginals_and_realizedRegret_tendstoInMeasure_zero
Compiled
Terminal theorem: exact scheduled marginals and convergence in probability of actual-sampled realized successor-average regret to zero.
theorem exploratorySource_selfConsistentScheduledStochasticCommonMeasure_marginals_and_realizedRegret_tendstoInMeasure_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, Measurable (selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)) /\ (forall n, (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ).map (fun omega => omega n) = selfConsistentScheduledStochasticWindowMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) /\ TendstoInMeasure (selfConsistentScheduledStochasticCommonMeasure mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (selfConsistentScheduledStochasticRealizedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) atTop (fun _ => 0)