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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedSampledReturnAndSuccessorPolicyExpectedReturnConsistency

# Stopped sampled-return and successor-policy expected-return consistency This module gives a literal policy-value interpretation to the stopped sampled-return theorem. At coordinate `t`, the successor policy is the actual exploratory policy selected from the dependent prefix through `t`; its expected return is the integral of cumulative reward under its generated trajectory law. These literal policy returns are averaged over the same natural prefix as the sampled-return and regret processes, with the optimal initial expected return at the empty prefix. The exact same-prefix identity says that sampled return minus successor-policy expected return is the normalized return deviation. It is transported to the capped first-passage approximation and the genuine uncapped `hittingAfter` prefix, then through Bochner integration. No expectation is interchanged with a random stopping index, and no optional-stopping theorem is used.

Module map

Declarations
29
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedAverageSampledReturnExpectedOptimality

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedSampledAndSuccessorPolicyReturnL1Optimality

Declarations

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

def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorPolicyExpectedReturn Compiled

Literal expected cumulative reward of the successor policy selected from the dependent prefix through `t`.

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

The literal successor-policy return is optimal value minus that policy's expected regret.

theorem naturalSuccessorPolicyExpectedReturn_eq_optimal_sub_expectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (t : Nat) : source.naturalSuccessorPolicyExpectedReturn trajectory t = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - (source.successorPolicyAt trajectory t).expectedRegret initialState
Source line 55 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalAverageSuccessorPolicyExpectedReturn Compiled

Equal-round average of literal successor-policy expected returns. The empty prefix uses the optimal initial expected return.

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

At every prefix, the literal policy-return average is optimal value minus the average successor-policy expected regret.

theorem naturalAverageSuccessorPolicyExpectedReturn_eq_optimal_sub_expectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.naturalAverageSuccessorPolicyExpectedReturn trajectory rounds = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - (∑ t ∈ Finset.range rounds, (source.successorPolicyAt trajectory t).expectedRegret initialState) / (rounds : Real)
Source line 92 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess Compiled

Natural-prefix average of literal expected returns of the actual successor policies selected by the self-consistent causal source.

noncomputable def selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real
Source line 131 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess_eq_optimal_sub_behaviorExpected Compiled

The literal prefix policy return is the complement of the existing average behavior expected-regret process.

theorem selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess_eq_optimal_sub_behaviorExpected (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (trajectory) : selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory
Source line 150 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess Compiled

Every deterministic-prefix literal policy-return coordinate is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Measurable (selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)
Source line 179 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess Compiled

Literal average successor-policy expected return evaluated at a `WithTop Nat` stopping prefix.

noncomputable def selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> Real
Source line 213 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess_apply Compiled

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

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess_apply (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory = selfConsistentScheduledNaturalCausalAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (stoppingPrefix scheduleIndex trajectory).untopA trajectory
Source line 238 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess_eq_optimal_sub_behaviorExpected Compiled

Stopping preserves the exact literal policy-return/behavior-regret complement.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess_eq_optimal_sub_behaviorExpected (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory
Source line 263 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess Compiled

A stopping time gives a measurable stopped literal policy-return coordinate.

theorem measurable_selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (hstopping : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (stoppingPrefix scheduleIndex)) : Measurable (selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex)
Source line 295 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_stoppedSuccessorPolicyExpectedReturn_of_integrable_behavior Compiled

Integrability transfers from a stopped behavior expected-regret process to its literal policy-return complement.

theorem integrable_stoppedSuccessorPolicyExpectedReturn_of_integrable_behavior {Omega : Type w} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (optimal : Real) (policyReturn behaviorRegret : Omega -> Real) (hpoint : forall omega, policyReturn omega = optimal - behaviorRegret omega) (hbehavior : Integrable behaviorRegret mu) : Integrable policyReturn mu
Source line 340 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integral_stoppedSuccessorPolicyExpectedReturn_eq_optimal_sub_behavior Compiled

The expectation of a stopped literal policy return is the optimal constant minus the expected behavior regret.

theorem integral_stoppedSuccessorPolicyExpectedReturn_eq_optimal_sub_behavior {Omega : Type w} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (optimal : Real) (policyReturn behaviorRegret : Omega -> Real) (hpoint : forall omega, policyReturn omega = optimal - behaviorRegret omega) (hbehavior : Integrable behaviorRegret mu) : integral mu policyReturn = optimal - integral mu behaviorRegret
Source line 354 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturn_sub_successorPolicyExpectedReturn_eq_returnDeviation Compiled

At any common stopping prefix, observed sampled return minus the literal successor-policy expected return is exactly the normalized return deviation.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturn_sub_successorPolicyExpectedReturn_eq_returnDeviation (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (stoppingPrefix : Nat -> HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (scheduleIndex : Nat) (trajectory) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory - selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory = selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory
Source line 369 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturn Compiled

Every capped stopped literal successor-policy expected-return coordinate is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturn (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Measurable (selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) scheduleIndex)
Source line 400 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturn Compiled

Every genuine uncapped stopped literal successor-policy expected-return coordinate is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturn (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Measurable (selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) scheduleIndex)
Source line 430 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturn Compiled

The capped stopped literal successor-policy expected return is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturn (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Integrable (policyReturn scheduleIndex) source.trajectoryMeasure
Source line 456 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturn Compiled

The genuine uncapped stopped literal successor-policy expected return is integrable.

theorem integrable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturn (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Integrable (policyReturn scheduleIndex) source.trajectoryMeasure
Source line 511 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturnIntegral_eq_optimal_sub_behaviorExpected Compiled

For the capped prefix, expected literal policy return is exactly optimal value minus expected behavior regret.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturnIntegral_eq_optimal_sub_behaviorExpected (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let behaviorRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (policyReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (behaviorRegret scheduleIndex)
Source line 566 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturnIntegral_eq_optimal_sub_behaviorExpected Compiled

For the genuine uncapped prefix, expected literal policy return is exactly optimal value minus expected behavior regret.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturnIntegral_eq_optimal_sub_behaviorExpected (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (scheduleIndex : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let behaviorRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (policyReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (behaviorRegret scheduleIndex)
Source line 616 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnIntegral_sub_successorPolicyExpectedReturnIntegral_eq_returnDeviationIntegral Compiled

At the capped prefix, the expected sampled/policy-return gap is exactly the expected return deviation.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnIntegral_sub_successorPolicyExpectedReturnIntegral_eq_returnDeviationIntegral (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 := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let returnDeviation := selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex) = integral source.trajectoryMeasure (returnDeviation scheduleIndex)
Source line 666 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnIntegral_sub_successorPolicyExpectedReturnIntegral_eq_returnDeviationIntegral Compiled

At the genuine uncapped prefix, the expected sampled/policy-return gap is exactly the expected return deviation.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnIntegral_sub_successorPolicyExpectedReturnIntegral_eq_returnDeviationIntegral (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 sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let returnDeviation := selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex) = integral source.trajectoryMeasure (returnDeviation scheduleIndex)
Source line 725 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnSuccessorPolicyExpectedReturnGap_tendsto_zero Compiled

The capped expected sampled/policy-return gap tends to zero.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnSuccessorPolicyExpectedReturnGap_tendsto_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex)) atTop (nhds 0)
Source line 783 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnSuccessorPolicyExpectedReturnGap_tendsto_zero Compiled

The genuine uncapped expected sampled/policy-return gap tends to zero.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnSuccessorPolicyExpectedReturnGap_tendsto_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex)) atTop (nhds 0)
Source line 859 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnSuccessorPolicyExpectedReturnAbsGap_tendsto_zero Compiled

The absolute capped expected sampled/policy-return gap tends to zero.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSampledReturnSuccessorPolicyExpectedReturnAbsGap_tendsto_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => |integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex)|) atTop (nhds 0)
Source line 935 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnSuccessorPolicyExpectedReturnAbsGap_tendsto_zero Compiled

The absolute genuine uncapped expected sampled/policy-return gap tends to zero.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSampledReturnSuccessorPolicyExpectedReturnAbsGap_tendsto_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let sampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => |integral source.trajectoryMeasure (sampledReturn scheduleIndex) - integral source.trajectoryMeasure (policyReturn scheduleIndex)|) atTop (nhds 0)
Source line 976 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturnIntegral_tendsto_optimal Compiled

Expected literal successor-policy return at the capped prefix converges to the optimal initial expected return.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedAverageSuccessorPolicyExpectedReturnIntegral_tendsto_optimal (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (policyReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState))
Source line 1017 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturnIntegral_tendsto_optimal Compiled

Expected literal successor-policy return at the genuine uncapped prefix converges to the optimal initial expected return.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedAverageSuccessorPolicyExpectedReturnIntegral_tendsto_optimal (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let policyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => integral source.trajectoryMeasure (policyReturn scheduleIndex)) atTop (nhds (AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState))
Source line 1084 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedSampledReturn_and_successorPolicyExpectedReturn_consistency Compiled

Terminal literal policy-return semantics and stopped expected-consistency package for the capped approximation and genuine uncapped stopping prefix.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedSampledReturn_and_successorPolicyExpectedReturn_consistency (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let cappedStoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedDoubleLinearRawWindowFirstPassageStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let uncappedStoppingPrefix := selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppingPrefix mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let cappedSampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedSampledReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedPolicyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedPolicyReturn := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedReturnDeviation := selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedReturnDeviation := selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedBehaviorRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedBehaviorRegret := selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix (forall scheduleIndex trajectory, cappedPolicyReturn scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - cappedBehaviorRegret scheduleIndex trajectory /\ uncappedPolicyReturn scheduleIndex trajectory = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - uncappedBehaviorRegret scheduleIndex trajectory /\ cappedSampledReturn scheduleIndex trajectory - cappedPolicyReturn scheduleIndex trajectory = cappedReturnDeviation scheduleIndex trajectory /\ uncappedSampledReturn scheduleIndex trajectory - uncappedPolicyReturn scheduleIndex trajectory = uncappedReturnDeviation scheduleIndex trajectory) /\ (forall scheduleIndex, Measurable (cappedPolicyReturn scheduleIndex) /\ Measurable (uncappedPolicyReturn scheduleIndex) /\ Integrable (cappedPolicyReturn scheduleIndex) source.trajectoryMeasure /\ Integrable (uncappedPolicyReturn scheduleIndex) source.trajectoryMeasure /\ integral source.trajectoryMeasure (cappedPolicyReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (cappedBehaviorRegret scheduleIndex) /\ integral source.trajectoryMeasure (uncappedPolicyReturn scheduleIndex) = AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState - integral source.trajectoryMeasure (uncappedBehaviorRegret scheduleIndex) /\ integral source.trajectoryMeasure (cappedSampledReturn scheduleIndex) - integral source.trajectoryMeasure (cappedPolicyReturn scheduleIndex) = integral source.trajectoryMeasure (cappedReturnDeviation scheduleIndex) /\ integral source.trajectoryMeasure (uncappedSampledReturn scheduleIndex) -
Source line 1151 Chapter context: Finite-horizon RL