BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEpisodewiseRealizedBehaviorConsistency

A complete episode row is a measurable coordinate of a finite batch.

theorem measurable_episode {mdp : MDP State Action} {episodes : Nat} (episode : Fin episodes) : Measurable (fun batch : EpisodeBatch mdp episodes => batch episode)

Complete generated episode rows are independent product coordinates.

theorem iIndepFun_episodeRowOfTrajectory {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.iIndepFun (fun episode trajectories => fun stage => mdp.episodeStepOfTrajectory (trajectories episode) stage) (policy.iidTrajectoryFamilyMeasure initialState episodes)

Complete episode rows remain independent after mapping trajectories to a batch.

theorem iIndepFun_iidEpisodeBatch_episode {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.iIndepFun (fun episode (batch : EpisodeBatch mdp episodes) => batch episode) (policy.iidEpisodeBatchMeasure initialState episodes)

Full episode returns are independent across iid batch coordinates.

theorem iIndepFun_iidEpisodeBatch_episodeReturn {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) : ProbabilityTheory.iIndepFun (fun episode (batch : EpisodeBatch mdp episodes) => EpisodeBatch.episodeReturn batch episode) (policy.iidEpisodeBatchMeasure initialState episodes)

Every episode return in an iid batch has the common trajectory-return mean.

theorem integral_episodeReturn_iidEpisodeBatchMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) : integral (policy.iidEpisodeBatchMeasure initialState episodes) (fun batch => EpisodeBatch.episodeReturn batch episode) = integral (policy.trajectoryMeasure initialState) mdp.cumulativeReward

One full episode's bounded-return Hoeffding proxy.

noncomputable def episodeReturnVarianceProxy (mdp : MDP State Action) : NNReal

Each bounded centered episode return is sub-Gaussian with proxy `horizon^2`.

theorem episodeReturn_centered_hasSubgaussianMGF {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] {episodes : Nat} (episode : Fin episodes) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ProbabilityTheory.HasSubgaussianMGF (fun batch : EpisodeBatch mdp episodes => EpisodeBatch.episodeReturn batch episode - integral (policy.trajectoryMeasure initialState) mdp.cumulativeReward) (episodeReturnVarianceProxy mdp) (policy.iidEpisodeBatchMeasure initialState episodes)

Sum of the independent full-episode return proxies in one batch.

noncomputable def episodewiseBatchReturnVarianceProxy (mdp : MDP State Action) (episodes : Nat) : NNReal

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

theorem episodeReturnVarianceProxy_coe (mdp : MDP State Action) : ((episodeReturnVarianceProxy mdp : NNReal) : Real) = ((mdp.horizon : Nat) : Real) ^ 2

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

theorem episodewiseBatchReturnVarianceProxy_coe (mdp : MDP State Action) (episodes : Nat) : ((episodewiseBatchReturnVarianceProxy mdp episodes : NNReal) : Real) = (episodes : Real) * ((mdp.horizon : Nat) : Real) ^ 2

The centered total batch return has the sharp episodewise proxy.

theorem totalReturn_centered_episodewise_hasSubgaussianMGF {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ProbabilityTheory.HasSubgaussianMGF (fun batch : EpisodeBatch mdp episodes => EpisodeBatch.totalReturn batch - integral (policy.iidEpisodeBatchMeasure initialState episodes) EpisodeBatch.totalReturn) (episodewiseBatchReturnVarianceProxy mdp episodes) (policy.iidEpisodeBatchMeasure initialState episodes)

The successor batch increment inherits the sharp episodewise batch proxy.

theorem successorReturnIncrement_succ_episodewise_hasCondSubgaussianMGF {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (n : Nat) (hrewardBound : forall state action, |mdp.reward state action| <= 1) : ProbabilityTheory.HasCondSubgaussianMGF (Filtration.piLE (X := fun _ : Nat => EpisodeBatch mdp episodes) n) ((Filtration.piLE (X := fun _ : Nat => EpisodeBatch mdp episodes)).le n) (source.successorReturnIncrement (n + 1)) (MarkovPolicy.episodewiseBatchReturnVarianceProxy mdp episodes) source.trajectoryMeasure

Sum of the sharp batch proxies over the successor rounds.

noncomputable def episodewiseCumulativeSuccessorReturnVarianceProxy (mdp : MDP State Action) (episodes rounds : Nat) : NNReal

The sharp cumulative proxy is `rounds * episodes * horizon^2`.

theorem episodewiseCumulativeSuccessorReturnVarianceProxy_coe (mdp : MDP State Action) (episodes rounds : Nat) : ((episodewiseCumulativeSuccessorReturnVarianceProxy mdp episodes rounds : NNReal) : Real) = (rounds : Real) * (episodes : Real) * (mdp.horizon : Real) ^ 2

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

theorem episodewiseBatchReturnVarianceProxy_pos (mdp : MDP State Action) (episodes : Nat) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) : 0 < MarkovPolicy.episodewiseBatchReturnVarianceProxy mdp episodes

Two-sided adaptive return tail with the sharp episodewise proxy.

theorem trajectoryMeasure_episodewiseCumulativeSuccessorReturnDeviation_abs_tail_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure {trajectory | Concentration.subGaussianSumConfidenceRadius (episodewiseCumulativeSuccessorReturnVarianceProxy mdp episodes rounds) delta <= |source.cumulativeSuccessorReturnDeviation rounds trajectory|} <= ENNReal.ofReal delta

Sharp successor-return deviation event.

noncomputable def episodewiseSuccessorReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : Set (EpisodeBatchTrajectory mdp episodes)

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

theorem measurableSet_episodewiseSuccessorReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (delta : Real) : MeasurableSet (source.episodewiseSuccessorReturnDeviationBadEvent rounds delta)

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

theorem trajectoryMeasure_episodewiseSuccessorReturnDeviationBadEvent_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure (source.episodewiseSuccessorReturnDeviationBadEvent rounds delta) <= ENNReal.ofReal delta

Transport an expected-regret certificate through the sharp return event.

theorem trajectoryMeasure_expected_to_realized_successor_average_regret_episodewise_transport {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} [StandardBorelSpace (EpisodeBatch mdp episodes)] [StandardBorelSpace (EpisodeBatchTrajectory mdp episodes)] (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : 0 < episodes) (hhorizon : 0 < mdp.horizon) (hrewardBound : forall state action, |mdp.reward state action| <= 1) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) (countBadEvent : Set (EpisodeBatchTrajectory mdp episodes)) (expectedBound : Real) (Good : EpisodeBatchTrajectory mdp episodes -> Prop) (hcountMeasurable : MeasurableSet countBadEvent) (hcountTail : source.trajectoryMeasure countBadEvent <= ENNReal.ofReal delta) (hcountGood : forall trajectory, trajectory ∉ countBadEvent -> Good trajectory /\ source.successorExpectedAverageRegret trajectory rounds <= expectedBound) : let returnBadEvent := source.episodewiseSuccessorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= ENNReal.ofReal delta + ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ combinedBadEvent -> Good trajectory /\ source.realizedSuccessorAverageRegret trajectory rounds <= expectedBound + Concentration.subGaussianSumConfidenceRadius (episodewiseCumulativeSuccessorReturnVarianceProxy mdp episodes rounds) delta / ((episodes : Real) * (rounds : Real))

Sharp return-deviation radius after normalization by all sampled episodes.

noncomputable def episodewiseNormalizedSuccessorReturnConfidenceRadius (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) : Real

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

theorem episodewiseNormalizedSuccessorReturnConfidenceRadius_nonneg (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) : 0 <= episodewiseNormalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta

Exact normalized radius: episode count now improves concentration.

theorem episodewiseNormalizedSuccessorReturnConfidenceRadius_eq (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) (hepisodes : 0 < episodes) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : episodewiseNormalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta = (mdp.horizon : Real) * Real.sqrt (2 * Real.log (2 / delta) / ((episodes : Real) * (rounds : Real)))

The sharp radius is no larger than the compiled whole-batch radius.

theorem episodewiseNormalizedSuccessorReturnConfidenceRadius_le_normalized (mdp : MDP State Action) (episodes rounds : Nat) (delta : Real) (hepisodes : 0 < episodes) (hrounds : 0 < rounds) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : episodewiseNormalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta <= normalizedSuccessorReturnConfidenceRadius mdp episodes rounds delta

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

theorem episodewiseNormalizedSuccessorReturnConfidenceRadius_le_decayingEnvelope (mdp : MDP State Action) (episodes : Nat) (n : Nat) (hepisodes : 0 < episodes) : episodewiseNormalizedSuccessorReturnConfidenceRadius mdp episodes (decayingExplorationRounds mdp n) (vanishingAverageConfidenceDelta n) <= decayingExplorationReturnRadiusEnvelope mdp n

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

theorem decayingExplorationEpisodewiseNormalizedReturnRadius_tendsto_zero (mdp : MDP State Action) (baseVisitFloor : Real) : Tendsto (fun n => episodewiseNormalizedSuccessorReturnConfidenceRadius mdp (decayingExplorationScheduledEpisodes mdp baseVisitFloor n) (decayingExplorationRounds mdp n) (vanishingAverageConfidenceDelta n)) atTop (nhds 0)

Expected behavior bound plus the sharp episodewise return radius.

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

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

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

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

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

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

theorem decayingExplorationEpisodewiseRealizedFailureAndRegretBound_tendsto_zero (mdp : MDP State Action) (hhorizon : 0 < mdp.horizon) (baseVisitFloor : Real) (hbaseVisitFloor : 0 < baseVisitFloor) : Tendsto (fun n => (decayingExplorationRealizedFailureBudget n, decayingExplorationEpisodewiseAverageRealizedBehaviorRegretBound mdp baseVisitFloor n)) atTop (nhds (0, 0))

Realized-regret violation set for the sharp episodewise return certificate.

noncomputable def decayingExplorationEpisodewiseAverageRealizedBehaviorRegretViolationSet (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (baseVisitFloor : Real) (n : Nat) : Set (EpisodeBatchTrajectory mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))

One scheduled finite window with episodewise return concentration. The realized violation set is covered by the measurable count/return union while the good side retains optimism and the sharp normalized return radius.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_optimism_and_decayingExplorationEpisodewiseAverageRealizedBehaviorConsistency (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (baseVisitFloor : Real) (n : Nat) [StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor 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) : let rounds := AdaptiveEpisodeBatchSource.decayingExplorationRounds mdp n let delta := AdaptiveEpisodeBatchSource.vanishingAverageConfidenceDelta n let explorationRate := AdaptiveEpisodeBatchSource.decayingExplorationRate n let visitFloor := AdaptiveEpisodeBatchSource.decayingExplorationVisitFloor mdp baseVisitFloor n let episodes := AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n let countRadius := AdaptiveEpisodeBatchSource.normalizedCumulativeInverseSqrtCountRadius mdp rounds delta visitFloor let source := exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate (AdaptiveEpisodeBatchSource.decayingExplorationRate_le_one n) let countBadEvent := source.adaptiveCumulativeCountBadEvent rounds delta let returnBadEvent := source.episodewiseSuccessorReturnDeviationBadEvent rounds delta let combinedBadEvent := countBadEvent ∪ returnBadEvent let violationSet := decayingExplorationEpisodewiseAverageRealizedBehaviorRegretViolationSet mdp initialState initialTable defaultState baseVisitFloor n MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n /\ violationSet ⊆ combinedBadEvent /\ source.trajectoryMeasure violationSet <= AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n /\ forall trajectory, trajectory ∉ combinedBadEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= AdaptiveEpisodeBatchSource.decayingExplorationEpisodewiseAverageRealizedBehaviorRegretBound mdp baseVisitFloor n

All scheduled finite windows with their indexed Borel witnesses, together with the joint scalar limit. The sample spaces may vary with the schedule index.

theorem exploratorySource_trajectoryMeasure_cumulativeInverseSqrtPathSupport_decayingExplorationEpisodewiseAverageRealizedBehaviorConsistency_allWindows (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) : Tendsto (fun n => (AdaptiveEpisodeBatchSource.decayingExplorationRealizedFailureBudget n, AdaptiveEpisodeBatchSource.decayingExplorationEpisodewiseAverageRealizedBehaviorRegretBound mdp baseVisitFloor n)) atTop (nhds (0, 0)) /\ forall n, letI : StandardBorelSpace (EpisodeBatch mdp (AdaptiveEpisodeBatchSource.decayingExplorationScheduledEpisodes mdp baseVisitFloor n))