Lean module · Finite-horizon RL
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAggregateTransition
# Cross-stage cumulative transition rows for UCBVI-CH UCBVI-CH pools every visit of a state-action pair across stages. The earlier foundation exposed the aggregate denominator `N_k(x,a)` but retained only the stage-indexed transition numerator. This module closes that structural gap: it defines `N_k(x,a,y)`, proves that its row sum is exactly the aggregate visit count, proves exact generated-prefix and successor identities, and normalizes the row into a probability kernel with an explicit Dirac fallback at zero. No concentration or regret conclusion is asserted here.
Module map
Imports
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeHoeffdingUCBVI
Imported by
BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIClippedPlanner
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateTransitionCount
Compiled
The UCBVI-CH numerator `N_k(x,a,y)`, pooled across every decision stage.
def aggregateTransitionCount {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (state : State) (action : Action) (nextState : State) : Nat
theorem
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.measurable_aggregateTransitionCount
Compiled
The complete pooled transition-count table is measurable.
theorem measurable_aggregateTransitionCount {mdp : MDP State Action} : Measurable fun summary : TransitionCountSummary mdp => fun state action nextState => summary.aggregateTransitionCount state action nextState
theorem
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.sum_aggregateTransitionCount_eq_aggregateVisitCount
Compiled
Pooling transition destinations gives exactly the pooled visit count.
theorem sum_aggregateTransitionCount_eq_aggregateVisitCount {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (state : State) (action : Action) : (∑ nextState : State, summary.aggregateTransitionCount state action nextState) = summary.aggregateVisitCount state action
def
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF
Compiled
The normalized pooled empirical row, with a Dirac fallback at zero visits.
noncomputable def aggregateEmpiricalTransitionPMF {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (state : State) (action : Action) : PMF State
theorem
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_of_aggregateVisitCount_eq_zero
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem aggregateEmpiricalTransitionPMF_of_aggregateVisitCount_eq_zero {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (state : State) (action : Action) (hzero : summary.aggregateVisitCount state action = 0) : summary.aggregateEmpiricalTransitionPMF defaultState state action = PMF.pure defaultState
theorem
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_apply_of_aggregateVisitCount_pos
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem aggregateEmpiricalTransitionPMF_apply_of_aggregateVisitCount_pos {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (state : State) (action : Action) (nextState : State) (hpos : 0 < summary.aggregateVisitCount state action) : summary.aggregateEmpiricalTransitionPMF defaultState state action nextState = (summary.aggregateTransitionCount state action nextState : ENNReal) / (summary.aggregateVisitCount state action : ENNReal)
def
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel
Compiled
The pooled empirical transition kernel is stage-homogeneous.
noncomputable def aggregateEmpiricalTransitionKernel {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) : ProbabilityTheory.Kernel (State × Action) State
theorem
BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel_isMarkov
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem aggregateEmpiricalTransitionKernel_isMarkov {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) : ProbabilityTheory.IsMarkovKernel (summary.aggregateEmpiricalTransitionKernel defaultState) where
def
BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt
Compiled
The pooled transition numerator through one generated trajectory prefix.
def adaptiveCumulativeAggregateTransitionCountAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) (nextState : State) : Nat
theorem
BanditRLProof.FiniteHorizonRL.measurable_adaptiveCumulativeAggregateTransitionCountAt
Compiled
No declaration docstring is present; use the chapter context and exact statement below.
theorem measurable_adaptiveCumulativeAggregateTransitionCountAt {mdp : MDP State Action} {episodes : Nat} (round : Nat) (state : State) (action : Action) (nextState : State) : Measurable fun trajectory : EpisodeBatchTrajectory mdp episodes => adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState
theorem
BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_eq_sum
Compiled
The pooled numerator is the literal episode-by-stage generated count.
theorem adaptiveCumulativeAggregateTransitionCountAt_eq_sum {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) (nextState : State) : adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState = ∑ i : Fin (round + 1), ∑ stage : Fin mdp.horizon, (trajectory i).transitionCount stage state action nextState
theorem
BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_succ
Compiled
Extending the prefix adds exactly one episode's pooled transition row.
theorem adaptiveCumulativeAggregateTransitionCountAt_succ {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) (nextState : State) : adaptiveCumulativeAggregateTransitionCountAt trajectory (round + 1) state action nextState = adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState + ∑ stage : Fin mdp.horizon, (trajectory (round + 1)).transitionCount stage state action nextState
theorem
BanditRLProof.FiniteHorizonRL.sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt
Compiled
At every generated prefix the pooled numerator row sums to the denominator.
theorem sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) : (∑ nextState : State, adaptiveCumulativeAggregateTransitionCountAt trajectory round state action nextState) = adaptiveCumulativeAggregateVisitCountAt trajectory round state action