BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityLogRate

# Fixed-prefix high-probability natural causal realized behavior regret This module converts the compiled fixed-prefix logarithmic behavior-expected regret route into a realized route on the same heterogeneous dependent causal source. Natural round `t` uses the sample average of the actual successor batch at coordinate `t + 1`, generated by the exploratory policy selected from the prefix through `t`. The return process keeps coordinate zero equal to zero and divides each globally centered successor-batch return by its own positive batch size. Mathlib's scalar sub-Gaussian MGF transport therefore multiplies the existing conditional proxy by the square of that reciprocal. The existing strongly-adapted finite-sum theorem gives a fixed-prefix two-sided return tail. Regularity: finite nonempty measurable State/Action with measurable singletons, a probability initial law, Standard Borel source spaces, positive round count and scheduled batch sizes, bounded stored means, a uniform selected-reward sub-Gaussian law, positive horizon/proxy/base floor, and exploratory path support. Failure policy: preserve the actual causal source, successor indexing, global initial-law centering, schedule-specific batch sizes, and separate model and return failure shares. This is fixed-prefix control of batch-average realized behavior regret. It is not arbitrary-delta model control, a one-raw-episode online process, uniform-time/anytime control, minimax/optimal-rate regret, or a complete UCB-VI theorem.

Module map

Declarations
43
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonNaturalCausalBehaviorExpectedRegretHighProbabilityLogRate, BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalRealizedSuccessorRegret

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeHighProbabilityAverageRealizedBehaviorRegret, BanditRLProof.RL.FiniteHorizonNaturalCausalRealizedBehaviorRegretHighProbabilityBurninLogRate

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorAverageReturnDeviationIncrement Compiled

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
Source line 54 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorAverageReturnVarianceProxyAt Compiled

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
Source line 68 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeSuccessorAverageReturnVarianceProxy Compiled

Total proxy for normalized successor sample-average deviations.

noncomputable def naturalCumulativeSuccessorAverageReturnVarianceProxy (mdp : MDP State Action) (episodes : Nat -> Nat) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) : NNReal
Source line 79 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeSuccessorAverageReturnDeviation Compiled

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
Source line 87 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorAverageReturnDeviationIncrement_stronglyAdapted_piLE Compiled

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
Source line 101 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_naturalCumulativeSuccessorAverageReturnDeviation Compiled

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)
Source line 129 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorAverageReturnDeviationIncrement_succ_hasCondSubgaussianMGF Compiled

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
Source line 146 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeSuccessorAverageReturnVarianceProxy_pos Compiled

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)
Source line 185 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.trajectoryMeasure_naturalCumulativeSuccessorAverageReturnDeviation_abs_tail_le Compiled

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
Source line 227 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeSuccessorAverageReturnDeviation_eq_sum_range Compiled

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
Source line 295 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorBatchAverageRealizedRegret Compiled

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
Source line 311 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeRealizedBehaviorRegret Compiled

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
Source line 324 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalAverageRealizedBehaviorRegret Compiled

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
Source line 335 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_naturalSuccessorBatchAverageRealizedRegret Compiled

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)
Source line 349 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_naturalCumulativeRealizedBehaviorRegret Compiled

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)
Source line 365 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.measurable_naturalAverageRealizedBehaviorRegret Compiled

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)
Source line 380 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalSuccessorBatchAverageRealizedRegret_eq_expected_sub_deviation Compiled

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
Source line 395 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.HeterogeneousAdaptiveStochasticEpisodeBatchSource.naturalCumulativeRealizedBehaviorRegret_eq_expected_sub_deviation Compiled

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
Source line 421 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy Compiled

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

noncomputable def selfConsistentScheduledNaturalCausalCumulativeReturnVarianceProxy (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : NNReal
Source line 459 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess Compiled

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
Source line 470 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess Compiled

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
Source line 486 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess Compiled

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
Source line 503 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeReturnBadEvent Compiled

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))
Source line 519 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalCumulativeReturnDeviationProcess Compiled

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)
Source line 539 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess Compiled

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)
Source line 560 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurable_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess Compiled

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)
Source line 577 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalCumulativeReturnBadEvent Compiled

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)
Source line 594 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_eq_expected_sub_deviation Compiled

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
Source line 612 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_eq_expected_sub_deviation Compiled

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)
Source line 650 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_naturalCumulativeReturnBadEvent_le Compiled

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
Source line 679 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRealizedCumulativeLogarithmicRate Compiled

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
Source line 728 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalRealizedAverageLogarithmicRate Compiled

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
Source line 738 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalModelReturnBadEvent Compiled

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))
Source line 745 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet Compiled

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))
Source line 763 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet Compiled

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))
Source line 782 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet Compiled

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)
Source line 801 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.measurableSet_selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet Compiled

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)
Source line 819 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_trajectoryMeasure_naturalModelReturnBadEvent_le Compiled

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
Source line 837 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretProcess_le_logarithmic_of_not_mem_modelReturnBadEvent Compiled

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
Source line 900 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess_le_logarithmic_of_not_mem_modelReturnBadEvent Compiled

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
Source line 991 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalCumulativeRealizedBehaviorRegretLogarithmicViolationSet_subset_modelReturnBadEvent Compiled

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
Source line 1032 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretLogarithmicViolationSet_subset_modelReturnBadEvent Compiled

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
Source line 1063 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.AdaptiveStochasticSampledEmpiricalOptimisticSource.selfConsistentScheduledCausalSource_fixedPrefixHighProbabilityLogarithmicCumulativeAverageRealizedBehaviorRegret Compiled

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
Source line 1100 Chapter context: Finite-horizon RL