Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStageVisitFactorization
# Generated stage-visit factorization This module factors a generated trajectory's stage/state/action visit mass into the corresponding stage-state mass and the policy action-kernel singleton mass. It is a population-law identity only: no reachability, action support, episode count, concentration, or regret premise is introduced.
Module map
Imports
BanditRLProof.RL.FiniteHorizonStageTransitionJointFactorization
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAlignment, BanditRLProof.RL.FiniteHorizonExploratoryReachabilityCalibration
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.MDP.stageOfRemainingCoordinate
Compiled
Chronological MDP stage represented by one coordinate of a remaining trace.
def stageOfRemainingCoordinate (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (coordinate : Fin remaining) : Fin mdp.horizon
theorem
BanditRLProof.FiniteHorizonRL.MDP.stageOfRemainingCoordinate_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stageOfRemainingCoordinate_succ (mdp : MDP State Action) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (coordinate : Fin remaining) : mdp.stageOfRemainingCoordinate (remaining + 1) hremaining coordinate.succ = mdp.stageOfRemainingCoordinate remaining (by omega) coordinate
theorem
BanditRLProof.FiniteHorizonRL.MDP.stageOfRemainingCoordinate_full
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stageOfRemainingCoordinate_full (mdp : MDP State Action) (stage : Fin mdp.horizon) : mdp.stageOfRemainingCoordinate mdp.horizon le_rfl stage = stage
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryKernelRemaining_visitEvent_eq_stateEvent_mul_action
Compiled
Inside a remaining generated trace, a state/action visit factors into the state event and the action singleton selected by the chronological policy kernel.
theorem trajectoryKernelRemaining_visitEvent_eq_stateEvent_mul_action {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (initial state : State) (action : Action) (coordinate : Fin remaining) : (policy.trajectoryKernelRemaining remaining hremaining initial) {trace | StepTrace.stateActionAt initial trace coordinate = (state, action)} = (policy.trajectoryKernelRemaining remaining hremaining initial) {trace | StepTrace.stateAt initial trace coordinate = state} * policy.actionKernel (mdp.stageOfRemainingCoordinate remaining hremaining coordinate) state {action}
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryMeasure_visitEvent_eq_stateEvent_mul_action
Compiled
The full trajectory visit event factors into its state event and action mass.
theorem trajectoryMeasure_visitEvent_eq_stateEvent_mul_action {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) : policy.trajectoryMeasure initialState {trajectory | (mdp.episodeStepOfTrajectory trajectory stage).state = state /\ (mdp.episodeStepOfTrajectory trajectory stage).action = action} = policy.trajectoryMeasure initialState {trajectory | mdp.trajectoryStateAt trajectory stage = state} * policy.actionKernel stage state {action}
def
BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageStateProbability
Compiled
Genuine state probability at one chronological stage of a generated trajectory.
noncomputable def stageStateProbability {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) : Real
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageVisitProbability_eq_stageStateProbability_mul_action
Compiled
A generated state/action visit probability is state mass times action mass.
theorem stageVisitProbability_eq_stageStateProbability_mul_action {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) : policy.stageVisitProbability initialState stage state action = policy.stageStateProbability initialState stage state * (policy.actionKernel stage state {action}).toReal