Lean module · Probability layer
BanditRLProof.MeasureL2Indicator
# L2 control of an indicator-restricted integral 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.
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)