BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEpisodewiseCommonSpaceExpectedConsistency

A deterministic finite trajectory has return bounded by the horizon.

theorem abs_cumulativeReward_le_horizon (mdp : MDP State Action) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (trajectory : Prod State (StepTrace Action State mdp.horizon)) : |mdp.cumulativeReward trajectory| <= (mdp.horizon : Real)

The optimal initial expected return inherits the deterministic horizon envelope.

theorem abs_optimalInitialExpectedReturn_le_horizon (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (hrewardBound : forall state action, |mdp.reward state action| <= 1) : |optimalInitialExpectedReturn mdp initialState| <= (mdp.horizon : Real)

Every adaptive successor batch is reward-consistent almost everywhere.

theorem trajectoryMeasure_successor_rewardConsistent_ae {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) : ∀ᵐ trajectory ∂source.trajectoryMeasure, (trajectory (n + 1)).RewardConsistent

Reward-consistent successor batches give a uniform realized-average envelope.

theorem abs_realizedSuccessorAverageRegret_le_two_mul_horizon {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (trajectory : EpisodeBatchTrajectory mdp episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hconsistent : forall round : Fin rounds, (trajectory ((round : Nat) + 1)).RewardConsistent) : |source.realizedSuccessorAverageRegret trajectory rounds| <= 2 * (mdp.horizon : Real)

The adaptive realized average has the `2H` envelope almost everywhere.

theorem trajectoryMeasure_abs_realizedSuccessorAverageRegret_le_two_mul_horizon_ae {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ∀ᵐ trajectory ∂source.trajectoryMeasure, |source.realizedSuccessorAverageRegret trajectory rounds| <= 2 * (mdp.horizon : Real)

The adaptive realized successor-average regret is integrable.

theorem integrable_realizedSuccessorAverageRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : Integrable (fun trajectory => source.realizedSuccessorAverageRegret trajectory rounds) source.trajectoryMeasure

The common-space regret process has the deterministic `2H` envelope a.e.

theorem decayingExplorationEpisodewiseCommonMeasure_abs_realizedBehaviorRegretProcess_le_two_mul_horizon_ae (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : ∀ᵐ omega ∂decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor, |decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n omega| <= 2 * (mdp.horizon : Real)

Every common-space regret coordinate is integrable.

theorem integrable_decayingExplorationEpisodewiseRealizedBehaviorRegretProcess (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (n : Nat) : Integrable (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)

The pulled-back sharp finite-window bad event is measurable on the common space.

theorem measurableSet_decayingExplorationEpisodewiseCommonBadEvent (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : MeasurableSet (decayingExplorationEpisodewiseCommonBadEvent mdp initialState initialTable defaultState baseVisitFloor n)

Expected absolute scheduled realized-behavior regret on the common space.

noncomputable def decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Real

The deterministic good-event radius plus the uniform bad-event contribution.

noncomputable def decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound (mdp : MDP State Action) (baseVisitFloor : Real) (n : Nat) : Real

Expected absolute realized-behavior regret is nonnegative.

theorem decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret_nonneg (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : 0 <= decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor n

The explicit expected-absolute bound is nonnegative.

theorem decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound_nonneg (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : 0 <= decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor n

The common-space expected absolute regret is controlled by the sharp good-event radius plus the uniform `2H` envelope times the failure probability.

theorem decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret_le_bound (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) (n : Nat) : decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor n <= decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor n

The real-valued failure budget tends to zero.

theorem decayingExplorationRealizedFailureBudget_toReal_tendsto_zero : Tendsto (fun n => (AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n).toReal) atTop (nhds 0)

The explicit expected-absolute envelope tends to zero.

theorem decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor) atTop (nhds 0)

Terminal expected-consistency theorem: all coordinates are integrable, every finite expected absolute regret obeys the explicit bound, and those expectations converge to zero.

theorem exploratorySource_decayingExplorationEpisodewiseCommonMeasure_integrable_expectedAbsoluteRealizedBehaviorRegret_tendsto_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (hbatchBorel : forall n, StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (htrajectoryBorel : forall n, StandardBorelSpace (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (support : ExploratoryPathSupport mdp initialState) (hbaseFloor : ExploratoryPathUniformVisitFloor support 1 baseVisitFloor) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (hhorizon : 0 < mdp.horizon) (hbaseVisitFloor : 0 < baseVisitFloor) : (forall n, Integrable (decayingExplorationEpisodewiseRealizedBehaviorRegretProcess mdp initialState initialTable defaultState baseVisitFloor n) (decayingExplorationEpisodewiseCommonMeasure mdp initialState initialTable defaultState baseVisitFloor)) /\ (forall n, decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor n <= decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegretBound mdp baseVisitFloor n) /\ Tendsto (decayingExplorationEpisodewiseExpectedAbsoluteRealizedBehaviorRegret mdp initialState initialTable defaultState baseVisitFloor) atTop (nhds 0)