BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeEmpiricalOptimisticRegret

A nonnegative transition radius that can only decrease as visits accumulate.

structure TransitionCountRadius where

A finite linear-decay radius, useful as an executable shrinking-radius canary.

def linearDecay (budget : Nat) : TransitionCountRadius where

Sum all transition-count coordinates in a nonempty finite batch prefix.

def cumulativeTransitionCountSummary {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) : TransitionCountSummary mdp

The complete cumulative transition-count summary is history measurable.

theorem measurable_cumulativeTransitionCountSummary {mdp : MDP State Action} {episodes n : Nat} : Measurable (cumulativeTransitionCountSummary : EpisodeBatchPrefix mdp episodes n -> TransitionCountSummary mdp)

Cumulative next-state counts still partition the cumulative visit count.

theorem cumulativeTransitionCountSummary_visitCount {mdp : MDP State Action} {episodes n : Nat} (history : EpisodeBatchPrefix mdp episodes n) (stage : Fin mdp.horizon) (state : State) (action : Action) : history.cumulativeTransitionCountSummary.visitCount stage state action = ∑ i : Fin (n + 1), (history ⟨i, Finset.mem_Iic.mpr (Nat.le_of_lt_succ i.isLt)⟩).visitCount stage state action

Cumulative count summary through trajectory coordinate `round`.

def cumulativeTransitionCountSummaryAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) : TransitionCountSummary mdp

Extending the trajectory prefix adds exactly the new batch coordinate.

theorem cumulativeTransitionCountSummaryAt_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : cumulativeTransitionCountSummaryAt trajectory (round + 1) stage state action nextState = cumulativeTransitionCountSummaryAt trajectory round stage state action nextState + (trajectory (round + 1)).transitionCount stage state action nextState

Every cumulative state-action visit count is monotone across rounds.

theorem cumulativeTransitionCountSummaryAt_visitCount_le_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : (cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action <= (cumulativeTransitionCountSummaryAt trajectory (round + 1)).visitCount stage state action

Count-antitone radii shrink along every accumulated state-action row.

theorem TransitionCountRadius.radius_cumulativeVisitCount_succ_le {mdp : MDP State Action} {episodes : Nat} (countRadius : TransitionCountRadius) (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (stage : Fin mdp.horizon) (state : State) (action : Action) : countRadius.radius ((cumulativeTransitionCountSummaryAt trajectory (round + 1)).visitCount stage state action) <= countRadius.radius ((cumulativeTransitionCountSummaryAt trajectory round).visitCount stage state action)

Known-reward empirical plan with a radius selected from cumulative visits.

noncomputable def countRadiusOptimisticPlan (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (countRadius : TransitionCountRadius) : mdp.EstimatedModelPlan where

Every count-radius optimistic value is controlled by the radius at zero visits.

theorem countRadiusOptimisticPlan_upperValueRemaining_abs_le (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (countRadius : TransitionCountRadius) (rewardBound : Real) (hrewardBound : forall state action, |mdp.reward state action| <= rewardBound) : forall (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State), |(summary.countRadiusOptimisticPlan mdp defaultState countRadius).upperValueRemaining remaining hremaining state| <= empiricalFiniteBatchValueEnvelope rewardBound (countRadius.radius 0) remaining

The cumulative count-radius plan selects exactly its chosen row radius.

theorem countRadiusOptimisticPlan_selectedRadiusRemaining (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (countRadius : TransitionCountRadius) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (summary.countRadiusOptimisticPlan mdp defaultState countRadius).selectedRadiusRemaining remaining hremaining state = countRadius.radius (summary.visitCount (mdp.decisionStageRemaining remaining hremaining) state ((summary.countRadiusOptimisticPlan mdp defaultState countRadius).optimisticAction (mdp.decisionStageRemaining remaining hremaining) ((summary.countRadiusOptimisticPlan mdp defaultState countRadius).upperValueRemaining remaining (by omega)) state))

Deterministic optimistic table selected from a cumulative count summary.

noncomputable def countRadiusOptimisticPolicyTable (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (countRadius : TransitionCountRadius) : DeterministicMarkovPolicyTable mdp

The table interpretation is the cumulative count-radius plan's policy.

theorem countRadiusOptimisticPolicyTable_toMarkovPolicy (mdp : MDP State Action) (summary : TransitionCountSummary mdp) (defaultState : State) (countRadius : TransitionCountRadius) : (summary.countRadiusOptimisticPolicyTable mdp defaultState countRadius).toMarkovPolicy = (summary.countRadiusOptimisticPlan mdp defaultState countRadius).optimisticPolicy

Cumulative known-reward optimistic plan recommended after one trajectory prefix.

noncomputable def adaptiveCumulativeEmpiricalOptimisticPlanAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (round : Nat) : mdp.EstimatedModelPlan

Sum of expected regrets of all cumulative empirical recommendations.

noncomputable def adaptiveCumulativeEmpiricalOptimisticRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (rounds : Nat) : Real

Cumulative optimistic table selected from every observed batch in a prefix.

noncomputable def successorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (countRadius : TransitionCountRadius) (n : Nat) (history : EpisodeBatchPrefix mdp episodes n) : DeterministicMarkovPolicyTable mdp

The cumulative history-to-table selector is measurable.

theorem measurable_successorTable {mdp : MDP State Action} {episodes : Nat} (defaultState : State) (countRadius : TransitionCountRadius) (n : Nat) : Measurable (successorTable (mdp

Exploratory behavior source centered on cumulative empirical recommendations.

noncomputable def exploratorySource (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (episodes : Nat) (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) : AdaptiveEpisodeBatchSource mdp initialState episodes where

The source's successor behavior is centered on the cumulative optimistic table.

theorem exploratorySource_successorPolicy {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (initialTable : DeterministicMarkovPolicyTable mdp) (defaultState : State) (countRadius : TransitionCountRadius) (explorationRate : NNReal) (hexplorationRate : explorationRate <= 1) (n : Nat) (history : EpisodeBatchPrefix mdp episodes n) : (exploratorySource mdp initialState episodes initialTable defaultState countRadius explorationRate hexplorationRate).successorPolicy n history = (successorTable defaultState countRadius n history).exploratoryPolicy explorationRate hexplorationRate

One global event contract for cumulative empirical plans. The missing statistical producer must supply coordinate confidence for every cumulative prefix plan outside `badEvent`.

structure AdaptiveCumulativeCoordinateConfidenceContract {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (defaultState : State) (countRadius : TransitionCountRadius) (rounds : Nat) (delta : Real) where

Roundwise cumulative confidence and a selected-radius envelope imply global optimism and the explicit finite recommendation-regret sum.

theorem adaptiveCumulativeCoordinateConfidence_optimism_and_recommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (defaultState : State) (countRadius : TransitionCountRadius) (radiusEnvelope : Fin rounds -> Real) (confidence : forall round : Fin rounds, (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).CoordinateConfidence) (hradius : forall (round : Fin rounds) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State), (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).selectedRadiusRemaining remaining hremaining state <= radiusEnvelope round) : (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticRecommendedExpectedRegret (initialState

Route endpoint: one measurable global cumulative-confidence event yields global optimism and an explicit shrinking-radius recommendation-regret bound.

theorem AdaptiveCumulativeCoordinateConfidenceContract.trajectoryMeasure_optimism_and_explicitRecommendedExpectedRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] {episodes rounds : Nat} (source : AdaptiveEpisodeBatchSource mdp initialState episodes) (defaultState : State) (countRadius : TransitionCountRadius) (delta : Real) (contract : AdaptiveCumulativeCoordinateConfidenceContract source defaultState countRadius rounds delta) (radiusEnvelope : Fin rounds -> Real) (hradius : forall trajectory, trajectory ∉ contract.badEvent -> forall (round : Fin rounds) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State), (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).selectedRadiusRemaining remaining hremaining state <= radiusEnvelope round) : MeasurableSet contract.badEvent /\ source.trajectoryMeasure contract.badEvent <= ENNReal.ofReal delta /\ forall trajectory, trajectory ∉ contract.badEvent -> (forall round : Fin rounds, forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= (adaptiveCumulativeEmpiricalOptimisticPlanAt trajectory defaultState countRadius round).upperValueRemaining mdp.horizon le_rfl state) /\ adaptiveCumulativeEmpiricalOptimisticRecommendedExpectedRegret (initialState