Lean module · Probability layer
BanditRLProof.ConcentrationFintypeTelescopingAllTime
# Finite-index telescoping all-time confidence union This module specializes the reusable finite-index/countable-time outer-measure union bound to the confidence schedule `delta / ((n+1)(n+2))`. Its reciprocal grows polynomially, so logarithmic confidence radii retain logarithmic time growth. The theorem only composes supplied event bounds; it is not a stochastic-process or UCB result.
Module map
Imports
BanditRLProof.ConcentrationFintypeGeometricAllTime
Imported by
BanditRLProof, BanditRLProof.ConditionalRewardPartialTrajectoryTelescopingAllTime
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_telescopingConfidenceShare
Compiled
Equal per-index telescoping shares at every time compose to the original outer confidence budget.
theorem measure_iUnion_iUnion_fintype_le_delta_of_telescopingConfidenceShare {Omega : Type u} {Idx : Type v} [MeasurableSpace Omega] [Fintype Idx] [Nonempty Idx] (mu : Measure Omega) (bad : Nat -> Idx -> Set Omega) (delta : Real) (hdelta : 0 <= delta) (hbad : forall n i, mu (bad n i) <= ENNReal.ofReal (telescopingConfidenceShare delta n / (Fintype.card Idx : Real))) : mu (⋃ n, ⋃ i, bad n i) <= ENNReal.ofReal delta