BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityLogRate

Successor return deviation divided by the actual successor batch size. Coordinate zero is a dummy zero so coordinate `n + 1` remains conditioned on the prefix filtration at `n`.

noncomputable def naturalSuccessorAverageReturnDeviationIncrement {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (round : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real

Exact square-scaled conditional proxy for the normalized increment.

noncomputable def naturalSuccessorAverageReturnVarianceProxyAt (mdp : MDP State Action) (episodes : Nat -> Nat) (round : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal

Total proxy for normalized successor sample-average deviations.

noncomputable def naturalCumulativeSuccessorAverageReturnVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal

Cumulative normalized deviation over natural successor rounds.

noncomputable def naturalCumulativeSuccessorAverageReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) : Real

The normalized successor return process is strongly adapted to `piLE`.

theorem naturalSuccessorAverageReturnDeviationIncrement_stronglyAdapted_piLE {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] : StronglyAdapted (Filtration.piLE (X := fun n : Nat => StochasticEpisodeBatch mdp (episodes n))) source.naturalSuccessorAverageReturnDeviationIncrement

The normalized cumulative return deviation is measurable.

theorem measurable_naturalCumulativeSuccessorAverageReturnDeviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) : Measurable (source.naturalCumulativeSuccessorAverageReturnDeviation rounds)

Scalar transport of the selected conditional successor-return MGF.

theorem naturalSuccessorAverageReturnDeviationIncrement_succ_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (n : Nat) [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [StandardBorelSpace (StochasticEpisodeBatch mdp (episodes (n + 1)))] [Nonempty (StochasticEpisodeBatch mdp (episodes (n + 1)))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) : HasCondSubgaussianMGF (Filtration.piLE (X := fun k : Nat => StochasticEpisodeBatch mdp (episodes k)) n) ((Filtration.piLE (X := fun k : Nat => StochasticEpisodeBatch mdp (episodes k))).le n) (source.naturalSuccessorAverageReturnDeviationIncrement (n + 1)) (naturalSuccessorAverageReturnVarianceProxyAt mdp episodes (n + 1) rewardBound rewardVarianceProxy) source.trajectoryMeasure

A positive prefix has positive normalized total return proxy.

theorem naturalCumulativeSuccessorAverageReturnVarianceProxy_pos (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrounds : 0 < rounds) (hepisodes : forall n, 0 < episodes n) (hrewardBound_pos : 0 < rewardBound) (hhorizon : 0 < mdp.horizon) : 0 < ((naturalCumulativeSuccessorAverageReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)

Fixed-prefix two-sided tail for normalized successor sample-average returns.

theorem trajectoryMeasure_naturalCumulativeSuccessorAverageReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} [StandardBorelSpace State] [StandardBorelSpace Action] [forall n, StandardBorelSpace (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, Nonempty (HeterogeneousStochasticEpisodeBatchPrefix mdp episodes n)] [forall n, StandardBorelSpace (StochasticEpisodeBatch mdp (episodes n))] [forall n, Nonempty (StochasticEpisodeBatch mdp (episodes n))] [StandardBorelSpace (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)] (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((naturalCumulativeSuccessorAverageReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (naturalCumulativeSuccessorAverageReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) delta <= |source.naturalCumulativeSuccessorAverageReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta

The dummy-zero process is exactly the natural successor-round sum.

theorem naturalCumulativeSuccessorAverageReturnDeviation_eq_sum_range {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.naturalCumulativeSuccessorAverageReturnDeviation rounds trajectory = ∑ t ∈ Finset.range rounds, ((episodes (t + 1) : Real)⁻¹) * source.successorGlobalReturnIncrement (t + 1) trajectory

Realized regret of the sample average in successor batch `t + 1`.

noncomputable def naturalSuccessorBatchAverageRealizedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (_source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (t : Nat) : Real

Natural-prefix cumulative successor-batch-average realized regret.

noncomputable def naturalCumulativeRealizedBehaviorRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

Natural-prefix round-average realized behavior regret.

noncomputable def naturalAverageRealizedBehaviorRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : Real

A successor-batch-average realized-regret coordinate is measurable.

theorem measurable_naturalSuccessorBatchAverageRealizedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (t : Nat) : Measurable (fun trajectory => source.naturalSuccessorBatchAverageRealizedRegret trajectory t)

The natural cumulative realized behavior-regret process is measurable.

theorem measurable_naturalCumulativeRealizedBehaviorRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.naturalCumulativeRealizedBehaviorRegret trajectory rounds)

The natural round-average realized behavior-regret process is measurable.

theorem measurable_naturalAverageRealizedBehaviorRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) : Measurable (fun trajectory => source.naturalAverageRealizedBehaviorRegret trajectory rounds)

Exact one-round batch-average realized/expected/deviation identity.

theorem naturalSuccessorBatchAverageRealizedRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (t : Nat) (hepisodes : 0 < episodes (t + 1)) : source.naturalSuccessorBatchAverageRealizedRegret trajectory t = (source.successorPolicyAt trajectory t).expectedRegret initialState - source.naturalSuccessorAverageReturnDeviationIncrement (t + 1) trajectory

Exact natural-prefix cumulative expected-minus-normalized-deviation identity.

theorem naturalCumulativeRealizedBehaviorRegret_eq_expected_sub_deviation {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hepisodes : forall n, 0 < episodes n) : source.naturalCumulativeRealizedBehaviorRegret trajectory rounds = (∑ t ∈ Finset.range rounds, (source.successorPolicyAt trajectory t).expectedRegret initialState) - source.naturalCumulativeSuccessorAverageReturnDeviation rounds trajectory

Self-consistent normalized successor-return proxy for a natural prefix.

noncomputable def selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : NNReal

Normalized successor-return deviation on the self-consistent causal source.

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

Natural cumulative successor-batch-average realized behavior regret.

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

Natural round-average successor-batch-average realized behavior regret.

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

Fixed-prefix two-sided normalized return-deviation event.

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

The self-consistent normalized return-deviation process is measurable.

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

The natural cumulative batch-average realized-regret process is measurable.

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

The natural round-average batch-average realized-regret process is measurable.

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

The fixed-prefix normalized return event is measurable.

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

Exact natural-prefix cumulative realized/expected/deviation identity.

theorem selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_eq_expected_sub_deviation (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory = selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory - selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory

Exact natural-prefix round-average realized/expected/deviation identity.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_eq_expected_sub_deviation (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory = (selfConsistentScheduledNaturalCausalCumulativeBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory - selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) / (rounds : Real)

The self-consistent normalized return event has its exact return share.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_naturalCumulativeReturnBadEvent_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) (rounds : Nat) (hrounds : 0 < rounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (selfConsistentScheduledNaturalCausalCumulativeReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta) <= ENNReal.ofReal returnDelta

Logarithmic model rate plus the normalized successor-return radius.

noncomputable def selfConsistentScheduledNaturalCausalRealizedCumulativeLogarithmicRate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (returnDelta : Real) : Real

Round-average form of the fixed-prefix realized logarithmic rate.

noncomputable def selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) (returnDelta : Real) : Real

Union of the actual finite-prefix model event and normalized return event.

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

One-sided cumulative realized-regret violation set.

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

One-sided round-average realized-regret violation set.

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

The cumulative realized-regret violation set is Borel measurable.

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

The average realized-regret violation set is Borel measurable.

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

The model/return union is measurable and obeys the sum of its two shares.

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

Outside the joint event, cumulative realized regret obeys the explicit rate.

theorem selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_le_logarithmic_of_not_mem_modelReturnBadEvent (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) (returnDelta : Real) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta) : selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalRealizedCumulativeLogarithmicRate mdp varianceProxy baseVisitFloor rounds returnDelta

Outside the joint event, average realized regret obeys the divided rate.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_logarithmic_of_not_mem_modelReturnBadEvent (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) (hrounds : 0 < rounds) (returnDelta : Real) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t)) (htrajectory : trajectory ∉ selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor rounds returnDelta

Every cumulative realized-regret violation lies in the joint event.

theorem selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet_subset_modelReturnBadEvent (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) (returnDelta : Real) : selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta ⊆ selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta

Every average realized-regret violation lies in the joint event.

theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_modelReturnBadEvent (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) (hrounds : 0 < rounds) (returnDelta : Real) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta ⊆ selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta

Every average realized-regret violation lies in the joint event. -/ theorem selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_modelReturnBadEvent (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) (hrounds : 0 < rounds) (returnDelta : Real) : selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta ⊆ selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta := by intro trajectory hviolation by_contra hgood have hbound := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_logarithmic_of_not_mem_modelReturnBadEvent mdp initialState rewardSource varianceProxy hvarianceProxy law initialTable defaultState support baseVisitFloor hbaseFloor hrewardBound hhorizon hbaseVisitFloor rounds hrounds returnDelta trajectory hgood exact (not_lt_of_ge hbound) hviolation /- Terminal fixed-prefix realized route. The model/return event and both one-sided realized-regret violation sets are measurable, both violations are covered by the joint event, all three probabilities use the sum of the actual model budget and the caller's return share, and every joint-good trajectory has the cumulative and round-average logarithmic certificates.

theorem selfConsistentScheduledCausalSource_fixedPrefixHighProbabilityLogarithmicCumulativeAverageRealizedBehaviorRegret (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) (hrounds : 0 < rounds) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledNaturalCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta let cumulativeViolation := selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta let averageViolation := selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta let failureBudget := selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal returnDelta MeasurableSet event ∧ MeasurableSet cumulativeViolation ∧ MeasurableSet averageViolation ∧ source.trajectoryMeasure event <= failureBudget ∧ cumulativeViolation ⊆ event ∧ averageViolation ⊆ event ∧ source.trajectoryMeasure cumulativeViolation <= failureBudget ∧ source.trajectoryMeasure averageViolation <= failureBudget ∧ (failureBudget < 1 -> source.trajectoryMeasure event < 1 ∧ source.trajectoryMeasure cumulativeViolation < 1 ∧ source.trajectoryMeasure averageViolation < 1) ∧ ∀ trajectory, trajectory ∉ event -> selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalRealizedCumulativeLogarithmicRate mdp varianceProxy baseVisitFloor rounds returnDelta ∧ selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory <= selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate mdp varianceProxy baseVisitFloor rounds returnDelta