Lean module · Probability layer
BanditRLProof.ProbabilityUnionBound
# Finite union probability bounds Thin Mathlib-backed finite-union wrappers. These are outer-measure bounds: no event measurability or probability-measure assumption is required.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.Algorithms.UCB, BanditRLProof.Algorithms.UCBFixedCountPeeling, BanditRLProof.ConcentrationFintypeGeometricAllTime, BanditRLProof.ConcentrationQuadraticMaximal, BanditRLProof.ConcentrationSubGaussian, BanditRLProof.DelayedFeedback.StochasticGoodEvent, BanditRLProof.DelayedFeedback.StochasticGoodEventAssembly, BanditRLProof.OFULUniformTimeConfidence, BanditRLProof.RL.FiniteHorizonAdaptiveCumulativeUCBVISimultaneousConfidence, BanditRLProof.RL.FiniteHorizonIIDMultiBatchCumulativeConfidenceRegret, BanditRLProof.RL.FiniteHorizonIIDSimultaneousCountConfidence, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeHighProbabilityAverageRealizedBehaviorRegret, BanditRLProof.UCBSummability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.ProbabilityUnionBound.measure_biUnion_finset_le
Compiled
The measure of a finite union of events is bounded by the finite sum of their measures. This is an outer-measure wrapper around `MeasureTheory.measure_biUnion_finset_le`, so it does not require the events to be measurable and does not require `mu` to be a probability measure.
theorem measure_biUnion_finset_le {Omega : Type u} [MeasurableSpace Omega] {Idx : Type v} (mu : Measure Omega) (s : Finset Idx) (E : Idx -> Set Omega) : mu (⋃ i ∈ s, E i) <= s.sum (fun i => mu (E i))
theorem
BanditRLProof.ProbabilityUnionBound.measure_biUnion_finset_le_of_uniform
Compiled
Equal-share finite-union bound. Every event receives confidence budget `delta / s.card`; nonemptiness of the index set lets the finite sum normalize back to `delta`. As with `measure_biUnion_finset_le`, no event measurability or probability-measure assumption is required.
theorem measure_biUnion_finset_le_of_uniform {Omega : Type u} [MeasurableSpace Omega] {Idx : Type v} [DecidableEq Idx] (mu : Measure Omega) (s : Finset Idx) (hs : s.Nonempty) (delta : Real) (E : Idx -> Set Omega) (hE : forall i, i ∈ s -> mu (E i) <= ENNReal.ofReal (delta / (s.card : Real))) : mu (⋃ i ∈ s, E i) <= ENNReal.ofReal delta
theorem
BanditRLProof.ProbabilityUnionBound.measure_iUnion_fintype_le_sum
Compiled
Fintype specialization of the finite-union probability bound. The index set is `(Finset.univ : Finset Idx)`, matching the finite-arm style used by the bandit proofs.
theorem measure_iUnion_fintype_le_sum {Omega : Type u} [MeasurableSpace Omega] {Idx : Type v} [Fintype Idx] (mu : Measure Omega) (E : Idx -> Set Omega) : mu (⋃ i, E i) <= (Finset.univ : Finset Idx).sum (fun i => mu (E i))