BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeSingleModelEventHighProbabilityAverageRealizedBehaviorRegret

A finite-horizon heterogeneous bad-event union is monotone in its outer horizon when the underlying coordinate event family is unchanged.

theorem finiteHorizonBadEvent_mono {mdp : MDP State Action} {episodes : Nat -> Nat} {rounds maxRounds : Nat} {initialBad : Set (StochasticEpisodeBatch mdp (episodes 0))} {successorBad : (n : Nat) -> Set (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n × StochasticEpisodeBatch mdp (episodes (n + 1)))} (hrounds : rounds <= maxRounds) : finiteHorizonBadEvent rounds initialBad successorBad ⊆ finiteHorizonBadEvent maxRounds initialBad successorBad

The actual self-consistent model-confidence event at a prefix is contained in the corresponding event at every larger deterministic horizon.

theorem selfConsistentScheduledCausalModelBadEvent_mono (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) {rounds maxRounds : Nat} (hrounds : rounds <= maxRounds) : selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds ⊆ selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds

Equal allocation of one global return confidence budget over the possible positive stopped prefixes.

noncomputable def selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare (maxRounds : Nat) (returnDelta : Real) : Real

A positive deterministic horizon has at least one positive prefix.

theorem selfConsistentScheduledNaturalCausalPositivePrefixIndex_nonempty (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) : (Finset.Icc 1 maxRounds).Nonempty

The equal return share is positive and at most one.

theorem selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare_spec (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : 0 < selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta ∧ selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta <= 1

Finite window containing only the return-deviation events at the possible positive stopped prefixes.

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

The finite return-only window is ambient measurable.

theorem measurableSet_selfConsistentScheduledNaturalCausalBoundedStoppingReturnBadEventWindow (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (maxRounds : Nat) (returnDelta : Real) : MeasurableSet (selfConsistentScheduledNaturalCausalBoundedStoppingReturnBadEventWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta)

Equal allocation bounds the finite return-deviation window by the one global return confidence budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingReturnBadEventWindow_le (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] [StandardBorelSpace State] [StandardBorelSpace Action] (rewardSource : mdp.MeanCompatibleRewardKernel) (varianceProxy : NNReal) (law : rewardSource.UniformSubgaussianRewardLaw varianceProxy) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalBoundedStoppingReturnBadEventWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta) <= ENNReal.ofReal returnDelta

One horizon model-confidence event joined with the finite return-only window for all possible positive stopped prefixes.

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

Every positive fixed-prefix average-regret violation with the equal return share lies in the single horizon model event or the return-only window.

theorem selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow_subset_boundedStoppingSingleModelReturnBadEvent (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) (maxRounds : Nat) (returnDelta : Real) : selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds (fun _ => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta) ⊆ selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta

The single-model return event is measurable and is charged by one horizon model budget plus the one global return budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingSingleModelReturnBadEvent_le (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) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta MeasurableSet event ∧ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelFailureBudget mdp maxRounds + ENNReal.ofReal returnDelta

The stopped violation is contained in the sharper single-model return event.

theorem selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_subset_singleModelReturnBadEvent (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) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (maxRounds : Nat) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) (returnDelta : Real) : selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (fun _ => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta) tau ⊆ selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta

The stopped violation is contained in the sharper single-model return event. -/ theorem selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_subset_singleModelReturnBadEvent (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) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (maxRounds : Nat) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) (returnDelta : Real) : selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (fun _ => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta) tau ⊆ selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta := by exact (selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_subset_positivePrefixWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (fun _ => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta) tau maxRounds htau_pos htau_le).trans (selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow_subset_boundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor maxRounds returnDelta) /- Terminal bounded-stopping route with one charged model-confidence event. The stopping-time premise proves filtered measurability; the probability bound is inherited from pathwise finite-prefix containment.

theorem selfConsistentScheduledCausalSource_boundedStoppingTimeSingleModelEventHighProbabilityAverageRealizedBehaviorRegret (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) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (htau : IsStoppingTime (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) tau) (maxRounds : Nat) (hmaxRounds : 0 < maxRounds) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let returnDeltaAt := fun _ : Nat => selfConsistentScheduledNaturalCausalBoundedStoppingEqualReturnShare maxRounds returnDelta let stoppedViolation := selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau let event := selfConsistentScheduledNaturalCausalBoundedStoppingSingleModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDelta let failureBudget := selfConsistentScheduledCausalModelFailureBudget mdp maxRounds + ENNReal.ofReal returnDelta MeasurableSet[ selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds] stoppedViolation ∧ MeasurableSet event ∧ stoppedViolation ⊆ event ∧ source.trajectoryMeasure event <= failureBudget ∧ source.trajectoryMeasure stoppedViolation <= failureBudget ∧ (failureBudget < 1 -> source.trajectoryMeasure stoppedViolation < 1) ∧ forall trajectory, trajectory ∉ event -> selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau trajectory <= selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau trajectory