BanditRLProof.RL.StoppedReturnJointErrorDeterministicTailHighProbability

The maximum of the six literal capped/uncapped stopped-return errors at one schedule index.

noncomputable def selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) → Real

The scalar joint error is nonnegative.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : 0 ≤ selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory

Every schedule-index coordinate of the scalar joint error is measurable.

theorem measurable_selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (scheduleIndex : Nat) : Measurable (selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex)

A strict scalar joint-error bound is exactly the conjunction of the same six literal stopped-return bounds.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError_lt_iff (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (scheduleIndex : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : 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 cappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let optimal := AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory < epsilon ↔ dist (cappedSampledReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (uncappedSampledReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (cappedPolicyReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (uncappedPolicyReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (cappedGap scheduleIndex trajectory) 0 < epsilon ∧ dist (uncappedGap scheduleIndex trajectory) 0 < epsilon

The accepted named weak-bad event is exactly the scalar joint-error weak superlevel set.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointViolationSet_eq_jointError_ge (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon scheduleIndex = {trajectory | epsilon ≤ selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory}

The accepted named strict-good event is exactly the scalar joint-error strict sublevel set.

theorem selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointGoodSet_eq_jointError_lt (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor epsilon : Real) (scheduleIndex : Nat) : selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointGoodSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor epsilon scheduleIndex = {trajectory | selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor scheduleIndex trajectory < epsilon}

Terminal scalar deterministic-tail confidence certificate. One noncomputable cutoff works for every later schedule index.

theorem selfConsistentScheduledCausalSource_inverseSqrtThresholdCappedUnboundedHittingAfter_stoppedSampledReturn_and_successorPolicyExpectedReturn_jointError_deterministicTailHighProbability_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 jointError := selfConsistentScheduledNaturalCausalInverseSqrtThresholdCappedUnboundedHittingAfterStoppedReturnJointError mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ epsilon delta, 0 < epsilon → 0 < delta → ∃ tailStart : Nat, ∀ scheduleIndex, tailStart ≤ scheduleIndex → Measurable (jointError scheduleIndex) ∧ MeasurableSet {trajectory | jointError scheduleIndex trajectory < epsilon} ∧ source.trajectoryMeasure {trajectory | epsilon ≤ jointError scheduleIndex trajectory} < ENNReal.ofReal delta ∧ 1 - delta < source.trajectoryMeasure.real {trajectory | jointError scheduleIndex trajectory < epsilon} ∧ ∀ trajectory, jointError scheduleIndex trajectory < epsilon ↔ 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 cappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor cappedStoppingPrefix let uncappedGap := selfConsistentScheduledNaturalCausalStoppingTimeAverageSampledPolicyExpectedReturnGapProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor uncappedStoppingPrefix let optimal := AdaptiveStochasticEpisodeBatchSource.optimalInitialExpectedReturn mdp initialState dist (cappedSampledReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (uncappedSampledReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (cappedPolicyReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (uncappedPolicyReturn scheduleIndex trajectory) optimal < epsilon ∧ dist (cappedGap scheduleIndex trajectory) 0 < epsilon ∧ dist (uncappedGap scheduleIndex trajectory) 0 < epsilon