Lean module · UCB
BanditRLProof.UCBSummability
This file records the finite-union/summation layer used by UCB-style bad events: once each arm-time event has a tail bound, the bad-event union over finite arms and a finite horizon is bounded by the corresponding double sum.
Module map
Imports
BanditRLProof.ProbabilityUnionBound
Imported by
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.UCBSummability.finiteHorizonBadEvent
Compiled
The union of arm-time bad events over all finite arms and times `< T`.
Used in these reading views: Bandit Book · Reinforcement Learning Book
4. UCB: confidence events to regret
Canonical node identity
declaration:BanditRLProof.UCBSummability.finiteHorizonBadEventReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
def finiteHorizonBadEvent {Omega : Type u} {Arm : Type v} (bad : Arm -> Nat -> Set Omega) (T : Nat) : Set Omega
theorem
BanditRLProof.UCBSummability.measure_finiteHorizonBadEvent_le_sum
Compiled
Finite-horizon union bound for a UCB-style arm-time bad-event family. No event measurability is required: this is an outer-measure bound inherited from Mathlib's finite-union measure inequality.
Used in these reading views: Bandit Book · Reinforcement Learning Book
4. UCB: confidence events to regret
Canonical node identity
declaration:BanditRLProof.UCBSummability.measure_finiteHorizonBadEvent_le_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measure_finiteHorizonBadEvent_le_sum {Omega : Type u} [MeasurableSpace Omega] {Arm : Type v} [Fintype Arm] (mu : Measure Omega) (bad : Arm -> Nat -> Set Omega) (T : Nat) : mu (finiteHorizonBadEvent bad T) <= (Finset.univ : Finset Arm).sum (fun a => (Finset.range T).sum (fun t => mu (bad a t)))
theorem
BanditRLProof.UCBSummability.measure_finiteHorizonBadEvent_le_tail_sum
Compiled
Tail-bound consumer for finite-horizon UCB bad events. The hypothesis `htail` is the per-arm/per-time concentration result; this wrapper only assembles those local bounds into the finite bad-event sum.
Used in these reading views: Bandit Book · Reinforcement Learning Book
4. UCB: confidence events to regret
Canonical node identity
declaration:BanditRLProof.UCBSummability.measure_finiteHorizonBadEvent_le_tail_sumReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem measure_finiteHorizonBadEvent_le_tail_sum {Omega : Type u} [MeasurableSpace Omega] {Arm : Type v} [Fintype Arm] (mu : Measure Omega) (bad : Arm -> Nat -> Set Omega) (tail : Arm -> Nat -> ENNReal) (T : Nat) (htail : forall a t, t < T -> mu (bad a t) <= tail a t) : mu (finiteHorizonBadEvent bad T) <= (Finset.univ : Finset Arm).sum (fun a => (Finset.range T).sum (fun t => tail a t))