Lean module · Foundations

BanditRLProof.Algorithms.CUCBHistory

The source CUCB statistics computed from chronological triggered feedback. Index n uses exactly rounds 0,...,n-1, so its source round number is n+1. The reward coordinate is not used to estimate individual arm means.

Module map

Source: BanditRLProof/Algorithms/CUCBHistory.lean
Teaching chapter: 1. Finite bandits, traces, and regret
Declarations: 28
Placeholders: 0

Imports

No project-local imports.

Imported by

BanditRLProof, BanditRLProof.Algorithms.CUCBTrajectory

Declarations

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

abbrev BanditRLProof.CUCB.UnitOutcome Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.UnitOutcome

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

abbrev UnitOutcome

Source line 14 Chapter context: Foundations

abbrev BanditRLProof.CUCB.Feedback Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.Feedback

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

abbrev Feedback (m : ℕ)

Source line 15 Chapter context: Foundations

def BanditRLProof.CUCB.observation Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observation

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

def observation {m : ℕ} (z : Feedback m) (i : Fin m) : ℝ

Source line 17 Chapter context: Foundations

def BanditRLProof.CUCB.observationCount Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationCount

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

def observationCount {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : ℕ

Source line 20 Chapter context: Foundations

def BanditRLProof.CUCB.observationSum Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationSum

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

noncomputable def observationSum {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : ℝ

Source line 23 Chapter context: Foundations

def BanditRLProof.CUCB.empiricalMean Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.empiricalMean

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

noncomputable def empiricalMean {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : ℝ

Source line 26 Chapter context: Foundations

def BanditRLProof.CUCB.upperIndex Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.upperIndex

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

noncomputable def upperIndex {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : ℝ

Source line 29 Chapter context: Foundations

theorem BanditRLProof.CUCB.observation_nonneg Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observation_nonneg

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

theorem observation_nonneg {m : ℕ} (z : Feedback m) (i : Fin m) : 0≤observation z i

Source line 33 Chapter context: Foundations

theorem BanditRLProof.CUCB.observationCount_succ Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationCount_succ

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

theorem observationCount_succ {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : observationCount Y (n+1) i = observationCount Y n i + if (Y n).1 i then 1 else 0

Source line 40 Chapter context: Foundations

theorem BanditRLProof.CUCB.observationSum_succ Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationSum_succ

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

theorem observationSum_succ {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : observationSum Y (n+1) i = observationSum Y n i + observation (Y n) i

Source line 44 Chapter context: Foundations

theorem BanditRLProof.CUCB.observationSum_nonneg Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationSum_nonneg

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

theorem observationSum_nonneg {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : 0≤observationSum Y n i

Source line 48 Chapter context: Foundations

theorem BanditRLProof.CUCB.observationSum_le_count Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.observationSum_le_count

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

theorem observationSum_le_count {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : observationSum Y n i ≤ (observationCount Y n i : ℝ)

Source line 52 Chapter context: Foundations

theorem BanditRLProof.CUCB.empiricalMean_le_one Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.empiricalMean_le_one

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

theorem empiricalMean_le_one {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : empiricalMean Y n i ≤ 1

Source line 63 Chapter context: Foundations

theorem BanditRLProof.CUCB.empiricalMean_unobserved Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.empiricalMean_unobserved

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

theorem empiricalMean_unobserved {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) (h : (Y n).1 i=false) : empiricalMean Y (n+1) i=empiricalMean Y n i

Source line 71 Chapter context: Foundations

theorem BanditRLProof.CUCB.empiricalMean_observed Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.empiricalMean_observed

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

theorem empiricalMean_observed {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) (h : (Y n).1 i=true) : empiricalMean Y (n+1) i = (observationSum Y n i + ((Y n).2.1 i : ℝ)) / ((observationCount Y n i : ℝ)+1)

Source line 75 Chapter context: Foundations

theorem BanditRLProof.CUCB.empiricalMean_nonneg Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.empiricalMean_nonneg

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

theorem empiricalMean_nonneg {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : 0≤empiricalMean Y n i

Source line 81 Chapter context: Foundations

theorem BanditRLProof.CUCB.upperIndex_mem Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.upperIndex_mem

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

theorem upperIndex_mem {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) (i : Fin m) : upperIndex Y n i ∈ Set.Icc (0:ℝ) 1

Source line 88 Chapter context: Foundations

def BanditRLProof.CUCB.oracleInput Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.oracleInput

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

noncomputable def oracleInput {m : ℕ} (Y : ℕ → Feedback m) (n : ℕ) : Fin m → UnitOutcome

Source line 96 Chapter context: Foundations

theorem BanditRLProof.CUCB.statistics_causal Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.statistics_causal

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

theorem statistics_causal {m : ℕ} (Y Z : ℕ → Feedback m) (n : ℕ) (h : ∀t<n, Y t=Z t) (i : Fin m) : observationCount Y n i=observationCount Z n i ∧ observationSum Y n i=observationSum Z n i

Source line 99 Chapter context: Foundations

theorem BanditRLProof.CUCB.oracleInput_causal Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.oracleInput_causal

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

theorem oracleInput_causal {m : ℕ} (Y Z : ℕ → Feedback m) (n : ℕ) (h : ∀t<n, Y t=Z t) : oracleInput Y n=oracleInput Z n

Source line 111 Chapter context: Foundations

theorem BanditRLProof.CUCB.oracleInput_visible Compiled

Masked latent values and the aggregate reward cannot leak into CUCB's choice: only matching masks and matching observed arm values are needed.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.oracleInput_visible

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

theorem oracleInput_visible {m : ℕ} (Y Z : ℕ → Feedback m) (n : ℕ) (hm : ∀t<n, ∀i, (Y t).1 i=(Z t).1 i) (hx : ∀t<n, ∀i, (Y t).1 i=true → (Y t).2.1 i=(Z t).2.1 i) : oracleInput Y n=oracleInput Z n

Source line 120 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_observation Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_observation

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

theorem measurable_observation {m : ℕ} (i : Fin m) : Measurable (fun z : Feedback m => observation z i)

Source line 139 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_observationCount Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_observationCount

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

theorem measurable_observationCount {m : ℕ} (n : ℕ) (i : Fin m) : Measurable (fun Y : ℕ → Feedback m => observationCount Y n i)

Source line 146 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_observationCount_real Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_observationCount_real

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

theorem measurable_observationCount_real {m : ℕ} (n : ℕ) (i : Fin m) : Measurable (fun Y : ℕ → Feedback m => (observationCount Y n i : ℝ))

Source line 154 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_observationSum Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_observationSum

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

theorem measurable_observationSum {m : ℕ} (n : ℕ) (i : Fin m) : Measurable (fun Y : ℕ → Feedback m => observationSum Y n i)

Source line 158 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_empiricalMean Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_empiricalMean

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

theorem measurable_empiricalMean {m : ℕ} (n : ℕ) (i : Fin m) : Measurable (fun Y : ℕ → Feedback m => empiricalMean Y n i)

Source line 165 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_upperIndex Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_upperIndex

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

theorem measurable_upperIndex {m : ℕ} (n : ℕ) (i : Fin m) : Measurable (fun Y : ℕ → Feedback m => upperIndex Y n i)

Source line 171 Chapter context: Foundations

theorem BanditRLProof.CUCB.measurable_oracleInput Compiled

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

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.CUCB.measurable_oracleInput

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

theorem measurable_oracleInput {m : ℕ} (n : ℕ) : Measurable (fun Y : ℕ → Feedback m => oracleInput Y n)

Source line 179 Chapter context: Foundations