BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeHoeffdingUCBVI

Reward sums indexed by stage, state, and action.

abbrev RewardSumSummary (mdp : MDP State Action)

The cumulative empirical-model state needed by UCB-VI: transition counts and sampled reward sums. State-action visit counts are derived from the transition summary, so they cannot drift away from the transition counts.

abbrev AdaptiveCumulativeEmpiricalModelState (mdp : MDP State Action)

UCBVI-CH state-action visits aggregated across every stage.

abbrev AggregateVisitCountSummary

Sum a stage-indexed transition summary into the paper count `N_k(x,a)`.

def aggregateVisitCount {mdp : MDP State Action} (summary : TransitionCountSummary mdp) : AggregateVisitCountSummary (State := State) (Action := Action)

The complete cross-stage aggregate count view is measurable.

theorem measurable_aggregateVisitCount {mdp : MDP State Action} : Measurable (aggregateVisitCount : TransitionCountSummary mdp -> AggregateVisitCountSummary (State := State) (Action := Action))

Sum every reward coordinate in a nonempty finite generated-batch prefix.

def cumulativeRewardSumSummary {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) : RewardSumSummary mdp

A fixed batch reward sum is measurable.

theorem measurable_rewardSum_coordinate {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

The complete cumulative reward-sum table is history measurable.

theorem measurable_cumulativeRewardSumSummary {mdp : MDP State Action} {episodes n : Nat} : Measurable (cumulativeRewardSumSummary : EpisodeBatchPrefix mdp episodes n -> RewardSumSummary mdp)

Cumulative transition counts and reward sums from exactly the same prefix.

def cumulativeEmpiricalModelState {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) : AdaptiveCumulativeEmpiricalModelState mdp

The paired cumulative empirical-model state is history measurable.

theorem measurable_cumulativeEmpiricalModelState {mdp : MDP State Action} {episodes n : Nat} : Measurable (cumulativeEmpiricalModelState : EpisodeBatchPrefix mdp episodes n -> AdaptiveCumulativeEmpiricalModelState mdp)

Cumulative empirical-model state through trajectory coordinate `round`.

def adaptiveCumulativeEmpiricalModelStateAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) : AdaptiveCumulativeEmpiricalModelState mdp

The cumulative empirical-model state at a fixed generated round is measurable.

theorem measurable_adaptiveCumulativeEmpiricalModelStateAt {mdp : MDP State Action} {episodes : Nat} (round : Nat) : Measurable fun trajectory : EpisodeBatchTrajectory mdp episodes => adaptiveCumulativeEmpiricalModelStateAt trajectory round

Extending the prefix adds exactly the new transition-count coordinate.

theorem adaptiveCumulativeEmpiricalModelStateAt_transitionCount_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : (adaptiveCumulativeEmpiricalModelStateAt trajectory (round + 1)).1 stage state action nextState = (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1 stage state action nextState + (trajectory (round + 1)).transitionCount stage state action nextState

Extending the prefix adds exactly the new reward-sum coordinate.

theorem adaptiveCumulativeEmpiricalModelStateAt_rewardSum_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : (adaptiveCumulativeEmpiricalModelStateAt trajectory (round + 1)).2 stage state action = (adaptiveCumulativeEmpiricalModelStateAt trajectory round).2 stage state action + (trajectory (round + 1)).rewardSum stage state action

Visit counts are definitionally derived from the same cumulative state.

theorem adaptiveCumulativeEmpiricalModelStateAt_visitCount {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : (adaptiveCumulativeEmpiricalModelStateAt trajectory round).1.visitCount stage state action = ∑ i : Fin (round + 1), (trajectory i).visitCount stage state action

The paper count `N_k(x,a)` read from exactly one generated prefix.

def adaptiveCumulativeAggregateVisitCountAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) : AggregateVisitCountSummary (State := State) (Action := Action)

Every fixed-round aggregate state-action count table is measurable.

theorem measurable_adaptiveCumulativeAggregateVisitCountAt {mdp : MDP State Action} {episodes : Nat} (round : Nat) : Measurable fun trajectory : EpisodeBatchTrajectory mdp episodes => adaptiveCumulativeAggregateVisitCountAt trajectory round

The aggregate count is the literal sum over prior episodes and stages.

theorem adaptiveCumulativeAggregateVisitCountAt_eq_sum {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) : adaptiveCumulativeAggregateVisitCountAt trajectory round state action = ∑ i : Fin (round + 1), ∑ stage : Fin mdp.horizon, (trajectory i).visitCount stage state action

Extending the generated prefix adds exactly one episode's stage visits.

theorem adaptiveCumulativeAggregateVisitCountAt_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) : adaptiveCumulativeAggregateVisitCountAt trajectory (round + 1) state action = adaptiveCumulativeAggregateVisitCountAt trajectory round state action + ∑ stage : Fin mdp.horizon, (trajectory (round + 1)).visitCount stage state action

Empirical reward with the explicit zero-count convention.

noncomputable def AdaptiveCumulativeEmpiricalModelState.empiricalReward {mdp : MDP State Action} (model : AdaptiveCumulativeEmpiricalModelState mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) : Real

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

theorem AdaptiveCumulativeEmpiricalModelState.empiricalReward_of_visitCount_eq_zero {mdp : MDP State Action} (model : AdaptiveCumulativeEmpiricalModelState mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) (hzero : model.1.visitCount stage state action = 0) : model.empiricalReward stage state action = 0

Total number of environment time steps after `episodes` episodes.

def totalSteps (mdp : MDP State Action) (episodes : Nat) : Nat

Integer numerator used in the UCBVI-CH logarithmic factor.

def confidenceNumerator (mdp : MDP State Action) (episodes : Nat) : Nat

Safe total version of the UCBVI-CH logarithmic factor. The `max 1` only specifies invalid/degenerate inputs and disappears under the positive task contract.

noncomputable def logFactor (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real

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

theorem one_le_confidenceNumerator_div (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 1 <= ((confidenceNumerator (State := State) (Action := Action) mdp episodes : Nat) : Real) / delta

On the task domain, the safe total logarithm is exactly the paper factor.

theorem logFactor_eq_paper (mdp : MDP State Action) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : logFactor (State := State) (Action := Action) mdp episodes delta = Real.log (((confidenceNumerator (State := State) (Action := Action) mdp episodes : Nat) : Real) / delta)

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

theorem logFactor_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) : 0 <= logFactor (State := State) (Action := Action) mdp episodes delta

Paper-shaped Hoeffding scale `7 H L`.

noncomputable def scale (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real

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

theorem scale_nonneg (mdp : MDP State Action) (episodes : Nat) (delta : Real) : 0 <= scale (State := State) (Action := Action) mdp episodes delta

Clipped Hoeffding radius: `H` at zero visits and `min H (7 H L / sqrt N)` afterwards.

noncomputable def countRadius (mdp : MDP State Action) (episodes : Nat) (delta : Real) : TransitionCountRadius

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

theorem countRadius_zero (mdp : MDP State Action) (episodes : Nat) (delta : Real) : (countRadius (State := State) (Action := Action) mdp episodes delta).radius 0 = (mdp.horizon : Real)

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

theorem countRadius_of_pos (mdp : MDP State Action) (episodes : Nat) (delta : Real) {count : Nat} (hcount : 0 < count) : (countRadius (State := State) (Action := Action) mdp episodes delta).radius count = min (mdp.horizon : Real) (scale (State := State) (Action := Action) mdp episodes delta / Real.sqrt count)

One-episode-at-a-time cumulative optimistic source. Coordinate zero follows `initialTable`; coordinate `n+1` is generated by the pure optimistic policy computed from all coordinates through `n`.

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

The next policy is exactly the cumulative empirical optimistic plan.

theorem source_successorPolicy_eq_optimisticPolicy (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (history : EpisodeBatchPrefix mdp 1 n) : (source mdp initialState initialTable defaultState episodes delta).successorPolicy n history = (history.cumulativeTransitionCountSummary.countRadiusOptimisticPlan mdp defaultState (countRadius (State := State) (Action := Action) mdp episodes delta) ).optimisticPolicy

On a complete generated trajectory, the policy at successor episode `n+1` uses exactly the cumulative counts through `n`.

theorem source_policyAt_succ_eq_optimisticPolicy (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : (source mdp initialState initialTable defaultState episodes delta).policyAt trajectory (n + 1) = (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState (countRadius (State := State) (Action := Action) mdp episodes delta) n ).optimisticPolicy

The policy/model alignment names the paired cumulative state explicitly.

theorem source_policyAt_succ_eq_modelState_optimisticPolicy (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (n : Nat) : (source mdp initialState initialTable defaultState episodes delta).policyAt trajectory (n + 1) = ((adaptiveCumulativeEmpiricalModelStateAt trajectory n).1 |>.countRadiusOptimisticPlan mdp defaultState (countRadius (State := State) (Action := Action) mdp episodes delta) |>.optimisticPolicy)