BanditRLlib
Lean gate passed before this site build; local proof declarations are shown as compiled.

Lean module · UCB

BanditRLProof.Algorithms.UCBRealHistoryIndex

# Native Real UCB history index 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.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`.

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`.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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.

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`.

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.

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.

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