BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeHoeffdingUCBVI

# Adaptive cumulative Hoeffding UCB-VI foundation This module records the first generated-process leaves for the Hoeffding UCB-VI route. It adds the reward-sum component that was absent from the existing cumulative transition-count state, proves exact prefix updates and measurability, and defines a one-episode-at-a-time adaptive source whose next policy is the cumulative empirical optimistic policy with a clipped inverse-square-root Hoeffding radius. The source is genuinely generated by `AdaptiveEpisodeBatchSource.trajectoryMeasure`. It has no forced uniform-exploration mixture and its policy depends on the complete generated prefix. The definitions are total at zero counts and at invalid confidence inputs; under the eventual task contract (`0 < delta <= 1`, positive horizon and episode budget) the logarithmic factor agrees with the usual UCBVI-CH factor. This is not yet the high-probability UCB-VI regret theorem. In particular, the existing `EstimatedModelPlan` recursion does not yet implement the paper's cross-episode `min (Q_previous, H, backup)` clipping, and the adaptive self-normalized transition-value confidence and cumulative martingale/bonus assembly remain downstream obligations.

Module map

Declarations
36
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeInverseSqrtCalibration

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAggregateTransition

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

abbrev BanditRLProof.FiniteHorizonRL.RewardSumSummary Compiled

Reward sums indexed by stage, state, and action.

abbrev RewardSumSummary (mdp : MDP State Action)
Source line 42 Chapter context: Finite-horizon RL
abbrev BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalModelState Compiled

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)
Source line 50 Chapter context: Finite-horizon RL
abbrev BanditRLProof.FiniteHorizonRL.AggregateVisitCountSummary Compiled

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

abbrev AggregateVisitCountSummary
Source line 54 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateVisitCount Compiled

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
Source line 59 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.measurable_aggregateVisitCount Compiled

The complete cross-stage aggregate count view is measurable.

theorem measurable_aggregateVisitCount {mdp : MDP State Action} : Measurable (aggregateVisitCount : TransitionCountSummary mdp -> AggregateVisitCountSummary (State
Source line 69 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.EpisodeBatchPrefix.cumulativeRewardSumSummary Compiled

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
Source line 87 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.EpisodeBatchPrefix.measurable_rewardSum_coordinate Compiled

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
Source line 97 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.EpisodeBatchPrefix.measurable_cumulativeRewardSumSummary Compiled

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)
Source line 121 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.EpisodeBatchPrefix.cumulativeEmpiricalModelState Compiled

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
Source line 140 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.EpisodeBatchPrefix.measurable_cumulativeEmpiricalModelState Compiled

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)
Source line 149 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.adaptiveCumulativeEmpiricalModelStateAt Compiled

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

def adaptiveCumulativeEmpiricalModelStateAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) : AdaptiveCumulativeEmpiricalModelState mdp
Source line 160 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.measurable_adaptiveCumulativeEmpiricalModelStateAt Compiled

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
Source line 169 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeEmpiricalModelStateAt_transitionCount_succ Compiled

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
Source line 179 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeEmpiricalModelStateAt_rewardSum_succ Compiled

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
Source line 196 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeEmpiricalModelStateAt_visitCount Compiled

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
Source line 221 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateVisitCountAt Compiled

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
Source line 235 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.measurable_adaptiveCumulativeAggregateVisitCountAt Compiled

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
Source line 243 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateVisitCountAt_eq_sum Compiled

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
Source line 253 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateVisitCountAt_succ Compiled

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
Source line 269 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalModelState.empiricalReward Compiled

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
Source line 283 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeEmpiricalModelState.empiricalReward_of_visitCount_eq_zero Compiled

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
Source line 294 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.totalSteps Compiled

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

def totalSteps (mdp : MDP State Action) (episodes : Nat) : Nat
Source line 305 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.confidenceNumerator Compiled

Integer numerator used in the UCBVI-CH logarithmic factor.

def confidenceNumerator (mdp : MDP State Action) (episodes : Nat) : Nat
Source line 309 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.logFactor Compiled

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
Source line 319 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.one_le_confidenceNumerator_div Compiled

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
Source line 327 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.logFactor_eq_paper Compiled

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
Source line 349 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.logFactor_nonneg Compiled

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
Source line 365 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.scale Compiled

Paper-shaped Hoeffding scale `7 H L`.

noncomputable def scale (mdp : MDP State Action) (episodes : Nat) (delta : Real) : Real
Source line 372 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.scale_nonneg Compiled

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
Source line 380 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.countRadius Compiled

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
Source line 392 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.countRadius_zero Compiled

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
Source line 404 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.countRadius_of_pos Compiled

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
Source line 413 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.source Compiled

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
Source line 430 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.source_successorPolicy_eq_optimisticPolicy Compiled

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
Source line 461 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.source_policyAt_succ_eq_optimisticPolicy Compiled

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
Source line 480 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.source_policyAt_succ_eq_modelState_optimisticPolicy Compiled

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
Source line 495 Chapter context: Finite-horizon RL