BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIClippedPlanner

A chronological action-value table for all actual decision stages.

abbrev QTable (mdp : MDP State Action)

The UCBVI-CH initialization `Q_{0,h}(x,a)=H`.

def initialQTable (mdp : MDP State Action) : QTable mdp

Sum a finite sequence of observed transition summaries coordinatewise.

def cumulativeSummaryOfSequence {mdp : MDP State Action} {n : Nat} (summaries : Fin n -> TransitionCountSummary mdp) : TransitionCountSummary mdp

The recursively selected clipped value with a given previous-episode Q table and one pooled empirical transition model. The index is decisions remaining; its successor case uses the chronological stage `H-(remaining+1)`.

noncomputable def clippedValueRemaining {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _state => 0 | remaining + 1, hremaining => let stage := mdp.decisionStageRemaining remaining hremaining let tail := clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega) let score : State -> Action -> Real := fun state action => let count := summary.aggregateVisitCount state action if count = 0 then (mdp.horizon : Real) else min (previousQ stage state action) (min (mdp.horizon : Real) (mdp.reward state action + (∫ nextState, tail nextState ∂ summary.aggregateEmpiricalTransitionKernel defaultState (state, action)) + bonusScale / Real.sqrt count)) fun state => score state (FiniteRealArgmax.choose (fun action => score state action)) /-- The action-value used at one remaining-horizon coordinate. -/ noncomputable def clippedQRemaining {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) : Real

The action-value used at one remaining-horizon coordinate.

noncomputable def clippedQRemaining {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) : Real

The complete chronological Q table produced by one recurrent update.

noncomputable def clippedQTable (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) : QTable mdp

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

theorem clippedQRemaining_of_aggregateVisitCount_eq_zero {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) (hzero : summary.aggregateVisitCount state action = 0) : clippedQRemaining previousQ summary defaultState bonusScale remaining hremaining state action = (mdp.horizon : Real)

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

theorem clippedQRemaining_of_aggregateVisitCount_pos {mdp : MDP State Action} (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) (hpos : 0 < summary.aggregateVisitCount state action) : clippedQRemaining previousQ summary defaultState bonusScale remaining hremaining state action = min (previousQ (mdp.decisionStageRemaining remaining hremaining) state action) (min (mdp.horizon : Real) (mdp.reward state action + (∫ nextState, clippedValueRemaining previousQ summary defaultState bonusScale remaining (by omega) nextState ∂ summary.aggregateEmpiricalTransitionKernel defaultState (state, action)) + bonusScale / Real.sqrt (summary.aggregateVisitCount state action)))

Fixed-enumeration argmax table of one recurrent Q update.

noncomputable def clippedPolicyTable (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) : DeterministicMarkovPolicyTable mdp

The selected recurrent action maximizes the actual clipped Q table.

theorem clippedQTable_le_selected (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (stage : Fin mdp.horizon) (state : State) (action : Action) : clippedQTable mdp previousQ summary defaultState bonusScale stage state action <= clippedQTable mdp previousQ summary defaultState bonusScale stage state (clippedPolicyTable mdp previousQ summary defaultState bonusScale stage state)

Every recurrent selector is measurable on the finite state space.

theorem measurable_clippedPolicyTable (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (stage : Fin mdp.horizon) : Measurable (clippedPolicyTable mdp previousQ summary defaultState bonusScale stage)

Fold observed summaries into the genuine sequence of previous-Q updates.

noncomputable def recurrentQTableOfSummaries (mdp : MDP State Action) (defaultState : State) (bonusScale : Real) : (n : Nat) -> (Fin n -> TransitionCountSummary mdp) -> QTable mdp | 0, _summaries => initialQTable mdp | n + 1, summaries => let previous := recurrentQTableOfSummaries mdp defaultState bonusScale n (fun i => summaries i.castSucc) let cumulative := cumulativeSummaryOfSequence summaries clippedQTable mdp previous cumulative defaultState bonusScale /-- Policy table obtained after the same finite previous-Q fold. -/ noncomputable def recurrentPolicyTableOfSummaries (mdp : MDP State Action) (defaultState : State) (bonusScale : Real) (n : Nat) (summaries : Fin n -> TransitionCountSummary mdp) : DeterministicMarkovPolicyTable mdp

Policy table obtained after the same finite previous-Q fold.

noncomputable def recurrentPolicyTableOfSummaries (mdp : MDP State Action) (defaultState : State) (bonusScale : Real) (n : Nat) (summaries : Fin n -> TransitionCountSummary mdp) : DeterministicMarkovPolicyTable mdp

Extract exactly the transition summaries stored in one finite prefix.

def prefixTransitionSummaries {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) : Fin (n + 1) -> TransitionCountSummary mdp

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

theorem measurable_prefixTransitionSummaries {mdp : MDP State Action} {episodes n : Nat} : Measurable (prefixTransitionSummaries : EpisodeBatchPrefix mdp episodes n -> Fin (n + 1) -> TransitionCountSummary mdp)

Measurable strict-prefix selector for the recurrent generated source.

noncomputable def recurrentSuccessorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (bonusScale : 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_recurrentSuccessorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (bonusScale : Real) (n : Nat) : Measurable (recurrentSuccessorTable (mdp := mdp) (episodes := episodes) defaultState bonusScale n)

The initial table is the fixed argmax of the all-`H` Q initialization.

noncomputable def recurrentInitialTable (mdp : MDP State Action) : DeterministicMarkovPolicyTable mdp

Canonical one-episode recurrent UCBVI source. It has no arbitrary initial policy parameter: coordinate zero executes `recurrentInitialTable`; coordinate `n+1` executes the fold of exactly the observed coordinates `0,...,n`.

noncomputable def recurrentSource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) : AdaptiveEpisodeBatchSource mdp initialState 1 where

Coordinate zero uses the all-`H` initialized recurrent policy.

theorem recurrentSource_policyAt_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) : (recurrentSource mdp initialState defaultState episodes delta).policyAt trajectory 0 = (recurrentInitialTable mdp).toMarkovPolicy

Every successor policy is the exact strict-prefix previous-Q fold.

theorem recurrentSource_policyAt_succ (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : (recurrentSource mdp initialState defaultState episodes delta).policyAt trajectory (n + 1) = (recurrentSuccessorTable defaultState (scale (State := State) (Action := Action) mdp episodes delta) n (Preorder.frestrictLe n trajectory)).toMarkovPolicy