Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSource
# Adaptive sampled-reward empirical optimistic source This module constructs a genuinely sampled-reward adaptive optimistic source. The successor table is computed from the latest complete stochastic batch, including its observed rewards, rather than from the known-mean projection. The main regularity obligation is measurability of the finite-horizon dynamic program as a function of the sampled batch. The explicit finite argmax and a batch-indexed empirical transition kernel discharge that obligation. The resulting source has the exact selected-policy iid stochastic batch law in every history fiber by construction.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardEmpiricalOptimisticProjection, BanditRLProof.RL.FiniteHorizonStochasticRewardIIDAllCoordinateEmpiricalModelConfidence
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticConfidence
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_rewardSum
Compiled
A fixed sampled-reward sum is measurable on raw episode batches.
theorem measurable_rewardSum {mdp : MDP State Action} {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable fun batch : EpisodeBatch mdp episodes => batch.rewardSum stage state action
theorem
BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_empiricalReward
Compiled
A fixed empirical sampled-reward mean is measurable on raw batches.
theorem measurable_empiricalReward {mdp : MDP State Action} {episodes : Nat} (stage : Fin mdp.horizon) (state : State) (action : Action) : Measurable fun batch : EpisodeBatch mdp episodes => batch.empiricalReward stage state action
def
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.stateKernel
Compiled
A fixed empirical next-state law as a kernel in the count summary.
noncomputable def stateKernel {mdp : MDP State Action} (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.Kernel (TransitionCountSummary mdp) State
def
BanditRLProof.FiniteHorizonRL.EpisodeBatch.empiricalTransitionStateKernel
Compiled
The raw-batch empirical next-state law as a Markov kernel in the batch.
noncomputable def empiricalTransitionStateKernel {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : ProbabilityTheory.Kernel (EpisodeBatch mdp episodes) State
theorem
BanditRLProof.FiniteHorizonRL.EpisodeBatch.empiricalTransitionStateKernel_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem empiricalTransitionStateKernel_apply {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : empiricalTransitionStateKernel (episodes
theorem
BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_uncurry_of_forall_measurable
Compiled
Finite-state coordinatewise measurability yields joint measurability.
theorem measurable_uncurry_of_forall_measurable {Omega : Type*} [MeasurableSpace Omega] (value : Omega -> State -> Real) (hvalue : forall nextState : State, Measurable fun omega => value omega nextState) : Measurable (Function.uncurry value)
theorem
BanditRLProof.FiniteHorizonRL.EpisodeBatch.measurable_empiricalTransitionValue
Compiled
The empirical transition integral is measurable when every continuation-value coordinate is measurable in the same raw batch.
theorem measurable_empiricalTransitionValue {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (value : EpisodeBatch mdp episodes -> State -> Real) (hvalue : forall nextState : State, Measurable fun batch => value batch nextState) : Measurable fun batch : EpisodeBatch mdp episodes => ∫ nextState, value batch nextState ∂batch.empiricalTransitionKernel defaultState stage (state, action)
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_stochasticAllCoordinateEmpiricalOptimisticQ
Compiled
Every sampled empirical optimistic action-value coordinate is measurable.
theorem measurable_stochasticAllCoordinateEmpiricalOptimisticQ (mdp : MDP State Action) (episodes : Nat) (defaultState : State) (rewardBudget transitionBudget : Real) (stage : Fin mdp.horizon) (state : State) (action : Action) (value : EpisodeBatch mdp episodes -> State -> Real) (hvalue : forall nextState : State, Measurable fun batch => value batch nextState) : Measurable fun batch : EpisodeBatch mdp episodes => let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget model.plan.optimisticQ stage (value batch) state action
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_stochasticAllCoordinateEmpiricalUpperValueRemaining
Compiled
The sampled empirical optimistic value recursion is batch-measurable.
theorem measurable_stochasticAllCoordinateEmpiricalUpperValueRemaining (mdp : MDP State Action) (episodes : Nat) (defaultState : State) (rewardBudget transitionBudget : Real) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State), Measurable fun batch : EpisodeBatch mdp episodes => let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget model.plan.upperValueRemaining remaining hremaining state | 0, _hremaining, state => by simp [EstimatedModelPlan.upperValueRemaining] | remaining + 1, hremaining, state => by let stage := mdp.decisionStageRemaining remaining hremaining let value := fun batch : EpisodeBatch mdp episodes => let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget model.plan.upperValueRemaining remaining (by omega) have hvalue : forall nextState : State, Measurable fun batch => value batch nextState
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_stochasticAllCoordinateEmpiricalOptimisticActionAt
Compiled
Every chronological sampled empirical optimistic action is measurable.
theorem measurable_stochasticAllCoordinateEmpiricalOptimisticActionAt (mdp : MDP State Action) (episodes : Nat) (defaultState : State) (rewardBudget transitionBudget : Real) (stage : Fin mdp.horizon) (state : State) : Measurable fun batch : EpisodeBatch mdp episodes => let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget model.plan.optimisticActionAt stage state
theorem
BanditRLProof.FiniteHorizonRL.MDP.measurable_stochasticAllCoordinateEmpiricalOptimisticPolicyTable
Compiled
The complete sampled empirical optimistic policy table is measurable.
theorem measurable_stochasticAllCoordinateEmpiricalOptimisticPolicyTable (mdp : MDP State Action) (episodes : Nat) (defaultState : State) (rewardBudget transitionBudget : Real) : Measurable fun batch : EpisodeBatch mdp episodes => fun stage state => (mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget).plan |>.optimisticActionAt stage state
def
BanditRLProof.FiniteHorizonRL.StochasticEpisodeBatch.sampledEmpiricalOptimisticPolicyTable
Compiled
Optimistic table computed from the actual sampled rewards in one batch.
noncomputable def sampledEmpiricalOptimisticPolicyTable {mdp : MDP State Action} {episodes : Nat} (batch : StochasticEpisodeBatch mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) : DeterministicMarkovPolicyTable mdp
theorem
BanditRLProof.FiniteHorizonRL.StochasticEpisodeBatch.measurable_sampledEmpiricalOptimisticPolicyTable
Compiled
The sampled-reward optimistic table is measurable in the stochastic batch.
theorem measurable_sampledEmpiricalOptimisticPolicyTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (rewardBudget transitionBudget : Real) : Measurable fun batch : StochasticEpisodeBatch mdp episodes => batch.sampledEmpiricalOptimisticPolicyTable defaultState rewardBudget transitionBudget
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.latestBatch
Compiled
The latest complete stochastic batch in a finite nonempty prefix.
def latestBatch {mdp : MDP State Action} {episodes n : Nat} (history : StochasticEpisodeBatchPrefix mdp episodes n) : StochasticEpisodeBatch mdp episodes
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_latestBatch
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_latestBatch {mdp : MDP State Action} {episodes n : Nat} : Measurable (latestBatch : StochasticEpisodeBatchPrefix mdp episodes n -> StochasticEpisodeBatch mdp episodes)
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.successorTable
Compiled
Sampled-reward optimistic table selected from the latest stochastic batch.
noncomputable def successorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (rewardBudget transitionBudget : Real) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : DeterministicMarkovPolicyTable mdp
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_successorTable
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_successorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (rewardBudget transitionBudget : Real) (n : Nat) : Measurable (successorTable (mdp
def
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource
Compiled
Adaptive exploratory source whose successor policy uses actual sampled rewards.
noncomputable def exploratorySource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : AdaptiveStochasticEpisodeBatchSource mdp initialState episodes where
theorem
BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.exploratorySource_batchKernel_eq_selectedPolicy_iidLaw
Compiled
Every history fiber has the exact iid stochastic law of its selected policy.
theorem exploratorySource_batchKernel_eq_selectedPolicy_iidLaw {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Real) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : StochasticEpisodeBatchPrefix mdp episodes n) : let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate source.batchKernel n history = rewardSource.iidStochasticTrajectoryFamilyMeasure ((successorTable defaultState rewardBudget transitionBudget n history) |>.exploratoryPolicy explorationRate hexplorationRate) initialState episodes