BanditRLProof.RL.FiniteHorizonEmpiricalModel

One recorded finite-horizon transition with its observed reward.

structure EpisodeStep (State : Type u) (Action : Type v) where

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

theorem measurable_state : Measurable (fun step : EpisodeStep State Action => step.state)

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

theorem measurable_action : Measurable (fun step : EpisodeStep State Action => step.action)

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

theorem measurable_reward : Measurable (fun step : EpisodeStep State Action => step.reward)

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

theorem measurable_nextState : Measurable (fun step : EpisodeStep State Action => step.nextState)

A finite table with one record at each valid stage of every episode. This raw type does not enforce cross-stage state continuity or identify the records with samples from the MDP trajectory law; those are downstream probabilistic laws.

abbrev EpisodeBatch (mdp : MDP State Action) (episodes : Nat)

Number of batch episodes visiting a state-action pair at one stage.

def visitCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : Nat

Sum of rewards recorded at a state-action pair and stage.

def rewardSum {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : Real

Empirical reward mean, with the conventional zero value at zero visits.

noncomputable def empiricalReward {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : Real

Number of matching transitions to a fixed next state.

def transitionCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Nat

Next-state transition counts partition the state-action visit count.

theorem sum_transitionCount_eq_visitCount {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (stage : Fin mdp.horizon) (state : State) (action : Action) : ∑ nextState, batch.transitionCount stage state action nextState = batch.visitCount stage state action

Empirical next-state PMF with an explicit zero-visit fallback state.

noncomputable def empiricalTransitionPMF {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : PMF State

Real singleton mass of the empirical transition PMF.

noncomputable def empiricalTransitionMass {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : Real

Zero-visit state-action pairs use the declared fallback distribution.

theorem empiricalTransitionPMF_eq_pure_of_visitCount_eq_zero {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (hzero : batch.visitCount stage state action = 0) : batch.empiricalTransitionPMF defaultState stage state action = PMF.pure defaultState

At a positive visit count, empirical PMF mass is normalized count.

theorem empiricalTransitionPMF_apply_of_visitCount_ne_zero {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (hvisit : batch.visitCount stage state action ≠ 0) : batch.empiricalTransitionPMF defaultState stage state action nextState = (batch.transitionCount stage state action nextState : ENNReal) / (batch.visitCount stage state action : ENNReal)

Real empirical singleton mass is the usual count divided by visit count.

theorem empiricalTransitionMass_eq_div_of_visitCount_ne_zero {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) (hvisit : batch.visitCount stage state action ≠ 0) : batch.empiricalTransitionMass defaultState stage state action nextState = (batch.transitionCount stage state action nextState : Real) / (batch.visitCount stage state action : Real)

State-action indexed empirical PMFs form a measurable finite-state kernel.

noncomputable def empiricalTransitionKernel {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) : ProbabilityTheory.Kernel (State × Action) State

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

theorem empiricalTransitionKernel_apply {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : batch.empiricalTransitionKernel defaultState stage (state, action) = (batch.empiricalTransitionPMF defaultState stage state action).toMeasure

Every section of the empirical transition kernel is a probability law.

theorem empiricalTransitionKernel_isMarkov {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) : ProbabilityTheory.IsMarkovKernel (batch.empiricalTransitionKernel defaultState stage) where

Kernel singleton mass agrees with the named empirical transition mass.

theorem empiricalTransitionKernel_real_singleton {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (batch.empiricalTransitionKernel defaultState stage (state, action)).real {nextState} = batch.empiricalTransitionMass defaultState stage state action nextState

A finite batch together with reward and transition radii. The empirical reward and transition model are derived from `batch`; zero transition counts use the explicit `defaultState` fallback rather than an implicit arbitrary law.

structure FiniteBatchModel (mdp : MDP State Action) (episodes : Nat) where

The estimated-model plan canonically generated by a finite episode batch.

noncomputable def plan {mdp : MDP State Action} {episodes : Nat} (model : FiniteBatchModel mdp episodes) : EstimatedModelPlan mdp where

Raw finite-batch confidence contracts. Reward errors and singleton-frequency errors are stated directly on the empirical statistics, while the envelope and radius-cover fields discharge the value-dependent coordinate transport.

structure Confidence {mdp : MDP State Action} {episodes : Nat} (model : FiniteBatchModel mdp episodes) where

Raw empirical-statistic confidence gives coordinate model confidence.

noncomputable def Confidence.toCoordinateConfidence {mdp : MDP State Action} {episodes : Nat} {model : FiniteBatchModel mdp episodes} (confidence : model.Confidence) : model.plan.CoordinateConfidence where

Route endpoint: finite-batch reward and singleton-frequency confidence imply global optimism and the compiled selected-radius expected-regret bound.

theorem Confidence.optimism_and_expectedRegret_le_two_occupancySelectedRadiusRemaining {mdp : MDP State Action} {episodes : Nat} {model : FiniteBatchModel mdp episodes} (confidence : model.Confidence) (initialState : Measure State) [IsProbabilityMeasure initialState] : (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ model.plan.optimisticPolicy.expectedRegret initialState <= model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState