BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretHighProbabilityLogRate

Natural-prefix sum of the causal planning-rate coordinates.

noncomputable def selfConsistentScheduledNaturalCausalCumulativePlanningRate (mdp : MDP State Action) (rounds : Nat) : Real

The pathwise planning sum is dominated by the integrated finite-prefix sum.

theorem selfConsistentScheduledNaturalCausalCumulativePlanningRate_le_integrated (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativePlanningRate mdp rounds <= selfConsistentScheduledNaturalCausalCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds

The natural-prefix planning sum has the existing explicit logarithmic envelope.

theorem selfConsistentScheduledNaturalCausalCumulativePlanningRate_le_logarithmic (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativePlanningRate mdp rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds

The accumulated prefix budget is exactly the finite sum of both model shares.

theorem selfConsistentScheduledCausalModelFailureBudget_eq_fin_sum (mdp : MDP State Action) (rounds : Nat) : selfConsistentScheduledCausalModelFailureBudget mdp rounds = ∑ round : Fin rounds, (ENNReal.ofReal (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp round) + ENNReal.ofReal (AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledLocalDelta mdp round))

Avoiding the prefix event implies avoiding every coordinate event in it.

theorem not_mem_selfConsistentScheduledCausalModelRoundBadEvent_of_not_mem_prefix (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) {rounds t : Nat} (ht : t < rounds) (hprefix : trajectory ∉ selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) : trajectory ∉ selfConsistentScheduledCausalModelRoundBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor t

The random natural-prefix cumulative behavior expected-regret process is measurable.

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

Off the finite-prefix model event, the actual process obeys the planning sum.

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_planning_of_not_mem_modelBadEvent (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) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (htrajectory : trajectory ∉ selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) : selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalCumulativePlanningRate mdp rounds

Off the finite-prefix model event, the actual process obeys the log envelope.

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess_le_logarithmic_of_not_mem_modelBadEvent (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) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun s => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor s)) (htrajectory : trajectory ∉ selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) : selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds

One-sided fixed-prefix violation event for the random cumulative process.

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

The fixed-prefix logarithmic violation event is measurable.

theorem measurableSet_selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : MeasurableSet (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)

Every logarithmic violation lies in the actual finite-prefix model event.

theorem selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet_subset_modelBadEvent (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) (rounds : Nat) : selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds ⊆ selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds

The one-sided logarithmic violation probability uses the exact prefix budget.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeBehaviorExpectedRegretLogarithmicViolationSet_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) (rounds : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) <= selfConsistentScheduledCausalModelFailureBudget mdp rounds

The one-sided logarithmic violation probability uses the exact prefix budget. -/ theorem selfConsistentScheduledCausalSource_trajectoryMeasure_cumulativeBehaviorExpectedRegretLogarithmicViolationSet_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) (rounds : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) <= selfConsistentScheduledCausalModelFailureBudget mdp rounds := by dsimp only let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds calc source.trajectoryMeasure (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds) <= source.trajectoryMeasure event := measure_mono (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet_subset_modelBadEvent mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor rounds) _ <= selfConsistentScheduledCausalModelFailureBudget mdp rounds := by have hparent := selfConsistentScheduledCausalSource_trajectoryMeasure_allCoordinateConfidence_optimism_and_recommendedExpectedRegret mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor rounds simpa [source, event] using hparent.2.1 /- Terminal fixed-prefix route: the model and violation events are measurable, the violation is contained in the model event, both probability controls use the exact accumulated model-confidence budget, and every model-good path has the explicit planning-sum and logarithmic cumulative bounds.

theorem selfConsistentScheduledCausalSource_fixedPrefixHighProbabilityLogarithmicCumulativeBehaviorExpectedRegret (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) (rounds : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds let violation := selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds MeasurableSet event ∧ MeasurableSet violation ∧ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelFailureBudget mdp rounds ∧ violation ⊆ event ∧ source.trajectoryMeasure violation <= selfConsistentScheduledCausalModelFailureBudget mdp rounds ∧ ∀ trajectory, trajectory ∉ event -> selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalCumulativePlanningRate mdp rounds ∧ selfConsistentScheduledNaturalCausalCumulativePlanningRate mdp rounds <= selfConsistentScheduledNaturalCausalLogarithmicCumulativeIntegratedBehaviorExpectedRegretRate mdp rounds