BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.Lean-verified build · exact declarations linked.

Lean module · Finite-horizon RL

BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVIAggregateTransition

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.

Module map

Declarations
13
Placeholders
0

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.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateTransitionCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

def aggregateTransitionCount {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (state : State) (action : Action) (nextState : State) : Nat
Source line 33 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.measurable_aggregateTransitionCount Compiled

The complete pooled transition-count table is measurable.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.measurable_aggregateTransitionCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem measurable_aggregateTransitionCount {mdp : MDP State Action} : Measurable fun summary : TransitionCountSummary mdp => fun state action nextState => summary.aggregateTransitionCount state action nextState
Source line 42 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.sum_aggregateTransitionCount_eq_aggregateVisitCount Compiled

Pooling transition destinations gives exactly the pooled visit count.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.sum_aggregateTransitionCount_eq_aggregateVisitCount

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 57 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF Compiled

The normalized pooled empirical row, with a Dirac fallback at zero visits.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def aggregateEmpiricalTransitionPMF {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) (state : State) (action : Action) : PMF State
Source line 68 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_of_aggregateVisitCount_eq_zero Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_of_aggregateVisitCount_eq_zero

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 103 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_apply_of_aggregateVisitCount_pos Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionPMF_apply_of_aggregateVisitCount_pos

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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)
Source line 111 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel Compiled

The pooled empirical transition kernel is stage-homogeneous.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

noncomputable def aggregateEmpiricalTransitionKernel {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) : ProbabilityTheory.Kernel (State × Action) State
Source line 121 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel_isMarkov Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.TransitionCountSummary.aggregateEmpiricalTransitionKernel_isMarkov

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

theorem aggregateEmpiricalTransitionKernel_isMarkov {mdp : MDP State Action} (summary : TransitionCountSummary mdp) (defaultState : State) : ProbabilityTheory.IsMarkovKernel (summary.aggregateEmpiricalTransitionKernel defaultState) where
Source line 128 Chapter context: Finite-horizon RL
def BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt Compiled

The pooled transition numerator through one generated trajectory prefix.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

def adaptiveCumulativeAggregateTransitionCountAt {mdp : MDP State Action} {episodes : Nat} (trajectory : EpisodeBatchTrajectory mdp episodes) (round : Nat) (state : State) (action : Action) (nextState : State) : Nat
Source line 142 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.measurable_adaptiveCumulativeAggregateTransitionCountAt Compiled

No declaration docstring is present; use the chapter context and exact statement below.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.measurable_adaptiveCumulativeAggregateTransitionCountAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 150 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_eq_sum Compiled

The pooled numerator is the literal episode-by-stage generated count.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_eq_sum

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 166 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_succ Compiled

Extending the prefix adds exactly one episode's pooled transition row.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.adaptiveCumulativeAggregateTransitionCountAt_succ

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 186 Chapter context: Finite-horizon RL
theorem BanditRLProof.FiniteHorizonRL.sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt Compiled

At every generated prefix the pooled numerator row sums to the denominator.

Used in these reading views: Bandit Book · Reinforcement Learning Book

9. Finite-horizon reinforcement learning

Canonical node identitydeclaration:BanditRLProof.FiniteHorizonRL.sum_adaptiveCumulativeAggregateTransitionCountAt_eq_visitCountAt

Reading membership is not a proof dependency. Exact assumptions remain in the Lean statement.

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
Source line 205 Open teaching explanation Chapter context: Finite-horizon RL