BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalReturnConcentration

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

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

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)))

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

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)

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

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))

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₂ (π := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) (Nat.le_succ n) history, history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) omit [DecidableEq State] [DecidableEq Action] [MeasurableSingletonClass State] [MeasurableSingletonClass Action] [Nonempty State] [Nonempty Action] in 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)

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)

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

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)

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 := fun n : Nat => StochasticEpisodeBatch mdp (episodes n))) source.sampledReturnDeviationIncrement

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

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 := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) n) ((Filtration.piLE (X := fun k : Nat => StochasticEpisodeBatch mdp (episodes k))).le n) (source.sampledReturnDeviationIncrement (n + 1)) (mdp.iidSampledCumulativeReturnDeviationVarianceProxy (episodes (n + 1)) rewardBound rewardVarianceProxy) source.trajectoryMeasure

Sum of coordinate-specific sampled-return variance proxies.

noncomputable def cumulativeSampledReturnDeviationVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal

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)

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

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

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

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

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)

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

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)))

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

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)

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

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))

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₂ (π := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) (Nat.le_succ n) history, history ⟨n + 1, Finset.mem_Iic.mpr le_rfl⟩) omit [DecidableEq State] [DecidableEq Action] [MeasurableSingletonClass State] [MeasurableSingletonClass Action] [Nonempty State] [Nonempty Action] in 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)

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)

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

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 := fun n : Nat => StochasticEpisodeBatch mdp (episodes n))) source.successorGlobalReturnIncrement

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 := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) n) ((Filtration.piLE (X := fun k : Nat => StochasticEpisodeBatch mdp (episodes k))).le n) (source.successorGlobalReturnIncrement (n + 1)) (mdp.iidGlobalSampledCumulativeReturnDeviationVarianceProxy (episodes (n + 1)) rewardBound rewardVarianceProxy) source.trajectoryMeasure

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

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)

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

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

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

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