BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeHighProbabilityAverageRealizedBehaviorRegret

A positive `WithTop Nat` time bounded by a finite horizon has a positive finite `untopA` value in the same deterministic range.

theorem one_le_untopA_and_untopA_le_of_withTop_bounds {Omega : Type*} (tau : Omega -> WithTop Nat) (maxRounds : Nat) (htau_pos : forall omega, (1 : WithTop Nat) <= tau omega) (htau_le : forall omega, tau omega <= (maxRounds : WithTop Nat)) (omega : Omega) : 1 <= (tau omega).untopA /\ (tau omega).untopA <= maxRounds

The prefix-scheduled deterministic logarithmic rate is strongly adapted to the natural trajectory filtration.

theorem selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate_stronglyAdapted (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (returnDeltaAt : Nat -> Real) : StronglyAdapted (selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor) (fun rounds (_trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) => selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor rounds (returnDeltaAt rounds))

Exact natural average realized behavior regret evaluated at one stopping time.

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

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

theorem selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret_apply (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau trajectory = selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (tau trajectory).untopA trajectory

The scheduled logarithmic average rate evaluated at the same stopping time.

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

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

theorem selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate_apply (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (returnDeltaAt : Nat -> Real) (tau : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) -> WithTop Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau trajectory = selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor (tau trajectory).untopA (returnDeltaAt (tau trajectory).untopA)

One-sided violation of the stopped logarithmic average-rate certificate.

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

A bounded stopping-time violation is measurable at the deterministic natural-filtration bound.

theorem measurableSet_selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (returnDeltaAt : Nat -> Real) (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) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) : MeasurableSet[ selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds] (selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau)

Finite union of all positive fixed-prefix average-regret violations through the deterministic stopping-time bound.

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

The finite positive-prefix violation window is ambient measurable.

theorem measurableSet_selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (maxRounds : Nat) (returnDeltaAt : Nat -> Real) : MeasurableSet (selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDeltaAt)

Every positive bounded stopped violation occurs at one fixed prefix in the finite window.

theorem selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_subset_positivePrefixWindow (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (returnDeltaAt : Nat -> Real) (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)) : selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau ⊆ selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDeltaAt

The positive-prefix violation window has the exact finite sum of the per-prefix model and return failure budgets.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_positivePrefixAverageRealizedBehaviorRegretViolationWindow_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) (returnDeltaAt : Nat -> Real) (hreturnDeltaAt : forall rounds, rounds ∈ Finset.Icc 1 maxRounds -> 0 < returnDeltaAt rounds /\ returnDeltaAt rounds <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDeltaAt) <= ∑ rounds ∈ Finset.Icc 1 maxRounds, (selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal (returnDeltaAt rounds))

The stopped violation inherits the same explicit finite-window budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_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) (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)) (returnDeltaAt : Nat -> Real) (hreturnDeltaAt : forall rounds, rounds ∈ Finset.Icc 1 maxRounds -> 0 < returnDeltaAt rounds /\ returnDeltaAt rounds <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau) <= ∑ rounds ∈ Finset.Icc 1 maxRounds, (selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal (returnDeltaAt rounds))

The stopped violation inherits the same explicit finite-window budget. -/ theorem selfConsistentScheduledCausalSource_trajectoryMeasure_boundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_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) (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)) (returnDeltaAt : Nat -> Real) (hreturnDeltaAt : forall rounds, rounds ∈ Finset.Icc 1 maxRounds -> 0 < returnDeltaAt rounds /\ returnDeltaAt rounds <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau) <= ∑ rounds ∈ Finset.Icc 1 maxRounds, (selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal (returnDeltaAt rounds)) := by dsimp only have hsubset : selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau ⊆ selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDeltaAt := selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet_subset_positivePrefixWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau maxRounds htau_pos htau_le have hwindow := selfConsistentScheduledCausalSource_trajectoryMeasure_positivePrefixAverageRealizedBehaviorRegretViolationWindow_le mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor maxRounds returnDeltaAt hreturnDeltaAt exact (measure_mono hsubset).trans hwindow /- The terminal packages filtered stopped-event measurability, ambient window measurability, pathwise containment, exact finite-sum probability bounds, and the stopped logarithmic certificate outside the finite violation window.

theorem selfConsistentScheduledCausalSource_boundedStoppingTimeHighProbabilityAverageRealizedBehaviorRegret (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) (htau_pos : forall trajectory, (1 : WithTop Nat) <= tau trajectory) (htau_le : forall trajectory, tau trajectory <= (maxRounds : WithTop Nat)) (returnDeltaAt : Nat -> Real) (hreturnDeltaAt : forall rounds, rounds ∈ Finset.Icc 1 maxRounds -> 0 < returnDeltaAt rounds /\ returnDeltaAt rounds <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let stoppedViolation := selfConsistentScheduledNaturalCausalBoundedStoppingTimeAverageRealizedBehaviorRegretViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau let violationWindow := selfConsistentScheduledNaturalCausalPositivePrefixAverageRealizedBehaviorRegretViolationWindow mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds returnDeltaAt let failureBudget := ∑ rounds ∈ Finset.Icc 1 maxRounds, (selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal (returnDeltaAt rounds)) MeasurableSet[ selfConsistentScheduledNaturalCausalTrajectoryFiltration mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor maxRounds] stoppedViolation /\ MeasurableSet violationWindow /\ stoppedViolation ⊆ violationWindow /\ source.trajectoryMeasure violationWindow <= failureBudget /\ source.trajectoryMeasure stoppedViolation <= failureBudget /\ (failureBudget < 1 -> source.trajectoryMeasure stoppedViolation < 1) /\ forall trajectory, trajectory ∉ violationWindow -> selfConsistentScheduledNaturalCausalStoppedAverageRealizedBehaviorRegret mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor tau trajectory <= selfConsistentScheduledNaturalCausalStoppedRealizedAverageLogarithmicRate mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor returnDeltaAt tau trajectory