Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonCoordinateModelConfidence
# Coordinate confidence for finite-horizon estimated models This module turns finite-state singleton transition-mass errors into the transition-expectation confidence consumed by the estimated-model optimistic regret route. The only value regularity required is an absolute envelope for the recursively generated tail upper value.
Module map
Imports
BanditRLProof.RL.FiniteHorizonEstimatedModelCertificate
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.FiniteHorizonRL.abs_integral_sub_integral_le_sum_coordinateRadius_mul_envelope
Compiled
On a finite measurable space, coordinate bounds on singleton masses control the expectation error of every pointwise-enveloped real value.
theorem abs_integral_sub_integral_le_sum_coordinateRadius_mul_envelope (estimated trueMeasure : Measure State) [IsFiniteMeasure estimated] [IsFiniteMeasure trueMeasure] (value coordinateRadius : State -> Real) (envelope : Real) (hcoordinate : forall state, |estimated.real {state} - trueMeasure.real {state}| <= coordinateRadius state) (hvalue : forall state, |value state| <= envelope) : |(∫ state, value state ∂estimated) - ∫ state, value state ∂trueMeasure| <= ∑ state, coordinateRadius state * envelope
structure
BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.CoordinateConfidence
Compiled
Finite-state coordinate confidence sufficient for the recursive optimistic model route. The transition radius may be any upper bound on the displayed coordinate sum, so later concentration producers can choose their own radii.
structure CoordinateConfidence {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) where
theorem
BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.CoordinateConfidence.transitionError_le_radius
Compiled
Coordinate transition confidence implies the recursive Bellman error bound.
theorem CoordinateConfidence.transitionError_le_radius {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.CoordinateConfidence) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) : |plan.transitionValue (mdp.decisionStageRemaining remaining hremaining) (plan.upperValueRemaining remaining (by omega)) state action - mdp.transitionValue (plan.upperValueRemaining remaining (by omega)) state action| <= plan.transitionRadius (mdp.decisionStageRemaining remaining hremaining) state action
def
BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.CoordinateConfidence.toConfidence
Compiled
Package coordinate confidence as the existing estimated-model confidence.
def CoordinateConfidence.toConfidence {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.CoordinateConfidence) : plan.Confidence where
theorem
BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.CoordinateConfidence.optimism_and_expectedRegret_le_two_occupancySelectedRadiusRemaining
Compiled
Route endpoint: coordinate model confidence gives global optimism and the compiled selected-radius single-episode expected-regret bound.
theorem CoordinateConfidence.optimism_and_expectedRegret_le_two_occupancySelectedRadiusRemaining {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.CoordinateConfidence) (initialState : Measure State) [IsProbabilityMeasure initialState] : (forall state, mdp.optimalValueRemaining mdp.horizon le_rfl state <= plan.upperValueRemaining mdp.horizon le_rfl state) /\ plan.optimisticPolicy.expectedRegret initialState <= plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState