Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRandomPrefixAverageRealizedBehaviorRegretAlmostSureConsistency

# Diverging random-prefix almost-sure natural causal consistency This module consumes the compiled deterministic all-prefix almost-sure theorem for the exact per-batch-normalized, equal-round-weighted natural average realized behavior-regret process. A countable random-index measurability wrapper makes every random-prefix evaluation measurable, while pathwise composition transports the limit through any measurable random-prefix schedule which diverges almost everywhere. This is random-subsequence transport on one dependent causal measure. It does not use optional stopping and does not prove an anytime confidence sequence, a stopping-time rate, raw single-episode regret, behavior/recommended-policy equality, minimax reachability, or complete UCB-VI.

Module map

Source: BanditRLProof/RL/FiniteHorizonNaturalCausalRandomPrefixAverageRealizedBehaviorRegretAlmostSureConsistency.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 8
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalStoppingTimeAverageRealizedBehaviorRegretAlmostSureConsistency

Declarations

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

theorem BanditRLProof.measurable_apply_randomNat Compiled

A countable random coordinate of a measurable process is measurable.

theorem measurable_apply_randomNat {Omega : Type w} {Beta : Type x} [MeasurableSpace Omega] [MeasurableSpace Beta] (process : Nat -> Omega -> Beta) (randomIndex : Omega -> Nat) (hprocess : forall n, Measurable (process n)) (hrandomIndex : Measurable randomIndex) : Measurable (fun omega => process (randomIndex omega) omega)

Source line 27 Chapter context: Finite-horizon RL

theorem BanditRLProof.ae_tendsto_apply_randomPrefix Compiled

An almost-everywhere limit survives an almost-everywhere diverging random prefix.

theorem ae_tendsto_apply_randomPrefix {Omega : Type w} {Beta : Type x} [MeasurableSpace Omega] [TopologicalSpace Beta] {mu : Measure Omega} {process : Nat -> Omega -> Beta} {randomPrefix : Nat -> Omega -> Nat} {z : Beta} (hprocess : ∀ᵐ omega ∂mu, Tendsto (fun n => process n omega) atTop (nhds z)) (hrandomPrefix : ∀ᵐ omega ∂mu, Tendsto (fun n => randomPrefix n omega) atTop atTop) : ∀ᵐ omega ∂mu, Tendsto (fun n => process (randomPrefix n omega) omega) atTop (nhds z)

Source line 41 Chapter context: Finite-horizon RL

theorem BanditRLProof.tendsto_randomPrefix_atTop_of_nat_le Compiled

A pointwise deterministic lower envelope forces a Nat-valued random prefix to diverge.

theorem tendsto_randomPrefix_atTop_of_nat_le {Omega : Type w} (randomPrefix : Nat -> Omega -> Nat) (hlower : forall n omega, n <= randomPrefix n omega) (omega : Omega) : Tendsto (fun n => randomPrefix n omega) atTop atTop

Source line 56 Chapter context: Finite-horizon RL

def

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess

Compiled

The exact natural average realized behavior regret at a random prefix.

noncomputable def selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (randomPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Nat) (scheduleIndex : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real

Source line 78 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess_apply

Compiled

No declaration docstring is present; use the chapter context and exact statement below.

theorem selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess_apply (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (randomPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Nat) (scheduleIndex : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix scheduleIndex trajectory = selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (randomPrefix scheduleIndex trajectory) trajectory

Source line 101 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess

Compiled

Every coordinate of the exact random-prefix process is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (randomPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Nat) (scheduleIndex : Nat) (hrandomPrefix : Measurable (randomPrefix scheduleIndex)) : Measurable (selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix scheduleIndex)

Source line 127 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_randomPrefixNaturalAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero

Compiled

The exact natural average realized behavior regret remains almost-surely consistent at every measurable random prefix which diverges almost everywhere.

theorem selfConsistentScheduledCausalSource_randomPrefixNaturalAverageRealizedBehaviorRegret_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) (randomPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Nat) (hrandomPrefixMeasurable : forall n, Measurable (randomPrefix n)) (hrandomPrefixDiverges : ∀ᵐ trajectory ∂ (selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor).trajectoryMeasure, Tendsto (fun n => randomPrefix n trajectory) atTop atTop) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall n, Measurable (selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix n)) /\ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun n => selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix n trajectory) atTop (nhds 0)

Source line 161 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_randomPrefixNaturalAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero_of_nat_le

Compiled

A pointwise lower envelope is a practical sufficient random-prefix contract.

theorem selfConsistentScheduledCausalSource_randomPrefixNaturalAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero_of_nat_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) (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) (randomPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Nat) (hrandomPrefixMeasurable : forall n, Measurable (randomPrefix n)) (hrandomPrefixLower : forall n trajectory, n <= randomPrefix n trajectory) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall n, Measurable (selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix n)) /\ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun n => selfConsistentScheduledNaturalCausalRandomPrefixAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor randomPrefix n trajectory) atTop (nhds 0)

Source line 221 Chapter context: Finite-horizon RL