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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalReturnConcentration

# Sampled-return concentration on the heterogeneous causal source This module transports two adaptive sampled-return concentration processes to the dependent source whose coordinate `n` contains `episodes n` complete stochastic episodes. The supporting process uses the initial policy and `episodes 0` at coordinate zero, then the prefix-selected policy and `episodes (n + 1)` at coordinate `n + 1`; each batch is centered at its own sampled initial-state value. The regret-facing global process is zero at coordinate zero and globally centers successor coordinates `1..rounds` by the initial-law expected value of the selected policy. Its measurable-selector boundary is packaged by `GlobalReturnMeasurability`. The proof route maps each exact selected iid batch fiber to its sampled-return deviation, identifies the dynamic conditional law through the prefix/next `compProd` theorem, obtains the corresponding conditional sub-Gaussian MGF, and applies the existing strongly-adapted finite-sum tail theorem. Each total variance proxy is the genuine heterogeneous sum of its coordinate proxies; the global proxy also retains sampled-initial-state value fluctuation. Regularity is finite measurable nonempty State/Action with measurable singletons, a probability initial law, Standard Borel State/Action for regular conditional laws, a uniform selected-reward sub-Gaussian law, and a deterministic bound on stored mean rewards. The generic tail keeps strict positivity of the summed proxy explicit. Failure policy: this proves sampled-return concentration for the new round-varying latest-batch causal algorithm. It does not transport empirical model confidence, optimism, regret, or any rate from the old constant-parameter window laws. It is fixed-`rounds`, not uniform-in-time, pathwise, almost-sure, anytime, minimax, or complete UCB-VI control.

Module map

Declarations
38
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalSource, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardTotalReturnConcentration

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalRealizedSuccessorRegret

Declarations

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

def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorSampledReturnDeviation Compiled

Dynamic next-coordinate sampled-return deviation on a prefix/batch pair.

noncomputable def successorSampledReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (pair : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1))) : Real
Source line 54 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorDeviationKernel Compiled

Conditional kernel of the dynamic heterogeneous successor deviation.

noncomputable def successorDeviationKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : Kernel (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) Real
Source line 65 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorDeviationKernel_apply Compiled

Every dynamic deviation fiber is the selected policy's iid statistic law.

theorem successorDeviationKernel_apply {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : source.successorDeviationKernel n history = (source.rewardSource.iidStochasticTrajectoryFamilyMeasure (source.successorPolicy n history) initialState (episodes (n + 1))).map (mdp.sampledCumulativeReturnDeviationSum (source.successorPolicy n history) (episodes (n + 1)))
Source line 88 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorSampledReturnDeviationAt Compiled

Dynamic deviation evaluated at successor trajectory coordinate `n + 1`.

noncomputable def successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 124 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_successorSampledReturnDeviationAt Compiled

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

theorem measurable_successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : Measurable (source.successorSampledReturnDeviationAt n)
Source line 137 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_condDistrib_successorSampledReturnDeviationAt Compiled

Conditional law of the heterogeneous dynamic successor deviation.

theorem trajectoryMeasure_condDistrib_successorSampledReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] : condDistrib (source.successorSampledReturnDeviationAt n) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.successorDeviationKernel n
Source line 151 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.condExpKernel_map_successorSampledReturnDeviationAt_eq Compiled

Trimmed conditional-expectation kernel form of the same dynamic law.

theorem condExpKernel_map_successorSampledReturnDeviationAt_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] : Filter.Eventually (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => Measure.map (source.successorSampledReturnDeviationAt n) (condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = source.successorDeviationKernel n (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))
Source line 183 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.sampledReturnDeviationPrefixIncrement Compiled

Prefix-level heterogeneous increment, including coordinate zero.

noncomputable def sampledReturnDeviationPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : (round : Nat) -> HeterogeneousStochasticEpisodeBatchPrefix mdp episodes round -> Real | 0, history => mdp.sampledCumulativeReturnDeviationSum source.initialPolicy (episodes 0) (history ⟨0, Finset.mem_Iic.mpr le_rfl⟩) | n + 1, history => source.successorSampledReturnDeviation n (Preorder.frestrictLe₂ (π
Source line 220 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_sampledReturnDeviationPrefixIncrement Compiled

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

theorem measurable_sampledReturnDeviationPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) : Measurable (source.sampledReturnDeviationPrefixIncrement round)
Source line 240 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.sampledReturnDeviationIncrement Compiled

Adapted heterogeneous sampled-return increment on the full trajectory.

noncomputable def sampledReturnDeviationIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 263 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_sampledReturnDeviationIncrement Compiled

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

theorem measurable_sampledReturnDeviationIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) : Measurable (source.sampledReturnDeviationIncrement round)
Source line 276 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.sampledReturnDeviationIncrement_stronglyAdapted_piLE Compiled

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

theorem sampledReturnDeviationIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : StronglyAdapted (Filtration.piLE (X
Source line 288 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.sampledReturnDeviationIncrement_zero_hasSubgaussianMGF Compiled

Coordinate zero inherits the iid batch MGF at `episodes 0`.

theorem sampledReturnDeviationIncrement_zero_hasSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes 0))] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasSubgaussianMGF (source.sampledReturnDeviationIncrement 0) (mdp.iidSampledCumulativeReturnDeviationVarianceProxy (episodes 0) rewardBound rewardVarianceProxy) source.trajectoryMeasure
Source line 306 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.sampledReturnDeviationIncrement_succ_hasCondSubgaussianMGF Compiled

Coordinate `n + 1` is conditionally sub-Gaussian at its own batch size.

theorem sampledReturnDeviationIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasCondSubgaussianMGF (Filtration.piLE (X
Source line 339 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSampledReturnDeviationVarianceProxy Compiled

Sum of coordinate-specific sampled-return variance proxies.

noncomputable def cumulativeSampledReturnDeviationVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal
Source line 457 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSampledReturnDeviationVarianceProxy_pos Compiled

The heterogeneous total proxy is positive under a positive batch schedule.

theorem cumulativeSampledReturnDeviationVarianceProxy_pos (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrounds : 0 < rounds) (hepisodes : forall n, 0 < episodes n) (hhorizon : 0 < mdp.horizon) (hrewardVarianceProxy : 0 < rewardVarianceProxy) : 0 < ((cumulativeSampledReturnDeviationVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)
Source line 468 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSampledReturnDeviation Compiled

Cumulative heterogeneous sampled-return deviation through `rounds`.

noncomputable def cumulativeSampledReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 502 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_cumulativeSampledReturnDeviation_abs_tail_le Compiled

Fixed-round two-sided tail on the heterogeneous causal law.

theorem trajectoryMeasure_cumulativeSampledReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSampledReturnDeviationVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (cumulativeSampledReturnDeviationVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) delta <= |source.cumulativeSampledReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta
Source line 515 Chapter context: Finite-horizon RL
class BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.GlobalReturnMeasurability Compiled

Measurability contract for history-selected globally centered returns.

class GlobalReturnMeasurability {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : Prop where
Source line 577 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnDeviation Compiled

Dynamic globally centered return on a heterogeneous prefix/batch pair.

noncomputable def successorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (pair : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1))) : Real
Source line 591 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_successorGlobalReturnDeviation Compiled

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

theorem measurable_successorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : Measurable (source.successorGlobalReturnDeviation n)
Source line 604 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnDeviationKernel Compiled

Selected conditional kernel of the globally centered successor return.

noncomputable def successorGlobalReturnDeviationKernel {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) : Kernel (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) Real
Source line 613 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnDeviationKernel_apply Compiled

Every global-return kernel fiber is the exact selected iid statistic law.

theorem successorGlobalReturnDeviationKernel_apply {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) (history : HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n) : source.successorGlobalReturnDeviationKernel n history = (source.rewardSource.iidStochasticTrajectoryFamilyMeasure (source.successorPolicy n history) initialState (episodes (n + 1))).map (mdp.globalSampledCumulativeReturnDeviationSum (source.successorPolicy n history) initialState (episodes (n + 1)))
Source line 636 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnDeviationAt Compiled

Globally centered return evaluated at successor coordinate `n + 1`.

noncomputable def successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (n : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 675 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_successorGlobalReturnDeviationAt Compiled

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

theorem measurable_successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) : Measurable (source.successorGlobalReturnDeviationAt n)
Source line 688 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_condDistrib_successorGlobalReturnDeviationAt Compiled

Dynamic conditional law of the globally centered successor return.

theorem trajectoryMeasure_condDistrib_successorGlobalReturnDeviationAt {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] : condDistrib (source.successorGlobalReturnDeviationAt n) (Preorder.frestrictLe n) source.trajectoryMeasure =ᵐ[ source.trajectoryMeasure.map (Preorder.frestrictLe n)] source.successorGlobalReturnDeviationKernel n
Source line 702 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.condExpKernel_map_successorGlobalReturnDeviationAt_eq Compiled

Trimmed conditional-expectation kernel form of the global-return law.

theorem condExpKernel_map_successorGlobalReturnDeviationAt_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] : Filter.Eventually (fun trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes => Measure.map (source.successorGlobalReturnDeviationAt n) (condExpKernel source.trajectoryMeasure ((inferInstance : MeasurableSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)).comap (Preorder.frestrictLe n)) trajectory) = source.successorGlobalReturnDeviationKernel n (Preorder.frestrictLe n trajectory)) (ae (source.trajectoryMeasure.trim (Preorder.measurable_frestrictLe n).comap_le))
Source line 733 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnPrefixIncrement Compiled

Prefix process with coordinate zero uncharged and successors globally centered.

noncomputable def successorGlobalReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) : (round : Nat) -> HeterogeneousStochasticEpisodeBatchPrefix mdp episodes round -> Real | 0, _history => 0 | n + 1, history => source.successorGlobalReturnDeviation n (Preorder.frestrictLe₂ (π
Source line 769 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_successorGlobalReturnPrefixIncrement Compiled

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

theorem measurable_successorGlobalReturnPrefixIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (round : Nat) : Measurable (source.successorGlobalReturnPrefixIncrement round)
Source line 787 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnIncrement Compiled

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

noncomputable def successorGlobalReturnIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 808 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnIncrement_stronglyAdapted_piLE Compiled

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

theorem successorGlobalReturnIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] : StronglyAdapted (Filtration.piLE (X
Source line 821 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorGlobalReturnIncrement_succ_hasCondSubgaussianMGF Compiled

Every successor global-return coordinate has its selected conditional MGF.

theorem successorGlobalReturnIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasCondSubgaussianMGF (Filtration.piLE (X
Source line 838 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy Compiled

Zero at coordinate zero plus heterogeneous global proxies at successors.

noncomputable def cumulativeSuccessorGlobalReturnVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal
Source line 957 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy_pos Compiled

Positive successor count and coordinate proxy imply a positive total proxy.

theorem cumulativeSuccessorGlobalReturnVarianceProxy_pos (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrounds : 0 < rounds) (hepisodes : forall n, 0 < episodes n) (hhorizon : 0 < mdp.horizon) (hrewardVarianceProxy : 0 < rewardVarianceProxy) : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)
Source line 971 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnDeviation Compiled

Cumulative globally centered deviation over successor coordinates only.

noncomputable def cumulativeSuccessorGlobalReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real
Source line 1016 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_abs_tail_le Compiled

Fixed-round successor-only globally centered two-sided tail.

theorem trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) delta <= |source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta
Source line 1029 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeSampledReturnDeviation_abs_tail_le Compiled

Concrete self-consistent schedule wrapper for the heterogeneous tail.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeSampledReturnDeviation_abs_tail_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (hrounds : 0 < rounds) (hhorizon : 0 < mdp.horizon) (hrewardVarianceProxy : 0 < rewardVarianceProxy) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSampledReturnDeviationVarianceProxy mdp (fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) rounds rewardBound rewardVarianceProxy) delta <= |source.cumulativeSampledReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta
Source line 1119 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_abs_tail_le Compiled

Self-consistent successor-only globally centered heterogeneous tail.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeSuccessorGlobalReturnDeviation_abs_tail_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (hrounds : 0 < rounds) (hhorizon : 0 < mdp.horizon) (hrewardVarianceProxy : 0 < rewardVarianceProxy) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp (fun n => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor n) rounds rewardBound rewardVarianceProxy) delta <= |source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta
Source line 1166 Chapter context: Finite-horizon RL