Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonOccupancyRegret

# Finite-horizon occupancy regret identity This module connects finite-horizon Bellman optimality to expected trajectory regret. It constructs chronological state occupancies, records the expected one-step Bellman optimality gap under a policy, and recursively sums those gaps along the policy-induced state laws. The resulting occupancy functional is exactly the difference between optimal and policy value, hence exactly the expected trajectory regret. The measurable greedy policy has zero regret.

Module map

Source: BanditRLProof/RL/FiniteHorizonOccupancyRegret.lean
Teaching chapter: 9. Finite-horizon reinforcement learning
Declarations: 19
Placeholders: 0

Imports

BanditRLProof.RL.FiniteHorizonOptimality

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonOptimisticCertificate

Declarations

Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.stateOccupancy Compiled

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)

Source line 31 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.policyBellmanGap Compiled

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

Source line 61 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.measurable_policyBellmanGap Compiled

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)

Source line 69 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.policyBellmanGap_nonneg Compiled

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

Source line 79 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.policyBellmanGap_stageOfRemaining Compiled

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

Source line 92 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_inducedStateKernel_eq_integral_transitionValue Compiled

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

Source line 113 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.bellman_sub_bellman_eq_integral_inducedStateKernel_sub Compiled

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

Source line 134 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.integral_sub_comp_inducedStateKernel_eq_integral_bellman_sub Compiled

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

Source line 186 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancyGapRemaining Compiled

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)

Source line 214 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancyGapRemaining_succ Compiled

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)

Source line 231 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancyGapRemaining_eq_integral_optimalValueRemaining_sub_valueRemaining Compiled

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

Source line 248 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.valueRemaining_le_optimalValueRemaining Compiled

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

Source line 291 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancyGapRemaining_nonneg Compiled

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

Source line 311 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret Compiled

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

Source line 323 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret_eq_integral_optimalValueAt_sub_valueAt Compiled

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

Source line 331 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret_eq_occupancyGapRemaining Compiled

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

Source line 351 Open teaching explanation Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.expectedRegret_nonneg Compiled

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

Source line 361 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.optimalPolicy_expectedRegret_eq_zero Compiled

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

Source line 373 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.expectedRegret_eq_occupancyGap_nonneg_and_optimalPolicy_zero Compiled

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

Source line 386 Chapter context: Finite-horizon RL