BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIEpisodeRegret

Nonnegative deterministic rewards give nonnegative finite-horizon policy values.

theorem valueRemaining_nonneg_of_reward_nonneg {mdp : MDP State Action} (policy : MarkovPolicy mdp) (hreward : ∀ state action, 0 <= mdp.reward state action) : ∀ remaining (hremaining : remaining <= mdp.horizon) state, 0 <= policy.valueRemaining remaining hremaining state

The recurrent Q table used at generated episode coordinate `episode`: exactly the strict prefix `0,...,episode-1` is folded.

noncomputable def generatedQTable (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) : QTable mdp

The deterministic argmax table of that exact generated Q table.

noncomputable def generatedPolicyTable (mdp : MDP State Action) (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) : DeterministicMarkovPolicyTable mdp

The canonical source policy at every coordinate is definitionally the argmax of `generatedQTable` built from its strict prefix.

theorem recurrentSource_policyAt_eq_generatedPolicyTable (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] (defaultState : State) (episodes : Nat) (delta : Real) (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) : (recurrentSource mdp initialState defaultState episodes delta).policyAt trajectory episode = DeterministicMarkovPolicyTable.toMarkovPolicy (generatedPolicyTable mdp defaultState episodes delta trajectory episode)

Totalized initial state of one generated single-episode batch. On the canonical positive-horizon domain it is literally stage zero's state.

def generatedEpisodeInitialState (mdp : MDP State Action) (defaultState : State) (batch : EpisodeBatch mdp 1) : State

Pathwise policy-value pseudo-regret of one generated coordinate.

noncomputable def generatedEpisodePseudoRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (defaultState : State) (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) : Real

Raw generated cumulative episode pseudo-regret over exactly coordinates `0,...,K-1`; coordinate zero is included and never hidden.

noncomputable def cumulativeEpisodePseudoRegret {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (defaultState : State) (episodes : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) : Real

Every generated policy-value pseudo-regret lies in `[0,H]` under rewards in `[0,1]`.

theorem generatedEpisodePseudoRegret_mem_Icc {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (defaultState : State) (trajectory : EpisodeBatchTrajectory mdp 1) (episode : Nat) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : generatedEpisodePseudoRegret source defaultState trajectory episode ∈ Set.Icc (0 : Real) mdp.horizon

Consequently the exact `K`-episode raw pseudo-regret lies in `[0,K H]`; this is the envelope later used only on the terminal failure event.

theorem cumulativeEpisodePseudoRegret_mem_Icc {mdp : MDP State Action} {initialState : Measure State} [IsProbabilityMeasure initialState] (source : AdaptiveEpisodeBatchSource mdp initialState 1) (defaultState : State) (episodes : Nat) (trajectory : EpisodeBatchTrajectory mdp 1) (hrewardNonneg : ∀ state action, 0 <= mdp.reward state action) (hrewardOne : ∀ state action, mdp.reward state action <= 1) : cumulativeEpisodePseudoRegret source defaultState episodes trajectory ∈ Set.Icc (0 : Real) ((episodes : Real) * mdp.horizon)