Lean module · Probability layer
BanditRLProof.MeasureL2Indicator
This is the nonnegative 2,2 Holder specialization used to turn an event probability bound and an exact second moment into an expected overflow bound.
Module map
Imports
No project-local imports.
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalBoundedStoppingTimeExplicitExpectedAverageRealizedBehaviorRegret, BanditRLProof.UnboundedStoppingTimeL2CoordinateIntegrability
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.integral_indicator_le_sqrt_secondMoment_mul_sqrt_real_measure
Compiled
A nonnegative `L2` function restricted to a measurable event is controlled by its exact second moment and the square root of the event's real mass.
Used in these reading views: Bandit Book · Reinforcement Learning Book · Online Learning Book
2. Probability, kernels, filtrations, and concentration
Canonical node identity
declaration:BanditRLProof.integral_indicator_le_sqrt_secondMoment_mul_sqrt_real_measureReading membership is not a proof dependency. Exact assumptions remain in the Lean statement.
theorem integral_indicator_le_sqrt_secondMoment_mul_sqrt_real_measure {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (f : Omega -> Real) (hf_nonneg : forall omega, 0 <= f omega) (hf : MemLp f 2 mu) (event : Set Omega) (hevent : MeasurableSet event) : integral mu (event.indicator f) <= Real.sqrt (integral mu (fun omega => f omega ^ 2)) * Real.sqrt (mu.real event)