BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAdaptiveBellmanMartingale

A function with a countable discrete left coordinate is measurable when every right section is measurable.

theorem measurable_prod_of_countable_left {Alpha Beta Gamma : Type*} [MeasurableSpace Alpha] [MeasurableSpace Beta] [MeasurableSpace Gamma] [Countable Alpha] [MeasurableSingletonClass Alpha] (f : Alpha × Beta -> Gamma) (hf : forall a, Measurable (fun b => f (a, b))) : Measurable f

Mapping a composition-product by a function which may also read the conditioning coordinate is the composition-product with the correspondingly mapped copy-and-kernel law.

lemma compProd_map_dependent {Alpha : Type u} {Beta : Type v} {Gamma : Type w} [MeasurableSpace Alpha] [MeasurableSpace Beta] [MeasurableSpace Gamma] (mu : Measure Alpha) [SFinite mu] (kappa : ProbabilityTheory.Kernel Alpha Beta) [ProbabilityTheory.IsSFiniteKernel kappa] (f : Alpha × Beta -> Gamma) (hf : Measurable f) : (mu ⊗ₘ kappa).map (fun p => (p.1, f p)) = mu ⊗ₘ ((ProbabilityTheory.Kernel.id ×ₖ kappa).map f)

Conditional law of a statistic which may depend measurably on both the observed prefix and the newly generated batch.

theorem trajectoryMeasure_condDistrib_historyBatchStatistic {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (statistic : EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes -> Real) (hstatistic : Measurable statistic) : ProbabilityTheory.condDistrib (fun trajectory : EpisodeBatchTrajectory mdp episodes => statistic (Preorder.frestrictLe n trajectory, trajectory (n + 1))) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] ((ProbabilityTheory.Kernel.id ×ₖ source.batchKernel n).map statistic)

Trimmed conditional-expectation-kernel version of the preceding dependent statistic law.

theorem condExpKernel_map_historyBatchStatistic_eq_batchKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (statistic : EpisodeBatchPrefix mdp episodes n × EpisodeBatch mdp episodes -> Real) (hstatistic : Measurable statistic) : Filter.Eventually (fun trajectory : EpisodeBatchTrajectory mdp episodes => Measure.map (fun path : EpisodeBatchTrajectory mdp episodes => statistic (Preorder.frestrictLe n path, path (n + 1))) (ProbabilityTheory.condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (EpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = ((ProbabilityTheory.Kernel.id ×ₖ source.batchKernel n).map statistic) (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))

Inflation factor generated by the `z/(32H)` self-bounding term.

noncomputable def bellmanInflation (mdp : MDP State Action) : Real

Uniform cap for every finite-horizon power of `bellmanInflation`.

noncomputable def bellmanWeightCap : Real

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

theorem bellmanInflation_one_le (mdp : MDP State Action) : 1 <= bellmanInflation mdp

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

theorem bellmanInflation_pow_le_cap (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : bellmanInflation mdp ^ remaining <= bellmanWeightCap

Normalized chronological recursion weight. Multiplication by the global cap `32/31` later recovers the exact factor `alpha^(stage+1)`.

noncomputable def normalizedBellmanWeight (mdp : MDP State Action) (stage : Fin mdp.horizon) : Real

Weight of the local charge at a chronological stage.

noncomputable def normalizedBellmanChargeWeight (mdp : MDP State Action) (stage : Fin mdp.horizon) : Real

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

theorem normalizedBellmanChargeWeight_mem_Icc (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (stage : Fin mdp.horizon) : normalizedBellmanChargeWeight mdp stage ∈ Set.Icc (0 : Real) 1

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

theorem normalizedBellmanChargeWeight_mul_inflation (mdp : MDP State Action) (stage : Fin mdp.horizon) : normalizedBellmanChargeWeight mdp stage * bellmanInflation mdp = normalizedBellmanWeight mdp stage

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

theorem normalizedBellmanWeight_mem_Icc (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (stage : Fin mdp.horizon) : normalizedBellmanWeight mdp stage ∈ Set.Icc (0 : Real) 1

The clipped, normalized and chronologically weighted continuation gap used by the predictable martingale. Clipping is inactive on the joint confidence event; normalization keeps the global MGF range exactly `[0,H]`.

noncomputable def clippedSuccessorGapFeatureOfSummaries (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (summaries : Fin (n + 1) -> TransitionCountSummary mdp) (stage : Fin mdp.horizon) (state : State) : Real

The martingale feature is globally in `[0,H]`, independently of whether the statistical event holds.

theorem clippedSuccessorGapFeatureOfSummaries_mem_Icc (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (summaries : Fin (n + 1) -> TransitionCountSummary mdp) (stage : Fin mdp.horizon) (state : State) : clippedSuccessorGapFeatureOfSummaries mdp defaultState episodes delta n summaries stage state ∈ Set.Icc (0 : Real) mdp.horizon

Compensated batch statistic for one fixed discrete prefix-summary table.

noncomputable def successorBellmanStatisticOfSummaries (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (tilt : Real) (input : (Fin (n + 1) -> TransitionCountSummary mdp) × EpisodeBatch mdp 1) : Real

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

theorem measurable_successorBellmanStatisticOfSummaries (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (tilt : Real) : Measurable (successorBellmanStatisticOfSummaries mdp defaultState episodes delta n tilt)

The same statistic with the prefix summarized exactly as the recurrent planner summarizes it.

noncomputable def successorBellmanHistoryBatchStatistic (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (tilt : Real) (input : EpisodeBatchPrefix mdp 1 n × EpisodeBatch mdp 1) : Real

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

theorem measurable_successorBellmanHistoryBatchStatistic (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (tilt : Real) : Measurable (successorBellmanHistoryBatchStatistic mdp defaultState episodes delta n tilt)

A successor episode's compensated, prefix-predictable Bellman innovation has conditional MGF at most one under the literal recurrent batch kernel.

theorem recurrentSuccessorBellmanInnovation_compensated_hasCondMGFUpperBoundAt {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) (n : Nat) (tilt : Real) : Concentration.HasCondMGFUpperBoundAt (BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.batchPrefixFiltration (mdp

The un-compensated Bellman innovation of one successor episode, with the policy and clipped gap feature read from one fixed prefix-summary table.

noncomputable def successorBellmanInnovationOfSummaries (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (input : (Fin (n + 1) -> TransitionCountSummary mdp) × EpisodeBatch mdp 1) : Real

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

theorem measurable_successorBellmanInnovationOfSummaries (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) : Measurable (successorBellmanInnovationOfSummaries mdp defaultState episodes delta n)

The successor Bellman innovation with the recurrent prefix summarized in exactly the same way as the generated source.

noncomputable def successorBellmanInnovationOfHistoryBatch (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) (input : EpisodeBatchPrefix mdp 1 n × EpisodeBatch mdp 1) : Real

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

theorem measurable_successorBellmanInnovationOfHistoryBatch (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (n : Nat) : Measurable (successorBellmanInnovationOfHistoryBatch mdp defaultState episodes delta n)

Prefix-predictable Bellman innovation. Coordinate zero is deliberately zero: the canonical initial episode is charged separately by its deterministic `H` envelope, while every successor coordinate uses its strict prefix.

noncomputable def recurrentBellmanInnovationPrefix (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) : (round : Nat) -> EpisodeBatchPrefix mdp 1 round -> Real | 0, _history => 0 | n + 1, history => successorBellmanInnovationOfHistoryBatch mdp defaultState episodes delta n (Preorder.frestrictLe₂ (π

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

theorem measurable_recurrentBellmanInnovationPrefix (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (round : Nat) : Measurable (recurrentBellmanInnovationPrefix mdp defaultState episodes delta round)

Actual successor-episode Bellman innovation process on the generated recurrent trajectory.

noncomputable def recurrentBellmanInnovationProcess (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (round : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : Real

Deterministic per-episode variance budget. Coordinate zero is zero because its regret is paid separately; every successor episode has budget `H^3`.

noncomputable def recurrentBellmanInnovationVarianceProcess (mdp : MDP State Action) (round : Nat) (_trajectory : EpisodeBatchTrajectory mdp 1) : Real

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

theorem recurrentBellmanInnovation_compensated_stronglyAdapted (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta tilt : Real) : StronglyAdapted (BanditRLProof.FiniteHorizonRL.AdaptiveEpisodeBatchSource.batchPrefixFiltration (mdp

Coordinate zero has the trivial compensated MGF certificate.

theorem recurrentBellmanInnovation_zero_compensated_hasMGFUpperBoundAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta tilt : Real) : Concentration.HasMGFUpperBoundAt (fun trajectory : EpisodeBatchTrajectory mdp 1 => tilt * recurrentBellmanInnovationProcess mdp defaultState episodes delta 0 trajectory - (tilt ^ 2 / 8) * recurrentBellmanInnovationVarianceProcess mdp 0 trajectory) 1 0 (recurrentSource mdp initialState defaultState episodes delta |>.trajectoryMeasure)

Fixed-tilt upper tail for the sum of the generated successor-episode Bellman innovations. The source, prefix policy, and transition law are the same objects as in the recurrent planner.

theorem trajectoryMeasure_recurrentBellmanInnovation_sum_ge_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) (tilt threshold : Real) (htilt : 0 < tilt) : let source := recurrentSource mdp initialState defaultState episodes delta source.trajectoryMeasure {trajectory | threshold <= (Finset.range episodes).sum (fun round => recurrentBellmanInnovationProcess mdp defaultState episodes delta round trajectory)} <= ENNReal.ofReal (Real.exp (-tilt * threshold + (tilt ^ 2 / 8) * ((episodes : Real) * ((mdp.horizon : Real) * (mdp.horizon : Real) ^ 2))))