BanditRLProof.RL.FiniteHorizonAdaptiveStochasticRewardSampledEmpiricalOptimisticSelfConsistentCausalRealizedSuccessorRegret

The selected policy that generates successor coordinate `n + 1`.

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

Total number of complete episodes in successor coordinates `1..rounds`.

noncomputable def successorEpisodeMass (episodes : Nat -> Nat) (rounds : Nat) : Real

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

theorem successorEpisodeMass_pos (episodes : Nat -> Nat) (rounds : Nat) (hrounds : 0 < rounds) (hepisodes : forall t, 0 < episodes t) : 0 < successorEpisodeMass episodes rounds

Batch-size-weighted expected regret of the selected successor policies.

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

Weighted successor expected regret per sampled successor episode.

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

Realized regret of every sampled successor batch, with its actual size.

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

Realized successor regret per actual sampled successor episode.

noncomputable def realizedSuccessorAverageRegret {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 increment is actual return minus its selected policy mean.

theorem successorGlobalReturnIncrement_succ_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) : source.successorGlobalReturnIncrement (n + 1) trajectory = mdp.sampledCumulativeRewardSum (episodes (n + 1)) (trajectory (n + 1)) - (episodes (n + 1) : Real) * integral initialState ((source.successorPolicyAt trajectory n).valueAt 0 (Nat.zero_le mdp.horizon))

The global deviation is exactly the finite sum of successor increments.

theorem cumulativeSuccessorGlobalReturnDeviation_eq_fin_sum {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (rounds : Nat) : source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory = ∑ round : Fin rounds, source.successorGlobalReturnIncrement ((round : Nat) + 1) trajectory

Exact weighted realized-equals-expected-minus-deviation identity.

theorem realizedSuccessorCumulativeRegret_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) : source.realizedSuccessorCumulativeRegret trajectory rounds = source.successorWeightedExpectedCumulativeRegret trajectory rounds - source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory

Exact weighted average form of the realized-regret decomposition.

theorem realizedSuccessorAverageRegret_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) (hmass : 0 < successorEpisodeMass episodes rounds) : source.realizedSuccessorAverageRegret trajectory rounds = source.successorWeightedExpectedAverageRegret trajectory rounds - source.cumulativeSuccessorGlobalReturnDeviation rounds trajectory / successorEpisodeMass episodes rounds

Named successor-only global-return event for heterogeneous batches.

noncomputable def successorGlobalReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)

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

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

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

theorem measurableSet_successorGlobalReturnDeviationBadEvent {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (source : HeterogeneousAdaptiveStochasticEpisodeBatchSource mdp initialState episodes) [source.GlobalReturnMeasurability] (rounds : Nat) (rewardBound rewardVarianceProxy : NNReal) (delta : Real) : MeasurableSet (source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy delta)

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

theorem trajectoryMeasure_successorGlobalReturnDeviationBadEvent_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 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : source.trajectoryMeasure (source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy delta) <= ENNReal.ofReal delta

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

theorem trajectoryMeasure_weightedExpected_to_realized_successor_average_regret_transport {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) (hrounds : 0 < rounds) (hepisodes : forall t, 0 < episodes t) (rewardBound rewardVarianceProxy : NNReal) (hrewardBound : forall state action, |mdp.reward state action| <= (rewardBound : Real)) (law : source.rewardSource.UniformSubgaussianRewardLaw rewardVarianceProxy) (htotal : 0 < ((cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy : NNReal) : Real)) (returnDelta : Real) (hreturnDelta : 0 < returnDelta) (hreturnDelta_le_one : returnDelta <= 1) (modelBadEvent : Set (HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes)) (modelFailureBudget : ENNReal) (expectedBound : Real) (Good : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes -> Prop) (hmodelMeasurable : MeasurableSet modelBadEvent) (hmodelTail : source.trajectoryMeasure modelBadEvent <= modelFailureBudget) (hmodelGood : forall trajectory, trajectory ∉ modelBadEvent -> Good trajectory /\ source.successorWeightedExpectedAverageRegret trajectory rounds <= expectedBound) : let returnBadEvent := source.successorGlobalReturnDeviationBadEvent rounds rewardBound rewardVarianceProxy returnDelta let combinedBadEvent := modelBadEvent ∪ returnBadEvent MeasurableSet combinedBadEvent /\ source.trajectoryMeasure combinedBadEvent <= modelFailureBudget + ENNReal.ofReal returnDelta /\ forall trajectory, trajectory ∉ combinedBadEvent -> Good trajectory /\ source.realizedSuccessorAverageRegret trajectory rounds <= expectedBound + Concentration.subGaussianSumConfidenceRadius (cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds rewardBound rewardVarianceProxy) returnDelta / successorEpisodeMass episodes rounds

A sampled stochastic empirical model has the two supplied fixed radii.

theorem MDP.stochasticAllCoordinateEmpiricalFiniteBatchModel_occupancySelectedRadiusRemaining_eq {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (batch : EpisodeBatch mdp episodes) (defaultState : State) (rewardBudget transitionBudget : Real) : let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel episodes batch defaultState rewardBudget transitionBudget model.plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * model.plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState = (mdp.horizon : Real) * (2 * (rewardBudget + transitionBudget))

The sampled table at coordinate `n` is exactly the next source policy.

theorem heterogeneousExploratorySource_successorPolicyAt_eq_sampledPlanExploratoryPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (explorationRate : Nat -> NNReal) (hexplorationRate : forall t, explorationRate t <= 1) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) : let source := heterogeneousExploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate source.successorPolicyAt trajectory n = ((trajectory n).sampledEmpiricalOptimisticPolicyTable defaultState (rewardBudget n) (transitionBudget n)).exploratoryPolicy (explorationRate (n + 1)) (hexplorationRate (n + 1))

One selected causal exploratory policy pays only its local charge.

theorem heterogeneousExploratorySource_successorPolicyAt_expectedRegret_le {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat -> Nat} (rewardSource : mdp.MeanCompatibleRewardKernel) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (rewardBudget transitionBudget : Nat -> Real) (explorationRate : Nat -> NNReal) (hexplorationRate : forall t, explorationRate t <= 1) (trajectory : HeterogeneousStochasticEpisodeBatchTrajectory mdp episodes) (n : Nat) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) : let source := heterogeneousExploratorySource mdp initialState episodes rewardSource initialTable defaultState rewardBudget transitionBudget explorationRate hexplorationRate let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes n) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes n) (trajectory n)) defaultState (rewardBudget n) (transitionBudget n) (source.successorPolicyAt trajectory n).expectedRegret initialState <= model.plan.optimisticPolicy.expectedRegret initialState + exploratoryBehaviorRegretCharge mdp (explorationRate (n + 1)) rewardBound

Weighted planning envelope for all causal successor batches.

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

The same planning envelope per actual sampled successor episode.

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

The same planning envelope per actual sampled successor episode. -/ noncomputable def selfConsistentScheduledCausalSuccessorPlanningAverageBound (mdp : MDP State Action) (varianceProxy : NNReal) (baseVisitFloor : Real) (rounds : Nat) : Real := selfConsistentScheduledCausalSuccessorPlanningCumulativeBound mdp varianceProxy baseVisitFloor rounds / HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorEpisodeMass (fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t) rounds /- The sampled-model event controls the actual exploratory successor policies. Every coordinate keeps its own model budgets, next-coordinate exploration rate, and successor batch-size weight.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_optimism_and_weightedExpectedSuccessorAverageRegret (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) : let episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds MeasurableSet event /\ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelFailureBudget mdp rounds /\ forall trajectory, trajectory ∉ event -> (forall round : Fin rounds, let t := (round : Nat) let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ source.successorWeightedExpectedAverageRegret trajectory rounds <= selfConsistentScheduledCausalSuccessorPlanningAverageBound mdp varianceProxy baseVisitFloor rounds

Named successor-only return event for the self-consistent causal source.

noncomputable def selfConsistentScheduledCausalSuccessorReturnBadEvent (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))

Union of the causal sampled-model and globally centered return events.

noncomputable def selfConsistentScheduledCausalModelReturnBadEvent (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))

Exact finite-prefix model-plus-return failure budget.

noncomputable def selfConsistentScheduledCausalModelReturnFailureBudget (mdp : MDP State Action) (rounds : Nat) (returnDelta : Real) : ENNReal

Exact finite-prefix model-plus-return failure budget. -/ noncomputable def selfConsistentScheduledCausalModelReturnFailureBudget (mdp : MDP State Action) (rounds : Nat) (returnDelta : Real) : ENNReal := selfConsistentScheduledCausalModelFailureBudget mdp rounds + ENNReal.ofReal returnDelta /- End-to-end causal finite-prefix theorem. Off one named event, every actual sampled model is optimistic and the weighted realized successor-average behavior regret is controlled by the coordinatewise schedule plus the heterogeneous globally centered return radius.

theorem selfConsistentScheduledCausalSource_trajectoryMeasure_optimism_and_realizedSuccessorAverageRegret (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 episodes := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledEpisodes mdp varianceProxy baseVisitFloor t let rewardBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledRewardBudget mdp varianceProxy baseVisitFloor t let transitionBudget := fun t => AdaptiveStochasticEpisodeBatchSource.selfConsistentScheduledTransitionBudget mdp varianceProxy baseVisitFloor t let source := selfConsistentScheduledCausalSource mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor let event := selfConsistentScheduledCausalModelReturnBadEvent mdp initialState rewardSource initialTable defaultState varianceProxy baseVisitFloor rounds returnDelta MeasurableSet event /\ source.trajectoryMeasure event <= selfConsistentScheduledCausalModelReturnFailureBudget mdp rounds returnDelta /\ forall trajectory, trajectory ∉ event -> (forall round : Fin rounds, let t := (round : Nat) let model := mdp.stochasticAllCoordinateEmpiricalFiniteBatchModel (episodes t) (mdp.sampledEpisodeBatchOfStochasticTrajectories (episodes t) (trajectory t)) defaultState (rewardBudget t) (transitionBudget t) forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= model.plan.upperValueRemaining mdp.horizon le_rfl state) /\ source.realizedSuccessorAverageRegret trajectory rounds <= selfConsistentScheduledCausalSuccessorPlanningAverageBound mdp varianceProxy baseVisitFloor rounds + Concentration.subGaussianSumConfidenceRadius (HeterogeneousAdaptiveStochasticEpisodeBatchSource.cumulativeSuccessorGlobalReturnVarianceProxy mdp episodes rounds 1 varianceProxy) returnDelta / HeterogeneousAdaptiveStochasticEpisodeBatchSource.successorEpisodeMass episodes rounds