9. Finite-horizon reinforcement learning

Plain-English statement. A finite-horizon Markov decision process packages a horizon, measurable finite state and action spaces, an initial-stage reward, and a stochastic transition kernel.

Intuition

The structure is the common mathematical world in which policies, trajectories, Bellman operators, empirical models, and regret are interpreted.

Why it is needed

Without one explicit MDP interface, later confidence or regret statements could silently switch reward, transition, horizon, or measurability conventions.

Place in the proof

It is the root declaration of the finite-horizon RL chapter.

Proof idea

This is a structure, not a theorem. Its fields carry the data and regularity needed by the recursive constructions that follow.

Lean reading notes

Finiteness and measurable-space facts are supplied through typeclasses around the structure. The exact field types in the Lean statement are authoritative.

Teaching dependencies

No direct teaching dependency recorded.

structure MDP (State : Type u) (Action : Type v) [MeasurableSpace State] [MeasurableSpace Action] [Fintype State] [Fintype Action] where

Plain-English statement. A Markov policy's expected regret equals the sum, under its own state occupancies, of the stagewise gap between the optimal Bellman value and the policy's Bellman value.

Intuition

Regret can be read either as a difference of total values or as local Bellman suboptimality accumulated along the states the policy actually visits.

Why it is needed

Optimistic confidence proofs naturally bound local Bellman residuals; this identity turns those local bounds into an expected policy-regret theorem.

Place in the proof

It joins Bellman optimality to occupancy-based empirical-model and optimistic-certificate consumers.

Proof idea

Prove a one-step Bellman difference identity, integrate it through the induced state kernel, and telescope recursively over the remaining horizon.

Lean reading notes

The occupancy recursion and all measurability/integrability obligations are explicit. This is expected policy regret, not realized sample-path regret.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.MDP.optimalValueAt_dominates_and_is_attained

theorem expectedRegret_eq_occupancyGapRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : policy.expectedRegret initialState = policy.occupancyGapRemaining mdp.horizon le_rfl initialState

Plain-English statement. Across the scheduled sequence of adaptive empirical planning windows, both the explicit failure probability and the average realized behavior-regret envelope converge to zero, and every window carries the corresponding confidence and optimism guarantee.

Intuition

Exploration decays slowly enough to keep learning the model while confidence tightens quickly enough that both the bad-event probability and average behavior regret vanish.

Why it is needed

This is a real adaptive stochastic-RL consistency endpoint, far beyond the Bellman interface that the earlier website still described as planned.

Place in the proof

It is the regularity-closed all-window parent for later natural-causal, first-passage, and stopping-time constructions.

Proof idea

Combine cumulative empirical transition confidence, path-support visit floors, known reward transport, optimistic planning, selected-return concentration, the decaying exploration schedule, and asymptotic estimates for both coordinates.

Lean reading notes

The long signature records finite nonempty Standard Borel spaces, exact generated sources, support, bounded means, sub-Gaussian rewards, and horizon positivity. It is not a minimax UCB-VI theorem.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret_eq_occupancyGapRemaining

theorem exploratorySource_trajectoryMeasure_projectedCumulativeInverseSqrtPathSupport_decayingExplorationAverageRealizedBehaviorConsistency_allWindows_of_standardBorel (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (baseVisitFloor : Real) (rewardSource : mdp.MeanCompatibleRewardKernel) (rewardVarianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => (AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticRealizedFailureBudget n, AdaptiveStochasticEpisodeBatchSource.decayingExplorationStochasticAverageRealizedBehaviorRegretBound mdp baseVisitFloor rewardVarianceProxy n)) atTop (nhds (0, 0)) /\ forall n, let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes rewardSource initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let projection := MDP.MeanCompatibleRewardKernel.knownRewardEpisodeBatchTrajectory (mdp

Plain-English statement. For each fixed inverse-square-root threshold index and horizon greater than four, the exact average realized behavior-regret process stopped at the genuine uncapped first passage is integrable, and its expectation is at most the threshold that was hit.

Intuition

The stopping rule waits until the certified average-regret process enters a shrinking target; square-integrable stopping fibers and uniform coordinate moments make the unbounded stopped value integrable.

Why it is needed

An almost-sure finite hit does not by itself justify taking expectations. This theorem supplies the missing L1 bridge and the expected upper bound without pretending to use optional stopping.

Place in the proof

It is the current fixed-index terminal of the natural-causal inverse-sqrt hittingAfter route.

Proof idea

Decompose the stopping time into equality fibers, use its L2 round count to sum square roots of fiber masses, apply indicator Hölder to uniformly L2 deterministic coordinates, then integrate the almost-everywhere hit-threshold inequality.

Lean reading notes

The result keeps the explicit assumption 4 < horizon and a fixed schedule index. It does not prove expected nonnegativity, an absolute-moment rate, uniform integrability, L1 convergence, optional stopping, raw-episode regret, or complete UCB-VI.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_squareIntegrableFiniteStoppingTime, BanditRLProof.integrable_stoppedValue_of_uniform_secondMoment_of_memLp_two_rounds

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdUnboundedHittingAfter_stoppedAverageRealizedBehaviorRegret_integrable_and_integral_le_threshold (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (hvarianceProxy : 0 < varianceProxy) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (baseVisitFloor : Real) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 4 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppedProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex Integrable stoppedProcess source.trajectoryMeasure /\ integral source.trajectoryMeasure stoppedProcess <= selfConsistentScheduledNaturalCausalInverseSqrtFirstPassageThreshold scheduleIndex

Plain-English statement. For every generated prefix and state-action pair, summing the aggregate transition numerator over next states gives exactly the aggregate visit-count denominator used by UCBVI.

Intuition

Every recorded visit has exactly one successor state, so the empirical transition row and its denominator count the same observations.

Why it is needed

A normalized model is unsound if its numerator and denominator come from different stages, batches, or samples; this identity locks both to one strict generated prefix.

Place in the proof

This is the aggregate empirical-transition foundation immediately below the recurrent planner and same-source confidence event.

Proof idea

Expand both prefix counts as finite sums over earlier episode coordinates and stages, interchange the finite next-state sum, and use the exact one-successor row-sum identity in each generated batch.

Lean reading notes

The zero-count row has an explicit fallback; at positive count, `aggregateEmpiricalTransitionPMF` divides this numerator by this exact denominator and sums to one.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.TransitionCountSummary.sum_aggregateTransitionCount_eq_aggregateVisitCount, BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_eq_sum

theorem sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) : (∑ nextState : State, adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState) = adaptiveCumulativeAggregateVisitCountAt trajectory round state action

Plain-English statement. At successor episode k+1, the canonical source selects exactly the measurable greedy policy produced by the previous-Q-clipped UCBVI recurrence from coordinates at most k.

Intuition

The algorithm never recomputes policy k from future data: its table is a deterministic measurable function of the strict history available before the next batch is generated.

Why it is needed

This is the algorithm-identity bridge between an optimistic dynamic program and the actual policy whose trajectory appears in the regret theorem.

Place in the proof

It consumes the aggregate empirical model and feeds policy alignment, optimism, and generated episode pseudo-regret.

Proof idea

Fold the cumulative transition summaries through the recurrent Q update, prove the zero-count value H and positive-count clipped backup equations, establish measurable finite argmax, and unfold the adaptive source's successor kernel selector.

Lean reading notes

The recurrence clips by both the previous Q table and H. `recurrentInitialTable` is canonical, ties are resolved by finite argmax, and no arbitrary initial optimistic table remains in the terminal.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.clippedQRemaining_of_aggregateVisitCount_pos, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.measurable_clippedPolicyTable, BanditRLProof.FiniteHorizonRL.sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt

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

Plain-English statement. On the recurrent source's own trajectory law, one finite joint event simultaneously controls actual-count singleton transition residuals and the normalized optimal-tail value probe, with mass at most delta/5.

Intuition

The confidence variables are generated from the same batches the algorithm counts. A scalar optimal-value probe is proved from the same transition law because singleton bounds alone would lose a square-root state factor.

Why it is needed

It rules out the common semantic gap of proving confidence on an offline or independent sample and applying it to another generated policy trajectory.

Place in the proof

This joint producer sits between strict-prefix trajectory alignment and Bellman optimism; its unused probability budget is combined with the Bellman innovation tail at the terminal.

Proof idea

Build predictable selected-transition residuals, prove conditional MGF bounds under the adaptive batch kernel, peel over actual positive visit counts, union over finite episode/state/action/probe indices, and calibrate the paper log factor.

Lean reading notes

The event contains p-sensitive Bernstein singleton coordinates plus a normalized `optimalTailProbe`. The latter is an additional proved projection on the same law, not a caller hypothesis or a logical consequence of singleton radii alone.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.trajectoryMeasure_bernsteinCoordinateFailureEvent_le, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.trajectoryMeasure_optimalTailFailureEvent_le, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_policyAt_succ

theorem recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hreward : ∀ state action, |mdp.reward state action| <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure (AdaptiveEpisodeBatchSource.simultaneousTransitionFailureEvent source episodes (logFactor (State

Plain-English statement. Outside the same-source transition failure event, every recurrent generated Q table dominates the true finite-horizon optimal Q values at every stage, state, and action.

Intuition

The empirical backup plus bonus covers the true optimal tail; clipping preserves optimism because both the previous table and the horizon cap are already upper bounds.

Why it is needed

Optimism converts the generated policy's greedy choice into a one-sided regret comparison, but only after it is proved for the exact table used by that source.

Place in the proof

It is the Bellman-induction consumer of same-source confidence and the principal premise discharged internally by the episode-regret decomposition.

Proof idea

Start from the canonical all-H table, induct over episode summaries, perform backward induction over the horizon, apply the optimal-tail confidence probe at positive count, and handle zero count by the explicit H branch.

Lean reading notes

The theorem quantifies over the recurrent source trajectory and reads the same `simultaneousTransitionFailureEvent`; no abstract `OptimisticBellmanCertificate` is passed to the final regret theorem.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.clippedQTable_dominatesOptimal

theorem recurrentQTableOfTrajectory_dominatesOptimal {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) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent source episodes (logFactor (State

Plain-English statement. For every aligned successor episode on the good transition event, the generated policy-value pseudo-regret is bounded by an inflated sum of visited local confidence charges plus its generated Bellman innovation.

Intuition

Optimism pays for systematic model uncertainty through bonuses; the difference between expected next-state propagation and the actually visited state is isolated as centered noise.

Why it is needed

This is the exact bridge from per-episode Bellman reasoning to the two global sums that can be bounded by counting and martingale concentration.

Place in the proof

It is downstream of strict-prefix action alignment and recurrent optimism, and directly upstream of the high-probability terminal.

Proof idea

Recursively compare clipped and true policy values, absorb coordinate model error with a small Bellman inflation, unroll the recursion with bounded weights, and identify the residual with the batch generated under the selected policy.

Lean reading notes

The regret object is raw generated policy-value pseudo-regret at the episode's sampled initial state. It is not behavior expected regret or realized sampled-return regret.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentQTableOfTrajectory_dominatesOptimal, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_all_successorBatchAligned_ae

theorem recurrentSource_generatedSuccessorPseudoRegret_le_charge_add_innovation {mdp : MDP State Action} (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} {delta : Real} {trajectory : EpisodeBatchTrajectory mdp 1} (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : forall state action, 0 <= mdp.reward state action) (hrewardOne : forall state action, mdp.reward state action <= 1) (defaultState : State) (htrajectory : trajectory ∉ simultaneousTransitionFailureEvent (recurrentSource mdp initialState defaultState episodes delta) episodes (logFactor (State

Plain-English statement. Along every generated path, the total clipped local UCBVI charge paid at actually visited state-action pairs obeys an explicit square-root leading bound plus low-count and harmonic corrections.

Intuition

Frequently visited pairs get cheap bonuses; zero and low counts can be expensive only a bounded number of times, while positive reciprocal-square-root charges telescope against count growth.

Why it is needed

The regret rate must come from exact generated counts, not from assuming the desired bonus sum or replacing it with a reachability denominator.

Place in the proof

This deterministic pathwise theorem discharges the charge branch of the episode decomposition before the final probability union.

Proof idea

Partition visits into zero/low and positive-count regimes, use the exact batched count successor relation, prove reciprocal-square-root and logarithmic summation inequalities, then sum over the finite state-action type.

Lean reading notes

All Nat-to-Real casts, state/action cardinalities, log positivity, and zero denominators are explicit. The terminal uses a coarser 20/250 envelope after combining this bound with other costs.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_positive_batchedInvSqrt_le, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.sum_high_batchedRatio_le_log, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSource_generatedSuccessorPseudoRegret_le_charge_add_innovation

theorem totalGeneratedPairCharge_le_explicit (mdp : MDP State Action) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : totalGeneratedPairCharge mdp episodes delta trajectory <= 18 * (mdp.horizon : Real) * logFactor (State

Plain-English statement. The sum of recurrent episode Bellman innovations on the actual generated filtration exceeds its explicit Hoeffding threshold with probability at most delta/5.

Intuition

After each policy is fixed by the strict past, the next generated episode contributes a bounded conditionally centered value-propagation error.

Why it is needed

Pathwise bonus control cannot eliminate stochastic next-state noise; this theorem pays that remaining term without pretending it is a deterministic Bellman residual.

Place in the proof

It is the generated-filtration probability producer parallel to transition confidence and immediately below the final failure-budget union.

Proof idea

Express each successor statistic under the source's conditional batch kernel, prove its compensated conditional MGF, package the sequence as strongly adapted, apply the finite-sum exponential tail, and calibrate the threshold by the common log factor.

Lean reading notes

The process uses coordinate zero and successor indices explicitly, reads no future episode, and is distinct from the transition-estimation residual controlled by the confidence event.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSuccessorBellmanInnovation_compensated_hasCondMGFUpperBoundAt, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.trajectoryMeasure_recurrentBellmanInnovation_sum_ge_le

theorem recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifth (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure {trajectory | bellmanInnovationThreshold (State

Plain-English statement. For one recurrent generated known-reward UCBVI-CH process, raw policy-value pseudo-regret across exactly K episode coordinates exceeds the explicit 20/250 Hoeffding bound with probability at most delta.

Intuition

Every ingredient is read from one adaptive history: the policy uses only the strict past, confidence controls that trajectory's aggregate transition rows, and the actual visited counts pay for the bonus.

Why it is needed

A planner or confidence certificate alone is not UCBVI regret; this theorem closes the generated policy-to-regret probability chain.

Place in the proof

This is the canonical Chapter 9 high-probability terminal for finite nonempty State and Action, positive H and K, a probability initial law, 0<delta<=1, and deterministic rewards in [0,1].

Proof idea

Use same-law singleton Bernstein and optimal-tail probes for optimism, decompose each successor episode into a weighted local charge and Bellman innovation, sum actual-count charges, pay the initial episode by H, and union the transition, innovation, and null alignment events.

Lean reading notes

The bound is `canonicalRegretBound`. Coordinate zero is included. The failure set is not caller supplied. This is policy-value pseudo-regret, not realized sampled-return regret; Bernstein/minimax UCB-VI is not claimed.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.AdaptiveEpisodeBatchSource.recurrentSource_generatedSuccessorPseudoRegret_le_charge_add_innovation, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.totalGeneratedPairCharge_le_explicit, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_bellmanInnovation_sum_ge_threshold_le_fifth, BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_simultaneousTransitionFailureEvent_le_fifth

theorem recurrentSource_trajectoryMeasure_cumulativeEpisodePseudoRegret_gt_canonicalRegretBound_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure {trajectory | canonicalRegretBound (State

Plain-English statement. The same recurrent UCBVI-CH pseudo-regret is integrable, and its expectation is at most the frozen high-probability bound plus the explicit K H delta failure contribution.

Intuition

On the good event use the compiled UCBVI bound; on its measurable hull use only the deterministic fact that K episodes can lose at most K H.

Why it is needed

A high-probability theorem does not automatically have the same expectation bound. The bad-event mass must be charged explicitly.

Place in the proof

This is the failure-aware expectation consumer immediately downstream of the Chapter 9 high-probability terminal.

Proof idea

Prove measurability and integrability of the recurrent policy-value regret, dominate it by the bound plus a K H indicator, integrate the indicator, and apply the proved delta tail.

Lean reading notes

The `K H delta` term is present in the exact Lean conclusion. It does not assert expected-average consistency, realized-return regret, optional stopping, or a stochastic-reward theorem.

Teaching dependencies

BanditRLProof.FiniteHorizonRL.AdaptiveCumulativeHoeffdingUCBVI.recurrentSource_trajectoryMeasure_cumulativeEpisodePseudoRegret_gt_canonicalRegretBound_le

theorem integral_cumulativeEpisodePseudoRegret_recurrentSource_le_canonicalRegretBound_add_failure (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace (EpisodeBatch mdp 1)] [StandardBorelSpace (EpisodeBatchTrajectory mdp 1)] (defaultState : State) (episodes : Nat) (delta : Real) (hhorizon : 0 < mdp.horizon) (hepisodes : 0 < episodes) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : let source := recurrentSource mdp initialState defaultState episodes delta ∫ trajectory, cumulativeEpisodePseudoRegret source defaultState episodes trajectory ∂source.trajectoryMeasure <= canonicalRegretBound (State