Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonEstimatedModelCertificate

# Estimated finite-horizon models produce optimistic certificates This module connects a stage-indexed estimated reward/transition model to the compiled deterministic optimistic-certificate route. Separate two-sided reward and transition-expectation radii are required only on the recursively generated tail upper values. They produce a true Bellman certificate. The deterministic policy greedy for the estimated optimistic backup then has true Bellman residual at most twice its selected reward-plus-transition radius, so the existing occupancy theorem gives a single-episode expected-regret bound.

Module map

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

Imports

BanditRLProof.FiniteRealArgmax, BanditRLProof.RL.FiniteHorizonOptimisticCertificate

Imported by

BanditRLProof, BanditRLProof.RL.FiniteHorizonCoordinateModelConfidence

Declarations

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

def BanditRLProof.FiniteHorizonRL.MDP.decisionStageRemaining Compiled

Chronological stage corresponding to a successor remaining-horizon index.

def decisionStageRemaining (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : Fin mdp.horizon

Source line 32 Chapter context: Finite-horizon RL

structure BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan Compiled

A stage-indexed estimated MDP together with separate reward and transition confidence radii. Confidence itself is a downstream proposition because the transition error is evaluated on the recursively generated upper value.

structure EstimatedModelPlan (mdp : MDP State Action) where

Source line 41 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.exactModelPlan Compiled

The true MDP with zero radii is the canonical exact estimated plan.

def exactModelPlan (mdp : MDP State Action) : EstimatedModelPlan mdp where

Source line 65 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.transitionValue Compiled

Estimated next-state expectation of a continuation value.

noncomputable def transitionValue {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) (action : Action) : Real

Source line 76 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.bellmanQ Compiled

Estimated one-step reward plus continuation value.

noncomputable def bellmanQ {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) (action : Action) : Real

Source line 83 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticQ Compiled

Estimated Bellman action value enlarged by both confidence radii.

noncomputable def optimisticQ {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) (action : Action) : Real

Source line 91 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.measurable_transitionValue Compiled

The estimated transition-value surface is measurable in the state-action pair.

theorem measurable_transitionValue {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) {value : State -> Real} (hvalue : Measurable value) : Measurable (Function.uncurry (plan.transitionValue stage value))

Source line 101 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.measurable_optimisticQ Compiled

The optimistic estimated action-value surface is measurable.

theorem measurable_optimisticQ {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) {value : State -> Real} (hvalue : Measurable value) : Measurable (Function.uncurry (plan.optimisticQ stage value))

Source line 110 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticAction Compiled

A finite action maximizing the estimated optimistic action value.

noncomputable def optimisticAction {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : Action

Source line 122 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticQ_le_optimisticAction Compiled

Every action is bounded by the selected optimistic estimated action value.

theorem optimisticQ_le_optimisticAction {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) (action : Action) : plan.optimisticQ stage value state action <= plan.optimisticQ stage value state (plan.optimisticAction stage value state)

Source line 130 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticBellman Compiled

Pointwise maximum of the estimated optimistic action values.

noncomputable def optimisticBellman {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : Real

Source line 141 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.measurable_optimisticAction Compiled

The finite-state estimated optimistic selector is measurable.

theorem measurable_optimisticAction {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) : Measurable (plan.optimisticAction stage value)

Source line 148 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.upperValueRemaining Compiled

Recursive estimated optimistic value indexed by decisions remaining.

noncomputable def upperValueRemaining {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) : (remaining : Nat) -> remaining <= mdp.horizon -> State -> Real | 0, _ => fun _ => 0 | remaining + 1, hremaining => plan.optimisticBellman (mdp.decisionStageRemaining remaining hremaining) (plan.upperValueRemaining remaining (by omega)) omit [MeasurableSingletonClass State] in /-- Transport the dependent upper-value recursion across equal remaining horizons. -/ theorem upperValueRemaining_eq_of_eq {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : plan.upperValueRemaining left hleft = plan.upperValueRemaining right hright

Source line 155 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.upperValueRemaining_eq_of_eq Compiled

Transport the dependent upper-value recursion across equal remaining horizons.

theorem upperValueRemaining_eq_of_eq {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) {left right : Nat} (hleft : left <= mdp.horizon) (hright : right <= mdp.horizon) (h : left = right) : plan.upperValueRemaining left hleft = plan.upperValueRemaining right hright

Source line 165 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.measurable_upperValueRemaining Compiled

Every recursively generated upper-value surface is measurable.

theorem measurable_upperValueRemaining {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) : Measurable (plan.upperValueRemaining remaining hremaining)

Source line 175 Chapter context: Finite-horizon RL

structure BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence Compiled

Two-sided model confidence on the recursive upper-value route. The transition contract is deliberately not quantified over arbitrary unbounded values.

structure Confidence {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) : Prop where

Source line 185 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.exactModelPlan_confidence Compiled

The canonical exact estimated plan satisfies confidence by reflexivity.

theorem exactModelPlan_confidence (mdp : MDP State Action) : (exactModelPlan mdp).Confidence

Source line 203 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.trueBellmanQ_le_optimisticQ Compiled

Two-sided confidence makes every true action value optimistic.

theorem Confidence.trueBellmanQ_le_optimisticQ {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) (action : Action) : mdp.bellmanQ (plan.upperValueRemaining remaining (by omega)) state action <= plan.optimisticQ (mdp.decisionStageRemaining remaining hremaining) (plan.upperValueRemaining remaining (by omega)) state action

Source line 213 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.certificate Compiled

The recursive estimated optimistic values form a true Bellman certificate.

noncomputable def certificate {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (confidence : plan.Confidence) : mdp.OptimisticBellmanCertificate where

Source line 231 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.optimalValueRemaining_le_upperValueRemaining Compiled

Estimated-model confidence implies pointwise global optimism.

theorem Confidence.optimalValueRemaining_le_upperValueRemaining {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (state : State) : mdp.optimalValueRemaining remaining hremaining state <= plan.upperValueRemaining remaining hremaining state

Source line 258 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticActionAt Compiled

Estimated optimistic action at a chronological stage.

noncomputable def optimisticActionAt {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) : State -> Action

Source line 268 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.measurable_optimisticActionAt Compiled

The chronological estimated optimistic selector is measurable.

theorem measurable_optimisticActionAt {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) : Measurable (plan.optimisticActionAt stage)

Source line 276 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticPolicy Compiled

Deterministic Markov policy greedy for each estimated optimistic backup.

noncomputable def optimisticPolicy {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) : MarkovPolicy mdp where

Source line 283 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticActionAt_decisionStageRemaining Compiled

Remaining-horizon and chronological selectors agree exactly.

theorem optimisticActionAt_decisionStageRemaining {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) : plan.optimisticActionAt (mdp.decisionStageRemaining remaining hremaining) = plan.optimisticAction (mdp.decisionStageRemaining remaining hremaining) (plan.upperValueRemaining remaining (by omega))

Source line 296 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.optimisticPolicy_bellman_eq_bellmanQ Compiled

The deterministic estimated-greedy policy Bellman integral selects its action.

theorem optimisticPolicy_bellman_eq_bellmanQ {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (stage : Fin mdp.horizon) (value : State -> Real) (state : State) : plan.optimisticPolicy.bellman stage value state = mdp.bellmanQ value state (plan.optimisticActionAt stage state)

Source line 311 Chapter context: Finite-horizon RL

def BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.selectedRadiusRemaining Compiled

Reward-plus-transition radius selected by the estimated optimistic policy.

noncomputable def selectedRadiusRemaining {mdp : MDP State Action} (plan : EstimatedModelPlan mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : Real

Source line 324 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.selectedRadiusRemaining_nonneg Compiled

Every selected radius is nonnegative under the two-sided confidence contract.

theorem Confidence.selectedRadiusRemaining_nonneg {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : 0 <= plan.selectedRadiusRemaining remaining hremaining state

Source line 336 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.policyBellmanResidual_le_two_selectedRadiusRemaining Compiled

The estimated-greedy policy residual is at most twice its selected model confidence radius. One side of each absolute-error bound produced optimism; the other side controls the remaining selected-action overestimate.

theorem Confidence.policyBellmanResidual_le_two_selectedRadiusRemaining {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (state : State) : (plan.certificate confidence).policyBellmanResidual plan.optimisticPolicy remaining hremaining state <= 2 * plan.selectedRadiusRemaining remaining hremaining state

Source line 357 Chapter context: Finite-horizon RL

theorem BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.expectedRegret_le_two_occupancySelectedRadiusRemaining Compiled

Full residual chain for the estimated-greedy policy under a probability initial law.

theorem Confidence.expectedRegret_le_two_occupancySelectedRadiusRemaining {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (initialState : Measure State) [IsProbabilityMeasure initialState] : 0 <= (plan.certificate confidence).residualOccupancyRemaining plan.optimisticPolicy mdp.horizon le_rfl initialState /\ plan.optimisticPolicy.expectedRegret initialState <= (plan.certificate confidence).residualOccupancyRemaining plan.optimisticPolicy mdp.horizon le_rfl initialState /\ (plan.certificate confidence).residualOccupancyRemaining plan.optimisticPolicy mdp.horizon le_rfl initialState <= plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState /\ plan.optimisticPolicy.expectedRegret initialState <= plan.optimisticPolicy.occupancySumRemaining (fun remaining hremaining state => 2 * plan.selectedRadiusRemaining remaining hremaining state) mdp.horizon le_rfl initialState

Source line 392 Chapter context: Finite-horizon RL

theorem

BanditRLProof.FiniteHorizonRL.MDP.EstimatedModelPlan.Confidence.optimism_and_expectedRegret_le_two_occupancySelectedRadiusRemaining

Compiled

Route endpoint: estimated-model confidence simultaneously gives global optimism and the selected-radius single-episode expected-regret bound.

theorem Confidence.optimism_and_expectedRegret_le_two_occupancySelectedRadiusRemaining {mdp : MDP State Action} {plan : EstimatedModelPlan mdp} (confidence : plan.Confidence) (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

Source line 425 Chapter context: Finite-horizon RL