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

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedSampledAndSuccessorPolicyReturnL1Optimality

# Stopped sampled and successor-policy return L1 optimality This module upgrades the stopped expectation-level consistency theorem to actual `L1` convergence. The sampled-return optimality error is exactly the negative realized behavior regret, the literal successor-policy return error is exactly the negative behavior expected regret, and their same-prefix gap is exactly the return deviation. The already compiled capped and genuine uncapped `hittingAfter` `L1` results therefore transport to all three return processes. The successor-policy process remains the literal trajectory-law expected return of the policy selected from the dependent prefix. No expectation is interchanged with a random stopping index, and no optional-stopping theorem is used.

Module map

Declarations
20
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedSampledReturnAndSuccessorPolicyExpectedReturnConsistency

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedSampledAndSuccessorPolicyReturnInMeasureAlmostSureOptimality

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_fun_neg Compiled

Eta-expanded negation has the same `eLpNorm`. This small wrapper keeps the return-process transport proofs independent of the syntactic representation of pointwise negation.

theorem eLpNorm_fun_neg {Omega : Type*} [MeasurableSpace Omega] (f : Omega -> Real) (p : ENNReal) (mu : Measure Omega) : eLpNorm (fun omega => -f omega) p mu = eLpNorm f p mu
Source line 39 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess Compiled

Sampled return centered at the optimal initial expected return.

noncomputable def selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess (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 46 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess Compiled

Literal successor-policy expected return centered at the optimal initial expected return.

noncomputable def selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess (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 73 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess Compiled

Same-prefix sampled return minus literal successor-policy expected return.

noncomputable def selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess (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 99 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess_eq_neg_realized Compiled

The stopped sampled-return optimality error is the negative stopped realized behavior regret, pointwise and before integration.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess_eq_neg_realized (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) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex = fun trajectory => -selfConsistentScheduledNaturalCausalStoppingTimeAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory
Source line 127 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess_eq_neg_behaviorExpected Compiled

The stopped literal successor-policy return optimality error is the negative stopped behavior expected regret.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess_eq_neg_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) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex = fun trajectory => -selfConsistentScheduledNaturalCausalStoppingTimeAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex trajectory
Source line 155 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess_eq_returnDeviation Compiled

The stopped sampled/policy return gap is exactly the stopped return deviation.

theorem selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess_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) : selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex = selfConsistentScheduledNaturalCausalStoppingTimeAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix scheduleIndex
Source line 183 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledReturnOptimalityError Compiled

Every capped stopped sampled-return optimality error belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledReturnOptimalityError (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 : 0 < 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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (errorProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 210 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledReturnOptimalityError_tendsto_zero Compiled

The capped sampled-return optimality error converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledReturnOptimalityError_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 : 0 < 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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (errorProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 246 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledReturnOptimalityError Compiled

Every uncapped `hittingAfter` stopped sampled-return optimality error belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledReturnOptimalityError (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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (errorProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 286 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledReturnOptimalityError_tendsto_zero Compiled

The genuine uncapped stopped sampled-return optimality error converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledReturnOptimalityError_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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (errorProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 323 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSuccessorPolicyExpectedReturnOptimalityError Compiled

Every capped stopped literal successor-policy return optimality error belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSuccessorPolicyExpectedReturnOptimalityError (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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (errorProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 363 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSuccessorPolicyExpectedReturnOptimalityError_tendsto_zero Compiled

The capped literal successor-policy return optimality error converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSuccessorPolicyExpectedReturnOptimalityError_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 : 0 < 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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (errorProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 393 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSuccessorPolicyExpectedReturnOptimalityError Compiled

Every genuine uncapped stopped literal successor-policy return optimality error belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSuccessorPolicyExpectedReturnOptimalityError (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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (errorProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 433 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSuccessorPolicyExpectedReturnOptimalityError_tendsto_zero Compiled

The genuine uncapped literal successor-policy return optimality error converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSuccessorPolicyExpectedReturnOptimalityError_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 : 0 < 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 errorProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (errorProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 463 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledPolicyExpectedReturnGap Compiled

Every capped stopped sampled/policy return gap belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledPolicyExpectedReturnGap (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 gapProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (gapProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 502 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledPolicyExpectedReturnGap_tendsto_zero Compiled

The capped stopped sampled/policy return gap converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedStoppedSampledPolicyExpectedReturnGap_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 gapProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (gapProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 538 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledPolicyExpectedReturnGap Compiled

Every genuine uncapped stopped sampled/policy return gap belongs to `L1`.

theorem memLp_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledPolicyExpectedReturnGap (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 gapProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix MemLp (gapProcess scheduleIndex) 1 source.trajectoryMeasure
Source line 576 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledPolicyExpectedReturnGap_tendsto_zero Compiled

The genuine uncapped stopped sampled/policy return gap converges to zero in `L1`.

theorem eLpNorm_one_selfConsistentScheduledNaturalCausalInverseSqrtThresholdUnboundedHittingAfterStoppedSampledPolicyExpectedReturnGap_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 gapProcess := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor stoppingPrefix Tendsto (fun scheduleIndex => eLpNorm (gapProcess scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 613 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedSampledReturn_and_successorPolicyExpectedReturn_L1_optimality Compiled

Terminal true-`L1` package for stopped sampled return, the literal return of the actually selected successor policies, and their same-prefix gap at both the capped first-passage approximation and genuine uncapped `hittingAfter`.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedSampledReturn_and_successorPolicyExpectedReturn_L1_optimality (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 cappedSampledError := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedSampledError := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedPolicyError := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedPolicyError := selfConsistentScheduledNaturalCausalStoppingTimeAverageSuccessorPolicyExpectedReturnOptimalityErrorProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let cappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix (forall scheduleIndex, MemLp (cappedSampledError scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, MemLp (uncappedSampledError scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, MemLp (cappedPolicyError scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, MemLp (uncappedPolicyError scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, MemLp (cappedGap scheduleIndex) 1 source.trajectoryMeasure) /\ (forall scheduleIndex, MemLp (uncappedGap scheduleIndex) 1 source.trajectoryMeasure) /\ Tendsto (fun scheduleIndex => eLpNorm (cappedSampledError scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (uncappedSampledError scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (cappedPolicyError scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (uncappedPolicyError scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (cappedGap scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0) /\ Tendsto (fun scheduleIndex => eLpNorm (uncappedGap scheduleIndex) 1 source.trajectoryMeasure) atTop (nhds 0)
Source line 653 Chapter context: Finite-horizon RL