BanditRLProof.RL.FiniteHorizonOccupancyRegret

State law at a chronological stage under a Markov policy.

noncomputable def stateOccupancy {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) : (stage : Nat) -> stage <= mdp.horizon -> Measure State | 0, _ => initialState | stage + 1, hstage => policy.inducedStateKernel ⟨stage, by omega⟩ ∘ₘ policy.stateOccupancy initialState stage (by omega) /-- Every chronological state occupancy is a probability measure. -/ instance instStateOccupancyIsProbabilityMeasure {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Nat) (hstage : stage <= mdp.horizon) : IsProbabilityMeasure (policy.stateOccupancy initialState stage hstage)

Expected one-step optimality gap after averaging the optimal action-value gap over the policy action kernel at a chronological stage.

noncomputable def policyBellmanGap {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) : Real

The policy-averaged one-step Bellman optimality gap is measurable.

theorem measurable_policyBellmanGap {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) : Measurable (policy.policyBellmanGap stage)

Every policy-averaged one-step Bellman optimality gap is nonnegative.

theorem policyBellmanGap_nonneg {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) : 0 <= policy.policyBellmanGap stage state

Reindex a chronological policy Bellman gap by the number of decisions remaining.

theorem policyBellmanGap_stageOfRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : policy.policyBellmanGap ⟨mdp.horizon - (remaining + 1), by omega⟩ state = mdp.optimalValueRemaining (remaining + 1) hremaining state - policy.bellman ⟨mdp.horizon - (remaining + 1), by omega⟩ (mdp.optimalValueRemaining remaining (by omega)) state

Integrating a continuation value against the induced state kernel averages its transition expectation over the policy action kernel.

theorem integral_inducedStateKernel_eq_integral_transitionValue {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : (∫ nextState, value nextState ∂policy.inducedStateKernel stage state) = ∫ action, mdp.transitionValue value state action ∂policy.actionKernel stage state

Changing only the continuation value in a policy Bellman step is integration against the induced next-state kernel.

theorem bellman_sub_bellman_eq_integral_inducedStateKernel_sub {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (left right : State -> Real) (state : State) : policy.bellman stage left state - policy.bellman stage right state = ∫ nextState, left nextState - right nextState ∂policy.inducedStateKernel stage state

Push an integrated continuation-value difference through one policy-induced state step.

theorem integral_sub_comp_inducedStateKernel_eq_integral_bellman_sub {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (left right : State -> Real) (mu : Measure State) [IsProbabilityMeasure mu] : (∫ nextState, left nextState - right nextState ∂policy.inducedStateKernel stage ∘ₘ mu) = ∫ state, policy.bellman stage left state - policy.bellman stage right state ∂mu

Finite occupancy sum of policy Bellman gaps, indexed by decisions remaining. Each recursive call advances the state law by the policy-induced kernel.

noncomputable def occupancyGapRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> Measure State -> Real | 0, _, _ => 0 | remaining + 1, hremaining, mu => let stage : Fin mdp.horizon := ⟨mdp.horizon - (remaining + 1), by omega⟩ (∫ state, mdp.optimalValueRemaining (remaining + 1) hremaining state - policy.bellman stage (mdp.optimalValueRemaining remaining (by omega)) state ∂mu) + policy.occupancyGapRemaining remaining (by omega) (policy.inducedStateKernel stage ∘ₘ mu) omit [MeasurableSingletonClass State] in /-- The successor recursion is an integral of the chronological policy Bellman gap plus the remaining occupancy gaps under the next-state law. -/ theorem occupancyGapRemaining_succ {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (mu : Measure State) : policy.occupancyGapRemaining (remaining + 1) hremaining mu = (∫ state, policy.policyBellmanGap ⟨mdp.horizon - (remaining + 1), by omega⟩ state ∂mu) + policy.occupancyGapRemaining remaining (by omega) (policy.inducedStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ ∘ₘ mu)

The successor recursion is an integral of the chronological policy Bellman gap plus the remaining occupancy gaps under the next-state law.

theorem occupancyGapRemaining_succ {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (mu : Measure State) : policy.occupancyGapRemaining (remaining + 1) hremaining mu = (∫ state, policy.policyBellmanGap ⟨mdp.horizon - (remaining + 1), by omega⟩ state ∂mu) + policy.occupancyGapRemaining remaining (by omega) (policy.inducedStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ ∘ₘ mu)

The recursive occupancy-gap sum is exactly the integrated optimal-policy value gap.

theorem occupancyGapRemaining_eq_integral_optimalValueRemaining_sub_valueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : policy.occupancyGapRemaining remaining hremaining mu = ∫ state, mdp.optimalValueRemaining remaining hremaining state - policy.valueRemaining remaining hremaining state ∂mu

Backward policy value is bounded by backward optimal value.

theorem valueRemaining_le_optimalValueRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : policy.valueRemaining remaining hremaining state <= mdp.optimalValueRemaining remaining hremaining state

The finite occupancy Bellman-gap sum is nonnegative.

theorem occupancyGapRemaining_nonneg {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : 0 <= policy.occupancyGapRemaining remaining hremaining mu

Expected finite-horizon regret: optimal initial value minus generated trajectory reward.

noncomputable def expectedRegret {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) : Real

Expected trajectory regret is the initial-law integral of the optimal-policy value gap.

theorem expectedRegret_eq_integral_optimalValueAt_sub_valueAt {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : policy.expectedRegret initialState = ∫ state, mdp.optimalValueAt 0 (Nat.zero_le mdp.horizon) state - policy.valueAt 0 (Nat.zero_le mdp.horizon) state ∂initialState

Expected trajectory regret equals the full recursively accumulated occupancy Bellman gap.

theorem expectedRegret_eq_occupancyGapRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : policy.expectedRegret initialState = policy.occupancyGapRemaining mdp.horizon le_rfl initialState

Expected finite-horizon regret is nonnegative.

theorem expectedRegret_nonneg {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : 0 <= policy.expectedRegret initialState

The measurable greedy policy has zero expected finite-horizon regret.

theorem optimalPolicy_expectedRegret_eq_zero (mdp : MDP State Action) (initialState : Measure State) [IsProbabilityMeasure initialState] : mdp.optimalPolicy.expectedRegret initialState = 0

Route endpoint: expected trajectory regret is exactly the finite occupancy Bellman-gap sum, is nonnegative for every Markov policy, and vanishes for the compiled measurable greedy optimal policy.

theorem expectedRegret_eq_occupancyGap_nonneg_and_optimalPolicy_zero (mdp : MDP State Action) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : policy.expectedRegret initialState = policy.occupancyGapRemaining mdp.horizon le_rfl initialState /\ 0 <= policy.expectedRegret initialState /\ mdp.optimalPolicy.expectedRegret initialState = 0