Lean module · Probability layer

BanditRLProof.ConcentrationFintypeGeometricAllTime

# Finite-index geometric all-time confidence This module composes two already-compiled outer-measure adapters: a finite equal-share union at each time and a countable geometric schedule over time. It is deliberately only a confidence-budget composition theorem. It does not produce the per-index tails and is not a Ville/Doob, mixture, optional-stopping, self-normalized, or general Freedman inequality.

Module map

Source: BanditRLProof/ConcentrationFintypeGeometricAllTime.lean
Teaching chapter: 2. Probability, kernels, filtrations, and concentration
Declarations: 2
Placeholders: 0

Imports

BanditRLProof.ConcentrationConfidenceSchedule, BanditRLProof.ProbabilityUnionBound

Imported by

BanditRLProof, BanditRLProof.ConcentrationFintypeTelescopingAllTime, BanditRLProof.ConditionalRewardPartialTrajectoryGeometricAllTime

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_tsum_of_uniform Compiled

A countable family of finite-index bad events is controlled by the sum of its per-time budgets when every index receives an equal share. No event measurability or probability-measure assumption is required.

theorem measure_iUnion_iUnion_fintype_le_tsum_of_uniform {Omega : Type u} {Idx : Type v} [MeasurableSpace Omega] [Fintype Idx] [Nonempty Idx] (mu : Measure Omega) (bad : Nat -> Idx -> Set Omega) (deltaAt : Nat -> Real) (hbad : forall n i, mu (bad n i) <= ENNReal.ofReal (deltaAt n / (Fintype.card Idx : Real))) : mu (⋃ n, ⋃ i, bad n i) <= ∑' n, ENNReal.ofReal (deltaAt n)

Source line 24 Chapter context: Probability layer

theorem BanditRLProof.Concentration.measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare Compiled

Equal sharing across a nonempty finite index type at every time, followed by the geometric schedule over time, gives one all-time outer confidence budget. No event measurability or probability-measure assumption is required.

theorem measure_iUnion_iUnion_fintype_le_delta_of_geometricConfidenceShare {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 (geometricConfidenceShare delta n / (Fintype.card Idx : Real))) : mu (⋃ n, ⋃ i, bad n i) <= ENNReal.ofReal delta

Source line 50 Open teaching explanation Chapter context: Probability layer