BanditRLProof.ConcentrationSubGaussian

Transport a conditional sub-Gaussian witness across equality of the conditioning measurable spaces. The two sub-sigma-algebra proofs are propositionally irrelevant once the measurable spaces are identified. This is a general-purpose adapter for filtrations presented through different but extensionally equal histories.

theorem HasCondSubgaussianMGF.of_measurableSpace_eq {Omega : Type u} {m0 m1 mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega -> Real} {c : NNReal} (hm0 : m0 <= mOmega) (hm1 : m1 <= mOmega) (hm : m0 = m1) (hX : HasCondSubgaussianMGF m0 hm0 X c mu) : HasCondSubgaussianMGF m1 hm1 X c mu

A conditionally sub-Gaussian real random variable is integrable under the ambient measure. Mathlib's conditional MGF contract already includes exponential integrability for every real tilt. Applying it at `1` and `-1` gives integrability of the first absolute moment.

theorem HasCondSubgaussianMGF.integrable {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsFiniteMeasure mu] {X : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) : MeasureTheory.Integrable X mu

A conditionally sub-Gaussian variable remains conditionally sub-Gaussian with the same proxy after restriction to an event measurable in the conditioning sigma-algebra. The proof uses one common exceptional set for every exponential tilt: the conditional-expectation kernel is supported on the current side of a conditioning-measurable event, so the indicator-masked variable is kernel-a.e. equal either to the original variable or to zero.

theorem HasCondSubgaussianMGF.indicator {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) {s : Set Omega} (hs : @MeasurableSet Omega m s) : HasCondSubgaussianMGF m hm (s.indicator X) c mu

At a fixed tilt, a conditioning-measurable mask pays the sub-Gaussian quadratic budget only on the masked event. This is the one-step predictable variance interface needed for count-sensitive adaptive-sampling tails.

theorem HasCondSubgaussianMGF.indicator_compensated_hasCondMGFUpperBoundAt {Omega : Type u} {m mOmega : MeasurableSpace Omega} [StandardBorelSpace Omega] {mu : MeasureTheory.Measure Omega} [MeasureTheory.IsProbabilityMeasure mu] {X : Omega -> Real} {c : NNReal} (hm : m <= mOmega) (hX : HasCondSubgaussianMGF m hm X c mu) {s : Set Omega} (hs : @MeasurableSet Omega m s) (tilt : Real) : BanditRLProof.Concentration.HasCondMGFUpperBoundAt m hm (fun omega => tilt * s.indicator X omega - (((c : NNReal) : Real) * tilt ^ 2 / 2) * s.indicator (fun _ : Omega => (1 : Real)) omega) 1 0 mu

Variance proxy induced by an almost-sure interval bound `[lo, hi]`. This is the reusable Hoeffding proxy `(hi - lo)^2 / 4`, represented in the same `NNReal` shape used by Mathlib's bounded-variable sub-Gaussian lemma.

noncomputable def intervalVarianceProxy (lo hi : Real) : NNReal

Bounded variable plus an exact mean identity gives a centered sub-Gaussian witness. This is the generic `TAIL-HOEFFDING-BOUNDED` import wrapper. It keeps the Mathlib assumptions explicit: an a.e.-measurable real variable, an a.s. interval bound, and an equality between its integral and the supplied mean.

theorem boundedCentered_hasSubgaussianMGF_of_mem_Icc_integral_eq {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] {X : Omega -> Real} {lo hi mean : Real} (hmeas : AEMeasurable X mu) (hbound : Filter.Eventually (fun omega : Omega => Set.Icc lo hi (X omega)) (ae mu)) (hmean : integral mu X = mean) : ProbabilityTheory.HasSubgaussianMGF (fun omega : Omega => X omega - mean) (intervalVarianceProxy lo hi) mu

A sub-Gaussian MGF controls the first absolute moment at the natural square-root scale. For a positive proxy, evaluate the MGF at the dimensionless tilt `t = 1 / sqrt c` and use `exp |x| <= exp x + exp (-x)`. The zero-proxy case is Mathlib's a.e.-zero theorem. The constant is intentionally simple; the route needs the `sqrt c` scaling rather than the sharp Gaussian constant.

theorem integral_abs_le_two_mul_sqrt_mul_exp_half_of_hasSubgaussianMGF {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (X : Omega -> Real) (c : NNReal) (hX : ProbabilityTheory.HasSubgaussianMGF X c mu) : integral mu (fun omega => |X omega|) <= 2 * Real.sqrt (c : Real) * Real.exp (1 / 2 : Real)

A global sub-Gaussian MGF gives a conservative explicit second-moment bound. For positive proxy `c`, evaluate the MGF at `t = 1 / sqrt c` and use the quadratic exponential inequality on `|t * X|`. The constant is intentionally non-sharp; it avoids assuming an unavailable derivative-to-variance bridge.

theorem integral_sq_le_four_mul_proxy_mul_exp_half_of_hasSubgaussianMGF {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsProbabilityMeasure mu] (X : Omega -> Real) (c : NNReal) (hX : ProbabilityTheory.HasSubgaussianMGF X c mu) : integral mu (fun omega => X omega ^ 2) <= 4 * (c : Real) * Real.exp (1 / 2 : Real)

Mathlib-backed one-sided tail bound for a finite sum of independent sub-Gaussian real random variables. This is the `TAIL-SUBGAUSS-SUM` import wrapper. It is a thin project-local surface over `ProbabilityTheory.HasSubgaussianMGF.measure_sum_ge_le_of_iIndepFun`.

theorem subGaussian_sum_tail_of_iIndepFun {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) {Idx : Type v} {X : Idx -> Omega -> Real} (h_indep : ProbabilityTheory.iIndepFun X mu) {c : Idx -> NNReal} {s : Finset Idx} (h_subG : forall i, i ∈ s -> ProbabilityTheory.HasSubgaussianMGF (X i) (c i) mu) {eps : Real} (heps : 0 <= eps) : mu.real {omega | eps <= s.sum (fun i => X i omega)} <= Real.exp (-eps ^ 2 / (2 * ((s.sum c : NNReal) : Real)))

ENNReal-valued version of `subGaussian_sum_tail_of_iIndepFun`. This is the `TAIL-SUBGAUSS-DIFF-SUM-IMPORT` boundary adapter used before an ETC-specific reward-difference specialization exists. The summands `X i` stay abstract; later leaves may instantiate them with centered non-best-minus-best exploration reward differences.

theorem subGaussian_sum_tail_ennreal_of_iIndepFun {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {Idx : Type v} {X : Idx -> Omega -> Real} (h_indep : ProbabilityTheory.iIndepFun X mu) {c : Idx -> NNReal} {s : Finset Idx} (h_subG : forall i, i ∈ s -> ProbabilityTheory.HasSubgaussianMGF (X i) (c i) mu) {eps : Real} (heps : 0 <= eps) : mu {omega | eps <= s.sum (fun i => X i omega)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * ((s.sum c : NNReal) : Real))))

Mathlib-backed Azuma-Hoeffding tail bound for a finite prefix of a strongly adapted conditionally sub-Gaussian process. This is the `TAIL-COND-SUBGAUSS` import wrapper. It keeps Mathlib's contract visible: the zeroth summand is unconditionally sub-Gaussian, later summands are conditionally sub-Gaussian with respect to the previous filtration level, and the process is strongly adapted.

theorem condSubGaussian_sum_tail_of_stronglyAdapted {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsZeroOrProbabilityMeasure mu] {Y : Nat -> Omega -> Real} {cY : Nat -> NNReal} {F : Filtration Nat mOmega} (h_adapted : StronglyAdapted F Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) mu) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (Y (i + 1)) (cY (i + 1)) mu) {eps : Real} (heps : 0 <= eps) : mu.real {omega | eps <= (Finset.range n).sum (fun i => Y i omega)} <= Real.exp (-eps ^ 2 / (2 * (((Finset.range n).sum cY : NNReal) : Real)))

ENNReal-valued version of `condSubGaussian_sum_tail_of_stronglyAdapted`. This boundary adapter is shaped for later ETC conditional/filtration routes: it preserves the same Mathlib hypotheses but returns an ordinary measure bound against the canonical exponential RHS wrapped in `ENNReal.ofReal`.

theorem condSubGaussian_sum_tail_ennreal_of_stronglyAdapted {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsFiniteMeasure mu] [IsZeroOrProbabilityMeasure mu] {Y : Nat -> Omega -> Real} {cY : Nat -> NNReal} {F : Filtration Nat mOmega} (h_adapted : StronglyAdapted F Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) mu) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (Y (i + 1)) (cY (i + 1)) mu) {eps : Real} (heps : 0 <= eps) : mu {omega | eps <= (Finset.range n).sum (fun i => Y i omega)} <= ENNReal.ofReal (Real.exp (-eps ^ 2 / (2 * (((Finset.range n).sum cY : NNReal) : Real))))

Two-sided ENNReal Hoeffding tail for a finite sum of independent sub-Gaussian random variables. Mathlib's `HasSubgaussianMGF.sum_of_iIndepFun` supplies the global sum MGF. Upper and negated lower tails are then combined by an outer-measure union, so no event-measurability hypothesis is needed.

theorem subGaussian_sum_abs_tail_ennreal_of_iIndepFun {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {Idx : Type v} {X : Idx -> Omega -> Real} (h_indep : ProbabilityTheory.iIndepFun X mu) {c : Idx -> NNReal} {s : Finset Idx} (h_subG : forall i, i ∈ s -> ProbabilityTheory.HasSubgaussianMGF (X i) (c i) mu) {eps : Real} (heps : 0 <= eps) : mu {omega | eps <= |s.sum (fun i => X i omega)|} <= ENNReal.ofReal (2 * Real.exp (-eps ^ 2 / (2 * ((s.sum c : NNReal) : Real))))

Two-sided ENNReal Azuma-Hoeffding tail for a finite prefix of a strongly adapted conditionally sub-Gaussian process. Mathlib first upgrades the conditional increment witnesses to a global `HasSubgaussianMGF` witness for the finite sum. Applying its one-sided tail to the sum and its negation, then taking an outer-measure union bound, gives the factor-two absolute-deviation estimate. No event-measurability hypothesis is needed.

theorem condSubGaussian_sum_abs_tail_ennreal_of_stronglyAdapted {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsFiniteMeasure mu] [IsZeroOrProbabilityMeasure mu] {Y : Nat -> Omega -> Real} {cY : Nat -> NNReal} {F : Filtration Nat mOmega} (h_adapted : StronglyAdapted F Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) mu) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (Y (i + 1)) (cY (i + 1)) mu) {eps : Real} (heps : 0 <= eps) : mu {omega | eps <= |(Finset.range n).sum (fun i => Y i omega)|} <= ENNReal.ofReal (2 * Real.exp (-eps ^ 2 / (2 * (((Finset.range n).sum cY : NNReal) : Real))))

Two-sided fixed-horizon sub-Gaussian confidence radius for total proxy variance `variance` and failure budget `delta`.

noncomputable def subGaussianSumConfidenceRadius (variance : NNReal) (delta : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem subGaussianSumConfidenceRadius_nonneg (variance : NNReal) (delta : Real) : 0 <= subGaussianSumConfidenceRadius variance delta

No declaration docstring is present; use the chapter context and exact statement below.

theorem subGaussianSumConfidenceRadius_sq (variance : NNReal) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : (subGaussianSumConfidenceRadius variance delta) ^ 2 = 2 * ((variance : NNReal) : Real) * Real.log (2 / delta)

No declaration docstring is present; use the chapter context and exact statement below.

theorem two_mul_exp_neg_subGaussianSumConfidenceRadius_sq_div_eq_delta (variance : NNReal) (delta : Real) (hvariance : 0 < ((variance : NNReal) : Real)) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : 2 * Real.exp (-(subGaussianSumConfidenceRadius variance delta) ^ 2 / (2 * ((variance : NNReal) : Real))) = delta

Delta-calibrated two-sided confidence bound for a finite sum of independent sub-Gaussian random variables.

theorem subGaussian_sum_abs_tail_ennreal_delta_of_iIndepFun {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {Idx : Type v} {X : Idx -> Omega -> Real} (h_indep : ProbabilityTheory.iIndepFun X mu) {c : Idx -> NNReal} {s : Finset Idx} (h_subG : forall i, i ∈ s -> ProbabilityTheory.HasSubgaussianMGF (X i) (c i) mu) (hvariance : 0 < (((s.sum c : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : mu {omega | subGaussianSumConfidenceRadius (s.sum c) delta <= |s.sum (fun i => X i omega)|} <= ENNReal.ofReal delta

Delta-calibrated two-sided Azuma-Hoeffding confidence bound for a finite prefix of a strongly adapted conditionally sub-Gaussian process. The positive-total-variance contract is required because the bad event is written with non-strict `radius <= |sum|`; at zero variance the zero-radius event contains the almost-sure equality path.

theorem condSubGaussian_sum_abs_tail_ennreal_delta_of_stronglyAdapted {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsFiniteMeasure mu] [IsZeroOrProbabilityMeasure mu] {Y : Nat -> Omega -> Real} {cY : Nat -> NNReal} {F : Filtration Nat mOmega} (h_adapted : StronglyAdapted F Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) mu) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (Y (i + 1)) (cY (i + 1)) mu) (hvariance : 0 < ((((Finset.range n).sum cY : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : mu {omega | subGaussianSumConfidenceRadius ((Finset.range n).sum cY) delta <= |(Finset.range n).sum (fun i => Y i omega)|} <= ENNReal.ofReal delta

Two-sided confidence radius for the average of `samples` centered increments. The total proxy variance belongs to the corresponding sum and the division by `samples` performs only the deterministic sum-to-average conversion.

noncomputable def subGaussianAverageConfidenceRadius (variance : NNReal) (samples : Nat) (delta : Real) : Real

No declaration docstring is present; use the chapter context and exact statement below.

theorem subGaussianAverageConfidenceRadius_nonneg (variance : NNReal) (samples : Nat) (delta : Real) : 0 <= subGaussianAverageConfidenceRadius variance samples delta

Deterministic positive-sample-count transport from a two-sided sum-confidence bound to the corresponding average-confidence bound.

theorem measure_average_abs_tail_le_of_measure_sum_abs_tail {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) (X : Omega -> Real) (variance : NNReal) (m : Nat) (hm : 0 < m) (delta : Real) (htail : mu {omega | subGaussianSumConfidenceRadius variance delta <= |X omega|} <= ENNReal.ofReal delta) : mu {omega | subGaussianAverageConfidenceRadius variance m delta <= |X omega / (m : Real)|} <= ENNReal.ofReal delta

Positive random-count transport from a two-sided sum-confidence bound to the corresponding average-confidence bound. No measurability of `count` is needed: Mathlib measures are outer measures on arbitrary sets, and the proof is the pointwise inclusion obtained by multiplying through by the positive realized count.

theorem measure_randomCount_average_abs_tail_le_of_measure_sum_abs_tail {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) (X : Omega -> Real) (count : Omega -> Nat) (variance : NNReal) (delta : Real) (htail : mu {omega | subGaussianSumConfidenceRadius variance delta <= |X omega|} <= ENNReal.ofReal delta) : mu {omega | 0 < count omega ∧ subGaussianAverageConfidenceRadius variance (count omega) delta <= |X omega / (count omega : Real)|} <= ENNReal.ofReal delta

A positive random-count event is covered by its exact-count fibers up to a deterministic count ceiling. This is an outer-measure statement, so neither the count nor the fiber events need to be measurable.

theorem measure_positive_randomCount_event_le_sum_exactCount {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) (count : Omega -> Nat) (maxCount : Nat) (bad : Nat -> Set Omega) (hcount_le : forall omega, count omega <= maxCount) : mu {omega | 0 < count omega ∧ omega ∈ bad (count omega)} <= (Finset.range maxCount).sum (fun i => mu {omega | count omega = i + 1 ∧ omega ∈ bad (i + 1)})

Equal-share finite peeling over every positive exact-count fiber.

theorem measure_positive_randomCount_event_le_of_exactCount_uniform {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) (count : Omega -> Nat) (maxCount : Nat) (bad : Nat -> Set Omega) (hcount_le : forall omega, count omega <= maxCount) (hmaxCount : 0 < maxCount) (delta : Real) (_hdelta : 0 < delta) (hfiber : forall k, 0 < k -> k <= maxCount -> mu {omega | count omega = k ∧ omega ∈ bad k} <= ENNReal.ofReal (delta / (maxCount : Real))) : mu {omega | 0 < count omega ∧ omega ∈ bad (count omega)} <= ENNReal.ofReal delta

Delta-calibrated two-sided confidence bound for the average of exactly `m` independent sub-Gaussian random variables indexed by a finite set.

theorem subGaussian_average_abs_tail_ennreal_delta_of_iIndepFun {Omega : Type u} [MeasurableSpace Omega] (mu : Measure Omega) [IsFiniteMeasure mu] {X : Nat -> Omega -> Real} {c : Nat -> NNReal} (h_indep : ProbabilityTheory.iIndepFun X mu) (m : Nat) (hm : 0 < m) (h_subG : forall i, i < m -> ProbabilityTheory.HasSubgaussianMGF (X i) (c i) mu) (hvariance : 0 < ((((Finset.range m).sum c : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : mu {omega | subGaussianAverageConfidenceRadius ((Finset.range m).sum c) m delta <= |((Finset.range m).sum (fun i => X i omega)) / (m : Real)|} <= ENNReal.ofReal delta

Delta-calibrated two-sided confidence bound for the average of exactly `m` successor increments in a zero-initialized conditional sub-Gaussian process. The process prefix is `Finset.range (m + 1)`: slot zero is the deterministic initial value and slots `1, ..., m` are the `m` averaged increments. The proof is a positive-denominator event transport from the compiled sum confidence theorem.

theorem condSubGaussian_average_abs_tail_ennreal_delta_of_stronglyAdapted {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsFiniteMeasure mu] [IsZeroOrProbabilityMeasure mu] {Y : Nat -> Omega -> Real} {cY : Nat -> NNReal} {F : Filtration Nat mOmega} (h_adapted : StronglyAdapted F Y) (h0 : ProbabilityTheory.HasSubgaussianMGF (Y 0) (cY 0) mu) (m : Nat) (hm : 0 < m) (h_subG : forall i, i < (m + 1) - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (Y (i + 1)) (cY (i + 1)) mu) (hvariance : 0 < ((((Finset.range (m + 1)).sum cY : NNReal) : Real))) (delta : Real) (hdelta : 0 < delta) (hdelta_le_one : delta <= 1) : mu {omega | subGaussianAverageConfidenceRadius ((Finset.range (m + 1)).sum cY) m delta <= |((Finset.range (m + 1)).sum (fun i => Y i omega)) / (m : Real)|} <= ENNReal.ofReal delta

Fixed-tilt one-sided tail for a conditionally sub-Gaussian process masked by conditioning-measurable events. The event retains the random cumulative masked proxy instead of charging every time step.

theorem condSubGaussian_indicator_sum_tail_predictableVariance_fixedTilt {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (X : Nat -> Omega -> Real) (c : Nat -> NNReal) (s : Nat -> Set Omega) (hY : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => (s i).indicator (X i) omega)) (hV : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => (s i).indicator (fun _ => (((c i : NNReal) : Real))) omega)) (hs : forall i, @MeasurableSet Omega (F i) (s i)) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (X i) (c i) mu) (tilt : Real) (htilt : 0 <= tilt) (threshold varianceBudget : Real) : mu {omega | threshold <= (Finset.range n).sum (fun t => match t with | 0 => 0 | i + 1 => (s i).indicator (X i) omega) ∧ (Finset.range n).sum (fun t => match t with | 0 => 0 | i + 1 => (s i).indicator (fun _ => (((c i : NNReal) : Real))) omega) <= varianceBudget} <= ENNReal.ofReal (Real.exp (-tilt * threshold + (tilt ^ 2 / 2) * varianceBudget))

Delta radius for a two-sided masked conditionally sub-Gaussian sum under a deterministic budget on its random cumulative predictable proxy.

noncomputable def subGaussianPredictableVarianceRadius (varianceBudget delta : Real) : Real

Two-sided delta tail for a conditionally sub-Gaussian process with a conditioning-measurable mask and a random cumulative predictable proxy.

theorem condSubGaussian_indicator_sum_abs_tail_predictableVariance_delta {Omega : Type u} [mOmega : MeasurableSpace Omega] [StandardBorelSpace Omega] {mu : Measure Omega} [IsProbabilityMeasure mu] (F : Filtration Nat mOmega) (X : Nat -> Omega -> Real) (c : Nat -> NNReal) (s : Nat -> Set Omega) (hY : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => (s i).indicator (X i) omega)) (hV : StronglyAdapted F (fun t omega => match t with | 0 => 0 | i + 1 => (s i).indicator (fun _ => (((c i : NNReal) : Real))) omega)) (hs : forall i, @MeasurableSet Omega (F i) (s i)) (n : Nat) (h_subG : forall i, i < n - 1 -> ProbabilityTheory.HasCondSubgaussianMGF (F i) (F.le i) (X i) (c i) mu) (varianceBudget delta : Real) (hvarianceBudget : 0 < varianceBudget) (hdelta : 0 < delta) : mu {omega | subGaussianPredictableVarianceRadius varianceBudget delta <= |(Finset.range n).sum (fun t => match t with | 0 => 0 | i + 1 => (s i).indicator (X i) omega)| ∧ (Finset.range n).sum (fun t => match t with | 0 => 0 | i + 1 => (s i).indicator (fun _ => (((c i : NNReal) : Real))) omega) <= varianceBudget} <= ENNReal.ofReal delta