BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSource

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

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

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

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

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 := episodes) defaultState stage state action batch = batch.empiricalTransitionKernel defaultState stage (state, action)

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)

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)

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

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

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

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

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

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

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

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)

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

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 := mdp) (episodes := episodes) defaultState rewardBudget transitionBudget n)

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

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