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

Lean module · UCB

BanditRLProof.Algorithms.UCBRealHistoryIndex

This module mirrors the path-dependent score used by the pinned LML UCB route. In particular, the confidence width divides by the realized pull count. It is therefore distinct from the earlier UCB surface whose proxy is deterministic in the sample point.

Module map

Declarations
22
Placeholders
0

Imports

BanditRLProof.Algorithms.UCB, BanditRLProof.Algorithms.ETCRealHistoryScore, BanditRLProof.MeasurableLocalQuantities, BanditRLProof.MeasurablePullCountCast

Imported by

BanditRLProof, BanditRLProof.Algorithms.MOSSHistory, BanditRLProof.Algorithms.ThompsonClippedUCBScore, BanditRLProof.Algorithms.UCBFixedCountPeeling

Declarations

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

def BanditRLProof.UCB.realEmpiricalMean Compiled

Real empirical mean of one arm before time `n`.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realEmpiricalMean

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

noncomputable def realEmpiricalMean {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (arm : Fin K) (n : Nat) : Real
Source line 19 Chapter context: UCB
def BanditRLProof.UCB.realWidth Compiled

LML-shaped path-dependent UCB width before time `n`.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realWidth

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

noncomputable def realWidth {K : Nat} (action : ActionTrace (Fin K)) (c : Real) (arm : Fin K) (n : Nat) : Real
Source line 25 Chapter context: UCB
def BanditRLProof.UCB.realIndex Compiled

Real empirical mean plus the realized pull-count confidence width.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realIndex

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

noncomputable def realIndex {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (arm : Fin K) (n : Nat) : Real
Source line 33 Chapter context: UCB
def BanditRLProof.UCB.realHistoryWidth Compiled

Inclusive finite-history version of the LML UCB width.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryWidth

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

noncomputable def realHistoryWidth {K : Nat} (c : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real
Source line 39 Chapter context: UCB
def BanditRLProof.UCB.realHistoryIndex Compiled

Inclusive finite-history Real UCB score.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryIndex

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

noncomputable def realHistoryIndex {K : Nat} (c : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) (arm : Fin K) : Real
Source line 48 Chapter context: UCB
def BanditRLProof.UCB.realIndexAction Compiled

Least-encoded maximizer of the path-dependent Real UCB index.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realIndexAction

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

noncomputable def realIndexAction {K : Nat} (hK : 0 < K) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (n : Nat) : Fin K
Source line 56 Chapter context: UCB
def BanditRLProof.UCB.realHistoryIndexAction Compiled

Least-encoded maximizer on an inclusive finite pair history.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryIndexAction

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

noncomputable def realHistoryIndexAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) (history : History.FinitePairHistory (Fin K) Real n) : Fin K
Source line 64 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistoryPullCount Compiled

A fixed-arm pull count is measurable as a function of finite pair history.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistoryPullCount

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

theorem measurable_realHistoryPullCount {K : Nat} (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => ETC.realHistoryPullCount n history arm)
Source line 71 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistorySumRewards Compiled

A fixed-arm reward sum is measurable as a function of finite pair history.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistorySumRewards

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

theorem measurable_realHistorySumRewards {K : Nat} (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => ETC.realHistorySumRewards n history arm)
Source line 85 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistoryEmpMean Compiled

A fixed-arm empirical mean is measurable on finite pair histories.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistoryEmpMean

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

theorem measurable_realHistoryEmpMean {K : Nat} (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => ETC.realHistoryEmpMean n history arm)
Source line 99 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistoryWidth Compiled

The fixed-arm UCB width is measurable on finite pair histories.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistoryWidth

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

theorem measurable_realHistoryWidth {K : Nat} (c : Real) (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => realHistoryWidth c n history arm)
Source line 109 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistoryIndex Compiled

Every fixed-arm UCB score is measurable on finite pair histories.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistoryIndex

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

theorem measurable_realHistoryIndex {K : Nat} (c : Real) (n : Nat) (arm : Fin K) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => realHistoryIndex c n history arm)
Source line 119 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realHistoryIndexAction Compiled

The least-encoded finite-history UCB selector is measurable.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realHistoryIndexAction

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

theorem measurable_realHistoryIndexAction {K : Nat} (hK : 0 < K) (c : Real) (n : Nat) : Measurable (fun history : History.FinitePairHistory (Fin K) Real n => realHistoryIndexAction hK c n history)
Source line 127 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realEmpiricalMean Compiled

The trace empirical mean is measurable under timewise measurable data.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realEmpiricalMean

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

theorem measurable_realEmpiricalMean {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSingletonClass (Fin K)] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (arm : Fin K) (n : Nat) : Measurable (fun omega => realEmpiricalMean (action omega) (reward omega) arm n)
Source line 138 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realWidth Compiled

The realized pull-count UCB width is measurable.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realWidth

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

theorem measurable_realWidth {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSingletonClass (Fin K)] (action : Omega -> ActionTrace (Fin K)) (haction : forall t, Measurable (fun omega => action omega t)) (c : Real) (arm : Fin K) (n : Nat) : Measurable (fun omega => realWidth (action omega) c arm n)
Source line 153 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realIndex Compiled

Every coordinate of the realized UCB index is measurable.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realIndex

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

theorem measurable_realIndex {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSingletonClass (Fin K)] (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (c : Real) (arm : Fin K) (n : Nat) : Measurable (fun omega => realIndex (action omega) (reward omega) c arm n)
Source line 166 Chapter context: UCB
theorem BanditRLProof.UCB.realIndexAction_spec Compiled

The least-encoded realized UCB index action maximizes every arm score.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realIndexAction_spec

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

theorem realIndexAction_spec {K : Nat} (hK : 0 < K) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (n : Nat) (arm : Fin K) : realIndex action reward c arm n <= realIndex action reward c (realIndexAction hK action reward c n) n
Source line 180 Chapter context: UCB
theorem BanditRLProof.UCB.measurable_realIndexAction Compiled

The least-encoded realized UCB index action is measurable.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.measurable_realIndexAction

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

theorem measurable_realIndexAction {Omega : Type u} {K : Nat} [MeasurableSpace Omega] [MeasurableSingletonClass (Fin K)] (hK : 0 < K) (action : Omega -> ActionTrace (Fin K)) (reward : Omega -> RewardTrace Real) (haction : forall t, Measurable (fun omega => action omega t)) (hreward : forall t, Measurable (fun omega => reward omega t)) (c : Real) (n : Nat) : Measurable (fun omega => realIndexAction hK (action omega) (reward omega) c n)
Source line 191 Chapter context: UCB
theorem BanditRLProof.UCB.realHistoryEmpiricalMean_finitePairHistoryOfTrace Compiled

Inclusive finite-history empirical means agree with the trace prefix.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryEmpiricalMean_finitePairHistoryOfTrace

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

theorem realHistoryEmpiricalMean_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (n : Nat) (arm : Fin K) : ETC.realHistoryEmpMean n (History.finitePairHistoryOfTrace action reward n) arm = realEmpiricalMean action reward arm (n + 1)
Source line 207 Chapter context: UCB
theorem BanditRLProof.UCB.realHistoryWidth_finitePairHistoryOfTrace Compiled

Inclusive finite-history widths agree with the trace width at `n + 1`.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryWidth_finitePairHistoryOfTrace

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

theorem realHistoryWidth_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (n : Nat) (arm : Fin K) : realHistoryWidth c n (History.finitePairHistoryOfTrace action reward n) arm = realWidth action c arm (n + 1)
Source line 216 Chapter context: UCB
theorem BanditRLProof.UCB.realHistoryIndex_finitePairHistoryOfTrace Compiled

Inclusive finite-history UCB scores agree with the trace score.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryIndex_finitePairHistoryOfTrace

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

theorem realHistoryIndex_finitePairHistoryOfTrace {K : Nat} (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (n : Nat) (arm : Fin K) : realHistoryIndex c n (History.finitePairHistoryOfTrace action reward n) arm = realIndex action reward c arm (n + 1)
Source line 226 Chapter context: UCB
theorem BanditRLProof.UCB.realHistoryIndexAction_finitePairHistoryOfTrace Compiled

The least-encoded history selector is exactly the trace selector.

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

4. UCB: confidence events to regret

Canonical node identitydeclaration:BanditRLProof.UCB.realHistoryIndexAction_finitePairHistoryOfTrace

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

theorem realHistoryIndexAction_finitePairHistoryOfTrace {K : Nat} (hK : 0 < K) (action : ActionTrace (Fin K)) (reward : RewardTrace Real) (c : Real) (n : Nat) : realHistoryIndexAction hK c n (History.finitePairHistoryOfTrace action reward n) = realIndexAction hK action reward c (n + 1)
Source line 237 Chapter context: UCB