Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonStageTransitionJointFactorization
# Generated stage-transition joint-law factorization This module proves that a fixed generated trajectory-stage joint transition mass factors into its state-action visit mass and the true MDP transition kernel singleton mass. The proof follows the recursive finite trajectory kernel; it does not divide by visit probabilities or introduce empirical confidence.
Module map
Imports
BanditRLProof.RL.FiniteHorizonIIDCountConcentration
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISameSourceConfidence, BanditRLProof.RL.FiniteHorizonIIDEligibleEmpiricalTransitionConfidence, BanditRLProof.RL.FiniteHorizonStageVisitFactorization
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.StepTrace.stateAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def stateAt : {n : Nat} -> State -> StepTrace Action State n -> Fin n -> State | 0, _initial, _trace, coordinate => Fin.elim0 coordinate | _n + 1, initial, trace, coordinate => Fin.cases initial (fun previous => (trace previous.castSucc).2) coordinate @[simp] theorem stateAt_zero (initial : State) (head : Action × State) (tail : StepTrace Action State n) : stateAt initial (Fin.cons head tail) (0 : Fin (n + 1)) = initial
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateAt_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateAt_zero (initial : State) (head : Action × State) (tail : StepTrace Action State n) : stateAt initial (Fin.cons head tail) (0 : Fin (n + 1)) = initial
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateAt_zero_apply
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateAt_zero_apply (initial : State) (trace : StepTrace Action State (n + 1)) : stateAt initial trace (0 : Fin (n + 1)) = initial
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateAt_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateAt_succ (initial : State) (head : Action × State) (tail : StepTrace Action State n) (coordinate : Fin n) : stateAt initial (Fin.cons head tail) coordinate.succ = stateAt head.2 tail coordinate
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateAt_eq_if
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateAt_eq_if {n : Nat} (initial : State) (trace : StepTrace Action State n) (coordinate : Fin n) : stateAt initial trace coordinate = if _hzero : coordinate.val = 0 then initial else (trace ⟨coordinate.val - 1, by omega⟩).2
def
BanditRLProof.FiniteHorizonRL.StepTrace.stateActionAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def stateActionAt {n : Nat} (initial : State) (trace : StepTrace Action State n) (coordinate : Fin n) : State × Action
def
BanditRLProof.FiniteHorizonRL.StepTrace.stateActionNextAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
def stateActionNextAt {n : Nat} (initial : State) (trace : StepTrace Action State n) (coordinate : Fin n) : (State × Action) × State
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateActionAt_cons_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateActionAt_cons_succ (initial : State) (head : Action × State) (tail : StepTrace Action State n) (coordinate : Fin n) : stateActionAt initial (Fin.cons head tail) coordinate.succ = stateActionAt head.2 tail coordinate
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.stateActionNextAt_cons_succ
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stateActionNextAt_cons_succ (initial : State) (head : Action × State) (tail : StepTrace Action State n) (coordinate : Fin n) : stateActionNextAt initial (Fin.cons head tail) coordinate.succ = stateActionNextAt head.2 tail coordinate
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.measurable_stateActionAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_stateActionAt {n : Nat} (initial : State) (coordinate : Fin n) : Measurable (fun trace : StepTrace Action State n => stateActionAt initial trace coordinate)
theorem
BanditRLProof.FiniteHorizonRL.StepTrace.measurable_stateActionNextAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_stateActionNextAt {n : Nat} (initial : State) (coordinate : Fin n) : Measurable (fun trace : StepTrace Action State n => stateActionNextAt initial trace coordinate)
theorem
BanditRLProof.FiniteHorizonRL.MDP.stepTrace_stateAt_eq_trajectoryStateAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stepTrace_stateAt_eq_trajectoryStateAt (mdp : MDP State Action) (trajectory : State × StepTrace Action State mdp.horizon) (stage : Fin mdp.horizon) : StepTrace.stateAt trajectory.1 trajectory.2 stage = mdp.trajectoryStateAt trajectory stage
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.actionStateKernel_apply_singleton
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem actionStateKernel_apply_singleton {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.actionStateKernel stage state {(action, nextState)} = policy.actionKernel stage state {action} * mdp.transition (state, action) {nextState}
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.actionStateKernel_apply_actionSet
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem actionStateKernel_apply_actionSet {mdp : MDP State Action} (policy : MarkovPolicy mdp) (stage : Fin mdp.horizon) (state : State) (action : Action) : policy.actionStateKernel stage state ({action} ×ˢ Set.univ) = policy.actionKernel stage state {action}
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryKernelRemaining_map_head
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem trajectoryKernelRemaining_map_head {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining + 1 <= mdp.horizon) (initial : State) : (policy.trajectoryKernelRemaining (remaining + 1) hremaining initial).map (fun trace => trace 0) = policy.actionStateKernel ⟨mdp.horizon - (remaining + 1), by omega⟩ initial
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryKernelRemaining_transitionEvent_eq_visitEvent_mul
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem trajectoryKernelRemaining_transitionEvent_eq_visitEvent_mul {mdp : MDP State Action} (policy : MarkovPolicy mdp) (remaining : Nat) (hremaining : remaining <= mdp.horizon) (initial state : State) (action : Action) (nextState : State) (coordinate : Fin remaining) : (policy.trajectoryKernelRemaining remaining hremaining initial) {trace | StepTrace.stateActionNextAt initial trace coordinate = ((state, action), nextState)} = (policy.trajectoryKernelRemaining remaining hremaining initial) {trace | StepTrace.stateActionAt initial trace coordinate = (state, action)} * mdp.transition (state, action) {nextState}
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.trajectoryMeasure_transitionEvent_eq_visitEvent_mul
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem trajectoryMeasure_transitionEvent_eq_visitEvent_mul {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.trajectoryMeasure initialState {trajectory | StepTrace.stateActionNextAt trajectory.1 trajectory.2 stage = ((state, action), nextState)} = policy.trajectoryMeasure initialState {trajectory | StepTrace.stateActionAt trajectory.1 trajectory.2 stage = (state, action)} * mdp.transition (state, action) {nextState}
theorem
BanditRLProof.FiniteHorizonRL.MarkovPolicy.stageTransitionJointProbability_eq_stageVisitProbability_mul_transition
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem stageTransitionJointProbability_eq_stageVisitProbability_mul_transition [DecidableEq State] [DecidableEq Action] {mdp : MDP State Action} (policy : MarkovPolicy mdp) (initialState : Measure State) [IsProbabilityMeasure initialState] (stage : Fin mdp.horizon) (state : State) (action : Action) (nextState : State) : policy.stageTransitionJointProbability initialState stage state action nextState = policy.stageVisitProbability initialState stage state action * (mdp.transition (state, action) {nextState}).toReal