BanditRLProof.UnboundedStoppingTimeL2CoordinateIntegrability

The squared successor-round count is the countable sum of its weighted equality fibers. This is an equality in `ENNReal`, so no integrability assumption is needed.

theorem tsum_natSuccSquare_mul_stoppingFiberMeasure_eq_lintegral_rounds_sq {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) : (∑' n : Nat, ((((n + 1) ^ 2 : Nat) : ENNReal) * mu {omega | tau omega = (n : WithTop Nat)})) = ∫⁻ omega, ENNReal.ofReal (((((tau omega).untopA + 1 : Nat) : Real)) ^ 2) ∂mu

The equality fibers of an a.e.-finite L2 stopping time have finite total mass after weighting by the squared successor index.

theorem tsum_natSuccSquare_mul_stoppingFiberMeasure_ne_top {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) : Ne (∑' n : Nat, ((((n + 1) ^ 2 : Nat) : ENNReal) * mu {omega | tau omega = (n : WithTop Nat)})) ∞

The real weighted fiber sum is exactly the second moment of the successor-round count.

theorem tsum_natSuccSquare_mul_stoppingFiberRealMeasure_eq_integral_rounds_sq {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) : (∑' n : Nat, (((n + 1 : Nat) : Real) ^ 2) * mu.real {omega | tau omega = (n : WithTop Nat)}) = integral mu (fun omega => ((((tau omega).untopA + 1 : Nat) : Real)) ^ 2)

The square roots of the real equality-fiber masses are summable for an a.e.-finite stopping time whose successor round count belongs to `L2`.

theorem summable_sqrt_stoppingFiberRealMeasure_of_memLp_two {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) : Summable (fun n : Nat => Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)}))

The square-root fiber-mass sum is quantitatively controlled by one half of the stopping-round second moment plus the universal inverse-square series. This is a fixed-stopping-time estimate, not a uniform family bound.

theorem tsum_sqrt_stoppingFiberRealMeasure_le_half_mul_integral_rounds_sq_add_tsum_inverse_natSuccSquare_of_memLp_two {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) : (∑' n : Nat, Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)})) <= (1 / 2 : Real) * (integral mu (fun omega => ((((tau omega).untopA + 1 : Nat) : Real)) ^ 2) + ∑' n : Nat, 1 / (((n + 1 : Nat) : Real) ^ 2))

Cauchy--Schwarz controls the square-root stopping-fiber masses by the actual successor-round second moment and the shifted inverse-square series. This is a fixed-stopping-time estimate, not a uniform family bound.

theorem tsum_sqrt_stoppingFiberRealMeasure_le_sqrt_integral_rounds_sq_mul_sqrt_tsum_inverse_natSuccSquare_of_memLp_two {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) : (∑' n : Nat, Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)})) <= Real.sqrt (integral mu (fun omega => ((((tau omega).untopA + 1 : Nat) : Real)) ^ 2)) * Real.sqrt (∑' n : Nat, 1 / (((n + 1 : Nat) : Real) ^ 2))

Uniform deterministic-coordinate second moments and an L2 finite stopping time make the corresponding unbounded stopped value integrable. The proof is a countable equality-fiber decomposition; it does not use optional stopping.

theorem integrable_stoppedValue_of_uniform_secondMoment_of_memLp_two_rounds {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) (process : Nat -> Omega -> Real) (hstoppedMeasurable : Measurable (stoppedValue process tau)) (secondMomentEnvelope : Real) (hprocessMemLp : ∀ n, MemLp (process n) 2 mu) (hprocessSecondMoment : ∀ n, integral mu (fun omega => process n omega ^ 2) <= secondMomentEnvelope) : Integrable (stoppedValue process tau) mu

A quantitative version of the stopping-fiber transport: the absolute first moment of the stopped value is bounded by the uniform coordinate L2 envelope times the sum of square roots of the stopping-fiber masses. This is a fixed-stopping-time bound, not an index-uniform rate or optional stopping.

theorem integral_abs_stoppedValue_le_uniformSecondMoment_mul_tsum_sqrt_stoppingFiberRealMeasure_of_memLp_two_rounds {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) (process : Nat -> Omega -> Real) (secondMomentEnvelope : Real) (hprocessMemLp : ∀ n, MemLp (process n) 2 mu) (hprocessSecondMoment : ∀ n, integral mu (fun omega => process n omega ^ 2) <= secondMomentEnvelope) : integral mu (fun omega => |stoppedValue process tau omega|) <= Real.sqrt secondMomentEnvelope * ∑' n : Nat, Real.sqrt (mu.real {omega | tau omega = (n : WithTop Nat)})

The stopped-value first moment inherits the Cauchy--Schwarz stopping-fiber bound. The estimate is for one fixed stopping time and does not invoke optional stopping.

theorem integral_abs_stoppedValue_le_uniformSecondMoment_mul_sqrt_integral_rounds_sq_mul_sqrt_tsum_inverse_natSuccSquare_of_memLp_two_rounds {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) (process : Nat -> Omega -> Real) (secondMomentEnvelope : Real) (hprocessMemLp : ∀ n, MemLp (process n) 2 mu) (hprocessSecondMoment : ∀ n, integral mu (fun omega => process n omega ^ 2) <= secondMomentEnvelope) : integral mu (fun omega => |stoppedValue process tau omega|) <= Real.sqrt secondMomentEnvelope * (Real.sqrt (integral mu (fun omega => ((((tau omega).untopA + 1 : Nat) : Real)) ^ 2)) * Real.sqrt (∑' n : Nat, 1 / (((n + 1 : Nat) : Real) ^ 2)))

The stopping-fiber absolute first-moment estimate with its fiber sum eliminated in favor of the actual successor-round second moment and the universal inverse-square series.

theorem integral_abs_stoppedValue_le_uniformSecondMoment_mul_half_roundSecondMoment_add_inverseSquareTsum_of_memLp_two_rounds {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] (tau : Omega -> WithTop Nat) (htau : Measurable tau) (hfinite : ∀ᵐ omega ∂mu, tau omega ≠ ⊤) (hrounds : MemLp (fun omega => (((tau omega).untopA + 1 : Nat) : Real)) 2 mu) (process : Nat -> Omega -> Real) (secondMomentEnvelope : Real) (hprocessMemLp : ∀ n, MemLp (process n) 2 mu) (hprocessSecondMoment : ∀ n, integral mu (fun omega => process n omega ^ 2) <= secondMomentEnvelope) : integral mu (fun omega => |stoppedValue process tau omega|) <= Real.sqrt secondMomentEnvelope * ((1 / 2 : Real) * (integral mu (fun omega => ((((tau omega).untopA + 1 : Nat) : Real)) ^ 2) + ∑' n : Nat, 1 / (((n + 1 : Nat) : Real) ^ 2)))