Lean module · Probability layer
BanditRLProof.ConcentrationQuadraticMaximal
# Finite maximal quadratic fixed-MGF tails This module adds a finite-index maximal surface to the quadratic fixed-MGF route. It uses equal confidence shares and the finite outer-measure union bound; it is not a Ville, Doob, or infinite-horizon maximal inequality.
Module map
Imports
BanditRLProof.ConcentrationQuadraticFixedMGF, BanditRLProof.ProbabilityUnionBound
Imported by
BanditRLProof, BanditRLProof.Exp3RealizedPredictableVarianceMaximal
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
def
BanditRLProof.Concentration.quadraticFixedMGFMaximalRadius
Compiled
Equal-share quadratic radius for a finite family of events.
noncomputable def quadraticFixedMGFMaximalRadius {Idx : Type*} [DecidableEq Idx] (times : Finset Idx) (varianceScale varianceBudget tiltCap delta : Real) : Real
theorem
BanditRLProof.Concentration.measure_biUnion_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail
Compiled
Finite maximal delta tail obtained by optimizing every fixed-tilt event at confidence `delta / times.card` and taking the finite union.
theorem measure_biUnion_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail {Omega Idx : Type*} [MeasurableSpace Omega] [DecidableEq Idx] (mu : Measure Omega) (times : Finset Idx) (htimes : times.Nonempty) (deviation predictableVariance : Idx -> Omega -> Real) (varianceScale varianceBudget tiltCap delta : Real) (hvarianceScale : 0 < varianceScale) (hvarianceBudget : 0 < varianceBudget) (htiltCap : 0 < tiltCap) (hdelta : 0 < delta) (hfixed : forall i, i ∈ times -> forall tilt, 0 <= tilt -> tilt <= tiltCap -> mu {omega | quadraticFixedMGFMaximalRadius times varianceScale varianceBudget tiltCap delta <= deviation i omega ∧ predictableVariance i omega <= varianceBudget} <= ENNReal.ofReal (Real.exp (-tilt * quadraticFixedMGFMaximalRadius times varianceScale varianceBudget tiltCap delta + varianceScale * (tilt ^ 2 * varianceBudget)))) : mu (⋃ i ∈ times, {omega | quadraticFixedMGFMaximalRadius times varianceScale varianceBudget tiltCap delta <= deviation i omega ∧ predictableVariance i omega <= varianceBudget}) <= ENNReal.ofReal delta