BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonOptimisticCertificate

This module isolates the deterministic dynamic-programming interface needed by optimistic finite-horizon RL. A certificate supplies upper values with zero terminal value and a one-step upper Bellman inequality. Backward induction turns that local contract into global optimism. For any Markov policy, the upper-value minus policy-value difference is then exactly a recursive sum of Bellman residuals under the true policy-induced state laws. A pointwise bonus bound on those residuals yields a finite-episode expected-regret bound.

Module map

Declarations
18
Placeholders
0

Imports

BanditRLProof.RL.FiniteHorizonOccupancyRegret

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonEstimatedModelCertificate

Declarations

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

theorem BanditRLProof.FiniteHorizonRL.MDP.optimalBellman_mono Compiled

The finite-action optimal Bellman operator is monotone in its continuation value.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.optimalBellman_mono

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem optimalBellman_mono (mdp : MDP State Action) {left right : State -> Real} (hle : forall state, left state <= right state) (state : State) : mdp.optimalBellman left state <= mdp.optimalBellman right state
Source line 31 Chapter context: Finite-horizon RL
structure BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate Compiled

An upper-value plan whose terminal value is zero and whose successor surface dominates one true optimal Bellman backup of its tail surface.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

structure OptimisticBellmanCertificate (mdp : MDP State Action) where
Source line 47 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.optimalBellmanCertificate Compiled

The true optimal value itself is the canonical exact optimistic certificate.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.optimalBellmanCertificate

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def optimalBellmanCertificate (mdp : MDP State Action) : OptimisticBellmanCertificate mdp where
Source line 60 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_upperValueRemaining Compiled

Every upper-value surface is measurable on the finite discrete state space.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_upperValueRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurable_upperValueRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (certificate.upperValueRemaining remaining hremaining)
Source line 71 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.optimalValueRemaining_le_upperValueRemaining Compiled

Local Bellman optimism implies the upper values dominate the true optimal values.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.optimalValueRemaining_le_upperValueRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem optimalValueRemaining_le_upperValueRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : mdp.optimalValueRemaining remaining hremaining state <= certificate.upperValueRemaining remaining hremaining state
Source line 78 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining Compiled

Recursive occupancy sum for a remaining-horizon-indexed stage cost. At a successor step, cost index `remaining` is chronological stage `horizon - (remaining + 1)`.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def occupancySumRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (cost : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real) : (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, cost remaining hremaining state ∂mu) + policy.occupancySumRemaining cost remaining (by omega) (policy.inducedStateKernel stage ∘ₘ mu) omit [MeasurableSingletonClass State] [Nonempty Action] in /-- Successor equation for a generic recursive occupancy sum. -/ theorem occupancySumRemaining_succ {mdp : MDP State Action} (policy : MarkovPolicy mdp) (cost : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (mu : Measure State) : policy.occupancySumRemaining cost (remaining + 1) hremaining mu = (∫ state, cost remaining hremaining state ∂mu) + policy.occupancySumRemaining cost remaining (by omega) (policy.inducedStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ ∘ₘ mu)
Source line 105 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_succ Compiled

Successor equation for a generic recursive occupancy sum.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_succ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem occupancySumRemaining_succ {mdp : MDP State Action} (policy : MarkovPolicy mdp) (cost : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (mu : Measure State) : policy.occupancySumRemaining cost (remaining + 1) hremaining mu = (∫ state, cost remaining hremaining state ∂mu) + policy.occupancySumRemaining cost remaining (by omega) (policy.inducedStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ ∘ₘ mu)
Source line 120 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_mono Compiled

Pointwise domination of stage costs lifts to domination of their occupancy sums.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_mono

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem occupancySumRemaining_mono {mdp : MDP State Action} (policy : MarkovPolicy mdp) {left right : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real} (hle : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State), left remaining hremaining state <= right remaining hremaining state) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : policy.occupancySumRemaining left remaining hremaining mu <= policy.occupancySumRemaining right remaining hremaining mu
Source line 135 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual Compiled

Policy Bellman residual of an optimistic upper-value plan.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def policyBellmanResidual {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : Real
Source line 169 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_policyBellmanResidual Compiled

The optimistic policy Bellman residual is measurable.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_policyBellmanResidual

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurable_policyBellmanResidual {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : Measurable (certificate.policyBellmanResidual policy remaining hremaining)
Source line 178 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual_nonneg Compiled

Every policy Bellman residual of an optimistic certificate is nonnegative.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem policyBellmanResidual_nonneg {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : 0 <= certificate.policyBellmanResidual policy remaining hremaining state
Source line 188 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining Compiled

Recursive true-occupancy sum of the certificate's policy Bellman residuals.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def residualOccupancyRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) : Real
Source line 203 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_eq_integral_upperValueRemaining_sub_valueRemaining Compiled

The residual occupancy sum is exactly the integrated difference between the certificate upper value and the supplied policy value.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_eq_integral_upperValueRemaining_sub_valueRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem residualOccupancyRemaining_eq_integral_upperValueRemaining_sub_valueRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : certificate.residualOccupancyRemaining policy remaining hremaining mu = ∫ state, certificate.upperValueRemaining remaining hremaining state - policy.valueRemaining remaining hremaining state ∂mu
Source line 214 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.optimalBellmanCertificate_residualOccupancyRemaining_eq_occupancyGapRemaining Compiled

For the canonical exact certificate, residual occupancy is the previously compiled optimality gap occupancy sum.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.optimalBellmanCertificate_residualOccupancyRemaining_eq_occupancyGapRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem optimalBellmanCertificate_residualOccupancyRemaining_eq_occupancyGapRemaining {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : mdp.optimalBellmanCertificate.residualOccupancyRemaining policy remaining hremaining mu = policy.occupancyGapRemaining remaining hremaining mu
Source line 266 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_nonneg Compiled

The residual occupancy sum is nonnegative.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_nonneg

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem residualOccupancyRemaining_nonneg {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : 0 <= certificate.residualOccupancyRemaining policy remaining hremaining mu
Source line 278 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.expectedRegret_le_residualOccupancyRemaining Compiled

Single-episode expected regret is bounded by the optimistic residual occupancy sum.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.expectedRegret_le_residualOccupancyRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem expectedRegret_le_residualOccupancyRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] : policy.expectedRegret initialState <= certificate.residualOccupancyRemaining policy mdp.horizon le_rfl initialState
Source line 294 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_le_occupancySumRemaining Compiled

A pointwise bonus bound on Bellman residuals bounds the residual occupancy sum.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_le_occupancySumRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem residualOccupancyRemaining_le_occupancySumRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (bonus : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real) (hbonus : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State), certificate.policyBellmanResidual policy remaining hremaining state <= bonus remaining hremaining state) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) [IsProbabilityMeasure mu] : certificate.residualOccupancyRemaining policy remaining hremaining mu <= policy.occupancySumRemaining bonus remaining hremaining mu
Source line 313 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.expectedRegret_le_residual_le_occupancyBonusRemaining Compiled

Route endpoint: local true-Bellman optimism induces global value optimism; single-episode expected regret is bounded by the true-occupancy residual sum; and any pointwise bonus dominating those residuals bounds regret.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.expectedRegret_le_residual_le_occupancyBonusRemaining

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem expectedRegret_le_residual_le_occupancyBonusRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (bonus : (remaining : Nat) -> remaining + 1 <= mdp.horizon -> State -> Real) (hbonus : forall (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State), certificate.policyBellmanResidual policy remaining hremaining state <= bonus remaining hremaining state) : 0 <= certificate.residualOccupancyRemaining policy mdp.horizon le_rfl initialState /\ policy.expectedRegret initialState <= certificate.residualOccupancyRemaining policy mdp.horizon le_rfl initialState /\ certificate.residualOccupancyRemaining policy mdp.horizon le_rfl initialState <= policy.occupancySumRemaining bonus mdp.horizon le_rfl initialState /\ policy.expectedRegret initialState <= policy.occupancySumRemaining bonus mdp.horizon le_rfl initialState
Source line 334 Chapter context: Finite-horizon RL