Lean module · Probability layer
BanditRLProof.UnboundedStoppingTimeWeightedL2CoordinateIntegrability
# Square-summable weights at an unbounded stopping time This module replaces a moment assumption on an a.e.-finite stopping time by a square-summable deterministic weight. Uniform L2 control of the deterministic coordinates and Cauchy--Schwarz over the measurable stopping fibers then give an integrable weighted stopped value. This is a countable-fiber argument, not optional stopping.
Module map
Imports
BanditRLProof.UnboundedStoppingTimeL2CoordinateIntegrability
Imported by
BanditRLProof, BanditRLProof.RL.FiniteHorizonNaturalCausalInverseSqrtThresholdUnboundedHittingAfterL1Consistency
Declarations
Open an item to read its exact compact statement and source link. Detailed teaching notes are linked when registered.
theorem
BanditRLProof.measurable_stoppedValue_of_measurable_coordinates
Compiled
A stopped value is measurable when the stopping index and every deterministic coordinate are measurable. The proof decomposes the dynamic evaluation into countably many natural-number fibers.
theorem measurable_stoppedValue_of_measurable_coordinates {Omega : Type u} [MeasurableSpace Omega] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (process : Nat -> Omega -> Real) (hprocess : forall n, Measurable (process n)) : Measurable (stoppedValue process tau)
theorem
BanditRLProof.summable_abs_weight_mul_sqrt_stoppingFiberRealMeasure_and_tsum_le
Compiled
Square-summable deterministic weights are summable against the square roots of the real masses of measurable stopping fibers.
theorem summable_abs_weight_mul_sqrt_stoppingFiberRealMeasure_and_tsum_le {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (weight : Nat -> Real) (hweightSq : Summable (fun n => weight n ^ 2)) : Summable (fun n => |weight n| * Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)})) /\ (∑' n : Nat, |weight n| * Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)})) <= Real.sqrt (∑' n : Nat, weight n ^ 2) * Real.sqrt (mu.real Set.univ)
theorem
BanditRLProof.integrable_and_integral_abs_stoppedValue_weight_mul_le
Compiled
Uniform deterministic-coordinate second moments and a square-summable deterministic weight make the weighted stopped value integrable and bound its absolute first moment.
theorem integrable_and_integral_abs_stoppedValue_weight_mul_le {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (process : Nat -> Omega -> Real) (weight : Nat -> Real) (hweightSq : Summable (fun n => weight n ^ 2)) (hstoppedMeasurable : Measurable (stoppedValue (fun n omega => weight n * process n omega) tau)) (secondMomentEnvelope : Real) (hprocessMemLp : forall n, MemLp (process n) 2 mu) (hprocessSecondMoment : forall n, integral mu (fun omega => process n omega ^ 2) <= secondMomentEnvelope) : Integrable (stoppedValue (fun n omega => weight n * process n omega) tau) mu /\ integral mu (fun omega => |stoppedValue (fun n omega => weight n * process n omega) tau omega|) <= Real.sqrt secondMomentEnvelope * (Real.sqrt (∑' n : Nat, weight n ^ 2) * Real.sqrt (mu.real Set.univ))