Lean module · UCB
BanditRLProof.UCBSummability
# Finite-horizon UCB tail summability wrappers 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`.
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.
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.
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))