Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonOptimisticCertificate
# Finite-horizon optimistic Bellman certificates 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
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.
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
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.
structure OptimisticBellmanCertificate (mdp : MDP State Action) where
def
BanditRLProof.FiniteHorizonRL.MDP.optimalBellmanCertificate
Compiled
The true optimal value itself is the canonical exact optimistic certificate.
noncomputable def optimalBellmanCertificate (mdp : MDP State Action) : OptimisticBellmanCertificate mdp where
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_upperValueRemaining
Compiled
Every upper-value surface is measurable on the finite discrete state space.
theorem measurable_upperValueRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (certificate.upperValueRemaining remaining hremaining)
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.optimalValueRemaining_le_upperValueRemaining
Compiled
Local Bellman optimism implies the upper values dominate the true optimal values.
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
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)`.
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)
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_succ
Compiled
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)
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.occupancySumRemaining_mono
Compiled
Pointwise domination of stage costs lifts to domination of their occupancy sums.
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
def
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual
Compiled
Policy Bellman residual of an optimistic upper-value plan.
noncomputable def policyBellmanResidual {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : Real
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.measurable_policyBellmanResidual
Compiled
The optimistic policy Bellman residual is measurable.
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)
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.policyBellmanResidual_nonneg
Compiled
Every policy Bellman residual of an optimistic certificate is nonnegative.
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
def
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining
Compiled
Recursive true-occupancy sum of the certificate's policy Bellman residuals.
noncomputable def residualOccupancyRemaining {mdp : MDP State Action} (certificate : OptimisticBellmanCertificate mdp) (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (mu : Measure State) : Real
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.
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
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.
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
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_nonneg
Compiled
The residual occupancy sum is nonnegative.
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
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.expectedRegret_le_residualOccupancyRemaining
Compiled
Single-episode expected regret is bounded by the optimistic residual occupancy sum.
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
theorem
BanditRLProof.FiniteHorizonRL.MDP.OptimisticBellmanCertificate.residualOccupancyRemaining_le_occupancySumRemaining
Compiled
A pointwise bonus bound on Bellman residuals bounds the residual occupancy sum.
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
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.
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