BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIOptimism

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

noncomputable def optimalQAt (mdp : MDP State Action) (stage : Fin mdp.horizon) (state : State) (action : Action) : Real

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

def QDominatesOptimal (mdp : MDP State Action) (table : QTable mdp) : Prop

Bounded rewards imply every optimal action value is at most `H`.

theorem optimalQAt_le_horizon (mdp : MDP State Action) (hreward : ∀ state action, |mdp.reward state action| <= 1) (stage : Fin mdp.horizon) (state : State) (action : Action) : optimalQAt mdp stage state action <= (mdp.horizon : Real)

The all-`H` initialization is optimistic.

theorem initialQTable_dominatesOptimal (mdp : MDP State Action) (hreward : ∀ state action, |mdp.reward state action| <= 1) : QDominatesOptimal mdp (initialQTable mdp)

Statistical premise for one deterministic clipped update. Downstream it is discharged from the same-source finite event; it is kept abstract here so the Bellman induction remains reusable and auditable.

def HasOptimalTailConfidence (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) : Prop

One clipped update preserves pointwise optimal-Q dominance.

theorem clippedQTable_dominatesOptimal (mdp : MDP State Action) (previousQ : QTable mdp) (summary : TransitionCountSummary mdp) (defaultState : State) (bonusScale : Real) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) (hprevious : QDominatesOptimal mdp previousQ) (hconfidence : HasOptimalTailConfidence mdp summary defaultState bonusScale) : QDominatesOptimal mdp (clippedQTable mdp previousQ summary defaultState bonusScale)

A pooled state-action count through prefix `round` is at most the number of observed episodes times `H`.

theorem adaptiveCumulativeAggregateVisitCountAt_le {mdp : MDP State Action} (trajectory : EpisodeBatchTrajectory mdp 1) (round : Nat) (state : State) (action : Action) : adaptiveCumulativeAggregateVisitCountAt trajectory round state action <= (round + 1) * mdp.horizon

The same-source joint event discharges the complete scalar confidence contract for the exact pooled summary at a queried positive prefix.

theorem hasOptimalTailConfidence_of_not_mem_simultaneousTransitionFailureEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State