Lean module · Probability layer
BanditRLProof.ConcentrationQuadraticFixedMGF
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.exists_tilt_quadratic_fixedMGF_exponent_le_negReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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`.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.quadraticFixedMGFRadiusReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.Concentration.measure_deviation_ge_inter_variance_le_delta_of_fixedTilt_quadratic_tailReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
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