Lean module · Foundations

BanditRLProof.Algorithms.HeavyTailUCB

Causal robust UCB with the audited conservative confidence schedule. Time is zero-based; the logarithm uses max(t,2), and failure probability t^-4 is the explicit repair recorded in DERIVATION.md. No regret endpoint is claimed here.

Module map

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

Imports

BanditRLProof.Algorithms.HeavyTailHistory

Imported by

BanditRLProof, BanditRLProof.HeavyTailTuning

Declarations

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

def BanditRLProof.HeavyTail.confidenceLog 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.HeavyTail.confidenceLog

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

noncomputable def confidenceLog (t : ℕ) : ℝ

Source line 10 Chapter context: Foundations

def BanditRLProof.HeavyTail.sampleThreshold 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.HeavyTail.sampleThreshold

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

noncomputable def sampleThreshold (ε u : ℝ) (t s : ℕ) : ℝ

Source line 12 Chapter context: Foundations

def BanditRLProof.HeavyTail.confidenceRadius 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.HeavyTail.confidenceRadius

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

noncomputable def confidenceRadius (ε u : ℝ) (t count : ℕ) : ℝ

Source line 15 Chapter context: Foundations

def BanditRLProof.HeavyTail.historyIndex 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.HeavyTail.historyIndex

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

noncomputable def historyIndex (initial : Fin K) (ε u : ℝ) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) (arm : Fin K) : ℝ

Source line 18 Chapter context: Foundations

def BanditRLProof.HeavyTail.nextArm 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.HeavyTail.nextArm

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

noncomputable def nextArm (hK : 0 < K) (ε u : ℝ) (n : ℕ) (h : History.FinitePairHistory (Fin K) ℝ n) : Fin K

Source line 23 Chapter context: Foundations

theorem BanditRLProof.HeavyTail.measurable_historyIndex 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.HeavyTail.measurable_historyIndex

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

theorem measurable_historyIndex (initial : Fin K) (ε u : ℝ) (n : ℕ) (arm : Fin K) : Measurable (fun h => historyIndex initial ε u n h arm)

Source line 28 Chapter context: Foundations

theorem BanditRLProof.HeavyTail.measurable_nextArm 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.HeavyTail.measurable_nextArm

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

theorem measurable_nextArm (hK : 0 < K) (ε u : ℝ) (n : ℕ) : Measurable (nextArm hK ε u n)

Source line 35 Chapter context: Foundations

def BanditRLProof.HeavyTail.robustAction 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.HeavyTail.robustAction

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

noncomputable def robustAction (hK : 0 < K) (ε u : ℝ)

Source line 45 Chapter context: Foundations

def BanditRLProof.HeavyTail.robustReward 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.HeavyTail.robustReward

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

noncomputable def robustReward (hK : 0 < K) (ε u : ℝ)

Source line 48 Chapter context: Foundations

theorem BanditRLProof.HeavyTail.measurable_robustAction 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.HeavyTail.measurable_robustAction

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

theorem measurable_robustAction (hK : 0 < K) (ε u : ℝ) (t : ℕ) : Measurable (fun stream => robustAction hK ε u stream t)

Source line 51 Chapter context: Foundations

theorem BanditRLProof.HeavyTail.robustAction_initialization 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.HeavyTail.robustAction_initialization

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

theorem robustAction_initialization (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (t : ℕ) (ht : t < K) : robustAction hK ε u stream t = UCB.initializationArm hK t

Source line 55 Chapter context: Foundations

theorem BanditRLProof.HeavyTail.robustAction_maximizes Compiled

The selected index is maximal on the actual observed history.

Used in these reading views: Bandit Book

1. Finite bandits, traces, and regret

Canonical node identity

declaration:BanditRLProof.HeavyTail.robustAction_maximizes

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

theorem robustAction_maximizes (hK : 0 < K) (ε u : ℝ) (stream : UCB.ArmRewardStream K) (n : ℕ) (hn : K ≤ n+1) (arm : Fin K) : let h := ArmStreamPolicy.history (UCB.initializationArm hK 0) (nextArm hK ε u) stream n historyIndex (UCB.initializationArm hK 0) ε u n h arm ≤ historyIndex (UCB.initializationArm hK 0) ε u n h (robustAction hK ε u stream (n+1))

Source line 63 Chapter context: Foundations