BanditRLProof.RL.FiniteHorizonAdaptiveEmpiricalOptimisticSource

All stage/state/action/next-state transition counts from one batch.

abbrev TransitionCountSummary (mdp : MDP State Action)

Compress an episode batch to the transition counts used by the planner.

def transitionCountSummary {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) : TransitionCountSummary mdp

The complete transition-count summary is measurable.

theorem measurable_transitionCountSummary {mdp : MDP State Action} {episodes : Nat} : Measurable (transitionCountSummary : EpisodeBatch mdp episodes -> TransitionCountSummary mdp)

Total visits represented by one state-action transition-count row.

def visitCount {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) : Nat

Normalized empirical transition PMF, with an explicit zero-count fallback.

noncomputable def empiricalTransitionPMF {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (stage : Fin mdp.horizon) (state : State) (action : Action) : PMF State

The summary-indexed empirical transition kernel.

noncomputable def empiricalTransitionKernel {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (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_isMarkov {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (stage : Fin mdp.horizon) : ProbabilityTheory.IsMarkovKernel (summary.empiricalTransitionKernel defaultState stage) where

Known-reward empirical-transition plan with zero reward radius and one fixed transition bonus at every coordinate.

noncomputable def optimisticPlan (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (transitionBonus : Real) : mdp.EstimatedModelPlan where

A deterministic action choice at every stage and state.

abbrev DeterministicMarkovPolicyTable (mdp : MDP State Action)

Interpret a deterministic action table as a Markov policy.

noncomputable def toMarkovPolicy {mdp : MDP State Action} (table : DeterministicMarkovPolicyTable mdp) : MarkovPolicy mdp where

The deterministic optimistic action table computed from a count summary.

noncomputable def optimisticPolicyTable (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (transitionBonus : Real) : DeterministicMarkovPolicyTable mdp

The action-table interpretation is exactly the plan's optimistic policy.

theorem optimisticPolicyTable_toMarkovPolicy (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (transitionBonus : Real) : (summary.optimisticPolicyTable mdp defaultState transitionBonus).toMarkovPolicy = (summary.optimisticPlan mdp defaultState transitionBonus).optimisticPolicy

The empirical optimistic action table computed from one observed batch.

noncomputable def empiricalOptimisticPolicyTable {mdp : MDP State Action} {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (transitionBonus : Real) : DeterministicMarkovPolicyTable mdp

The empirical optimistic table is measurable in the raw batch.

theorem measurable_empiricalOptimisticPolicyTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (transitionBonus : Real) : Measurable fun batch : EpisodeBatch mdp episodes => batch.empiricalOptimisticPolicyTable defaultState transitionBonus

Iid generated episode-batch law indexed by a deterministic policy table.

noncomputable def iidEpisodeBatchKernel {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.Kernel (DeterministicMarkovPolicyTable mdp) (EpisodeBatch mdp episodes)

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

theorem iidEpisodeBatchKernel_apply {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (table : DeterministicMarkovPolicyTable mdp) : iidEpisodeBatchKernel initialState episodes table = table.toMarkovPolicy.iidEpisodeBatchMeasure initialState episodes

The latest observed batch in a finite nonempty prefix.

def latestBatch {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) : EpisodeBatch 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 : EpisodeBatchPrefix mdp episodes n -> EpisodeBatch mdp episodes)

Optimistic table selected from the latest batch in a finite prefix.

noncomputable def successorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (transitionBonus : Real) (n : Nat) (history : EpisodeBatchPrefix 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) (transitionBonus : Real) (n : Nat) : Measurable (successorTable (mdp

Concrete adaptive source: after every batch, recompute the known-reward empirical-transition optimistic table from that batch and sample the next iid batch under the selected deterministic policy.

noncomputable def source (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) : AdaptiveEpisodeBatchSource mdp initialState episodes where

The selected policy is exactly the latest batch's optimistic plan policy.

theorem source_successorPolicy_eq_optimisticPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (n : Nat) (history : EpisodeBatchPrefix mdp episodes n) : (source mdp initialState episodes initialTable defaultState transitionBonus).successorPolicy n history = ((latestBatch history).transitionCountSummary.optimisticPlan mdp defaultState transitionBonus).optimisticPolicy

Measurability of a selected count event for any measurable finite policy-table selector. This discharges the regularity premise of the adaptive union route.

theorem measurableSet_selectedSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} {History : Type*} [MeasurableSpace History] (selector : History -> DeterministicMarkovPolicyTable mdp) (hselector : Measurable selector) (delta : Real) : MeasurableSet {pair : History × EpisodeBatch mdp episodes | pair.2 ∈ (selector pair.1).toMarkovPolicy.simultaneousCountBadEvent initialState episodes delta}

Every selected successor count event of the concrete source is measurable.

theorem source_measurableSet_successorSimultaneousCountBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (rounds : Nat) (delta : Real) (n : Nat) : MeasurableSet (AdaptiveEpisodeBatchSource.successorSimultaneousCountBadEvent (source mdp initialState episodes initialTable defaultState transitionBonus) rounds delta n)

The concrete source's next-batch conditional law is its latest empirical optimistic policy law.

theorem source_trajectoryMeasure_condDistrib_eq_empiricalOptimisticPolicyBatchLaw {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (n : Nat) : let concreteSource := source mdp initialState episodes initialTable defaultState transitionBonus Filter.EventuallyEq (ae (concreteSource.trajectoryMeasure.map (Preorder.frestrictLe n))) (ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => trajectory (n + 1)) (Preorder.frestrictLe n) concreteSource.trajectoryMeasure) (fun history => MarkovPolicy.iidEpisodeBatchMeasure ((latestBatch history).transitionCountSummary.optimisticPlan mdp defaultState transitionBonus).optimisticPolicy initialState episodes)

Concrete adaptive count-confidence terminal for the empirical optimistic source. No selected-law or successor-event measurability premise remains.

theorem source_trajectoryMeasure_adaptiveSimultaneousCountConfidence {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (transitionBonus : Real) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let concreteSource := source mdp initialState episodes initialTable defaultState transitionBonus MeasurableSet (concreteSource.adaptiveSimultaneousCountBadEvent rounds delta) ∧ concreteSource.trajectoryMeasure (concreteSource.adaptiveSimultaneousCountBadEvent rounds delta) <= ENNReal.ofReal delta ∧ forall trajectory, trajectory ∉ concreteSource.adaptiveSimultaneousCountBadEvent rounds delta -> forall round : Fin rounds, forall coordinate : CountCoordinate mdp, |coordinate.deviation (concreteSource.policyAt trajectory round) initialState (trajectory round)| < simultaneousCountConfidenceRadius mdp episodes (multiBatchLocalDelta rounds delta)