Lean module · Probability layer
BanditRLProof.ConcentrationQuadraticFixedMGF
# Quadratic fixed-MGF optimization This module turns a family of fixed-tilt quadratic exponential tails into a delta-shaped bound. The probabilistic construction of each fixed-tilt tail remains separate, so model-specific consumers only need to expose the common quadratic exponent and admissible tilt cap.
Module map
Imports
BanditRLProof.ConcentrationFixedMGF
Imported by
BanditRLProof, BanditRLProof.ConcentrationQuadraticMaximal, BanditRLProof.ConcentrationQuadraticScheduled, BanditRLProof.ConcentrationSubGaussian, BanditRLProof.Exp3MixedSquareBernstein
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.Concentration.exists_tilt_quadratic_fixedMGF_exponent_le_neg
Compiled
Optimize a quadratic fixed-tilt MGF budget when the quadratic coefficient and admissible tilt cap are separate parameters.
theorem exists_tilt_quadratic_fixedMGF_exponent_le_neg (horizon variance cap budget : Real) (hhorizon : 0 <= horizon) (hvariance : 0 < variance) (hcap : 0 < cap) (hbudget : 0 <= budget) : exists tilt : Real, 0 <= tilt ∧ tilt <= cap ∧ -tilt * (2 * Real.sqrt (horizon * variance * budget) + budget / cap) + horizon * (tilt ^ 2 * variance) <= -budget
def
BanditRLProof.Concentration.quadraticFixedMGFRadius
Compiled
Radius obtained by optimizing a quadratic fixed-tilt exponent over `0 <= tilt <= tiltCap`.
noncomputable def quadraticFixedMGFRadius (varianceScale varianceBudget tiltCap delta : Real) : Real
theorem
BanditRLProof.Concentration.measure_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail
Compiled
A family of fixed-tilt quadratic tails yields a delta-shaped joint deviation and variance-budget tail.
theorem measure_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tail {Omega : Type*} [MeasurableSpace Omega] (mu : Measure Omega) (deviation predictableVariance : Omega -> Real) (varianceScale varianceBudget tiltCap delta : Real) (hvarianceScale : 0 < varianceScale) (hvarianceBudget : 0 < varianceBudget) (htiltCap : 0 < tiltCap) (hdelta : 0 < delta) (hfixed : forall tilt, 0 <= tilt -> tilt <= tiltCap -> mu {omega | quadraticFixedMGFRadius varianceScale varianceBudget tiltCap delta <= deviation omega ∧ predictableVariance omega <= varianceBudget} <= ENNReal.ofReal (Real.exp (-tilt * quadraticFixedMGFRadius varianceScale varianceBudget tiltCap delta + varianceScale * (tilt ^ 2 * varianceBudget)))) : mu {omega | quadraticFixedMGFRadius varianceScale varianceBudget tiltCap delta <= deviation omega ∧ predictableVariance omega <= varianceBudget} <= ENNReal.ofReal delta