BanditRLProof.RL.FiniteHorizonNaturalCausalAverageRealizedBehaviorRegretAlmostSureConsistency

Pathwise equal-round average of successor-policy expected regret.

noncomputable def selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegretProcess (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

Cumulative normalized successor-return deviation divided by round count.

noncomputable def selfConsistentScheduledNaturalCausalAverageReturnDeviationProcess (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

Summable confidence share for the return event at prefix `n + 1`.

noncomputable def naturalAllPrefixReturnDelta (n : Nat) : Real

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

theorem naturalAllPrefixReturnDelta_pos (n : Nat) : 0 < naturalAllPrefixReturnDelta n

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

theorem naturalAllPrefixReturnDelta_le_one (n : Nat) : naturalAllPrefixReturnDelta n <= 1

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

theorem summable_naturalAllPrefixReturnDelta : Summable naturalAllPrefixReturnDelta

Fixed-prefix return radius after division by the positive prefix length.

noncomputable def naturalAllPrefixAverageReturnConfidenceRadius (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : Real

Deterministic square-root envelope for the normalized all-prefix radius.

noncomputable def naturalAllPrefixAverageReturnConfidenceEnvelope (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : Real

The inverse-square confidence share contributes at most three shifted logs.

theorem log_two_div_naturalAllPrefixReturnDelta_le (n : Nat) : Real.log (2 / naturalAllPrefixReturnDelta n) <= 3 * (1 + Real.log ((n + 2 : Nat) : Real))

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

theorem naturalAllPrefixAverageReturnConfidenceEnvelope_nonneg (mdp : MDP State Action) (varianceProxy : NNReal) (n : Nat) : 0 <= naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy n

The normalized fixed-prefix return radius is below its deterministic envelope.

theorem naturalAllPrefixAverageReturnConfidenceRadius_le_envelope (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (n : Nat) : naturalAllPrefixAverageReturnConfidenceRadius mdp varianceProxy baseVisitFloor n <= naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy n

The deterministic all-prefix return-radius envelope vanishes.

theorem naturalAllPrefixAverageReturnConfidenceEnvelope_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) : Tendsto (naturalAllPrefixAverageReturnConfidenceEnvelope mdp varianceProxy) atTop (nhds 0)

The normalized all-prefix return confidence radius vanishes.

theorem naturalAllPrefixAverageReturnConfidenceRadius_tendsto_zero (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) : Tendsto (naturalAllPrefixAverageReturnConfidenceRadius mdp varianceProxy baseVisitFloor) atTop (nhds 0)

Return bad event at positive prefix `n + 1` and inverse-square share.

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

The all-prefix shifted return event is measurable.

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

Each shifted return event has probability at most its inverse-square share.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_naturalAllPrefixReturnBadEvent_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) (n : Nat) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor source.trajectoryMeasure (naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n) <= ENNReal.ofReal (naturalAllPrefixReturnDelta n)

The shifted return-event probabilities have finite total mass.

theorem tsum_naturalAllPrefixReturnBadEvent_measure_ne_top (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (∑' n, source.trajectoryMeasure (naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n)) ≠ ∞

Almost every trajectory eventually avoids all shifted return bad events.

theorem ae_eventually_not_mem_naturalAllPrefixReturnBadEvent (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, ∀ᶠ n in atTop, trajectory ∉ naturalAllPrefixReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor n

The pathwise behavior expected-regret Cesaro average tends to zero a.e.

theorem selfConsistentScheduledCausalSource_naturalAverageBehaviorExpectedRegret_tendstoAlmostEverywhere_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageBehaviorExpectedRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)

The equal-round normalized return deviation vanishes on almost every trajectory.

theorem selfConsistentScheduledCausalSource_naturalAverageReturnDeviation_tendstoAlmostEverywhere_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageReturnDeviationProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)

All-prefix natural average realized behavior regret converges almost surely.

theorem selfConsistentScheduledCausalSource_naturalAverageRealizedBehaviorRegret_tendstoAlmostEverywhere_zero (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) : let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor (forall rounds, Measurable (selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds)) ∧ ∀ᵐ trajectory ∂source.trajectoryMeasure, Tendsto (fun rounds => selfConsistentScheduledNaturalCausalAverageRealizedBehaviorRegretProcess mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds trajectory) atTop (nhds 0)