FormalSLT theorem index

Time-uniform mixture confidence sequence from the sub-Gamma exponential supermartingale

Betting wealth from predictable bets under the conditional-mean null is a nonnegative supermartingale

End-to-end betting confidence sequence for a bounded mean from predictable bets and the conditional-mean null

Countable-time Ville confidence sequence for the betting wealth e-process

Conditional-expectation swap for the mixture exponential process

Weighted countable sums of real supermartingales are supermartingales under the domination hypothesis, the countable analogue of supermartingale_finset_sum

The p-series dyadic-epoch mixture of stitched sub-Gamma exponential processes is a nonnegative supermartingale

One-sided all-n dyadic-epoch sub-Gamma confidence sequence with the explicit grid budget

Two-sided all-n dyadic-epoch confidence sequence via the X/-X transfer and the explicit stitching penalty

Optional continuation: the stopped value of an e-process keeps integral at most one

Product of nonnegative supermartingale factors with unit start is an e-process

Safe-testing Type-I control: an e-process rejection event has mass at most the level α over the Ville maximal inequality

Obstruction: a fixed finite-grid all-time closed-form bridge forces the grid to attain the exact per-time optimal boundary

Obstruction: the literal harmonic dyadic-epoch weights are not summable, ruling out the naive all-n epoch mixture

Mixture of sub-Gamma exponential processes is a nonnegative supermartingale

Optimized-λ sub-Gamma confidence sequence with the stitched boundary

Closed-form pointwise interval-width form of the two-sided optimized-λ confidence sequence

Two-sided optimized-λ iterated-log confidence sequence via the deterministic stitching bridge and the X/-X transfer

The redirected p-series dyadic-epoch weights are summable, recovering a finite epoch-capital budget

The concrete unit-capital stitching penalty for the first p-series epoch is log 2

Prior mixture of per-hypothesis fixed-tilt exponential processes is a nonnegative supermartingale

Ville crossing bound for the stitched sub-Gamma boundary

The all-n dyadic-epoch boundary is the log-log width plus the explicit per-epoch stitching penalty

The closed-form log-log width equals the sub-Gamma boundary at the per-time optimal tilt

Stitched boundary half-width grows at the iterated-logarithm rate

Stitched-over-λ sub-Gamma exponential process is a nonnegative supermartingale

Process-level time-uniform PAC-Bayes bound: with probability at least 1 - δ, the posterior running mean of the abstract martingale-difference process stays under the cgf/KL/log(1/δ) boundary for every n ≥ 1

Ville crossing bound for the prior-mixture process over all times

Sample mean is the global Bernoulli log-likelihood maximizer

Bernoulli log-likelihood score vanishes at the sample-mean MLE

Bootstrap-resample mean equals the sample mean

Sample mean is the known-variance Gaussian MLE

Horvitz-Thompson estimator is design-unbiased for the finite-population total

Sample mean is unbiased for the finite population mean

Bessel-corrected sample variance (1/(n-1)) ∑ (x i - x̄)²

Bessel-corrected sample variance is unbiased for the finite-population variance

Finite weighted expectation ∑ w x · X x, the population-mean primitive

Linearity of the weighted expectation in the estimator

Pointwise Bennett Taylor bound for bounded increments in the regime b * λ < 3

Pulls a bounded measurable factor through conditional expectation under the stated integrability hypotheses

Under conditional centering, the conditional second moment is the conditional variance proxy

Conditional Jensen inequality for real-valued conditional expectations

Boundedness, conditional centering, and a conditional second-moment proxy imply a conditional sub-Gamma MGF bound

Conditional Markov-style inequality for nonnegative real functions

Bounded real increments have integrable exponential tilts under a finite measure

Finite-sample scalar contraction for 1-Lipschitz transforms

Empirical Rademacher wrapper for 1-Lipschitz transforms

Rad_S(φ ∘ F) <= L * Rad_S(F) for finite scalar classes

One coordinate replacement step for the finite contraction proof

Finite net with an explicit nearest projection

Predicate selecting empirical risk minimizers over a finite class

Binary label patterns realized on a sample

Distinct loss vectors realized on a sample

Finite-sample empirical Rademacher complexity

Sample average loss

Risk above the best-in-class comparator

One-sided uniform generalization gap

IID product measure on Fin n -> Z

Expected loss under a measure

Finite skeleton and terminal-scale certificate for an epsilonized Dudley boundary step

Finite-cover/pathwise-modulus certificate for the epsilonized Dudley boundary step

Packaged reusable finite dyadic Dudley instance: net sequence, coarse budget, variance positivity, and coarse projected-supremum bound

Optional supplied-supremum adapter to a terminal projected finite-net supremum plus explicit terminal error

Projected finite-net Dudley bound from a packaged finite dyadic Dudley instance

Supplied-supremum finite Dudley bound from a packaged instance and adapter

Finite image of a net projection, used to avoid a finite ambient index assumption

Dyadic total-bounded net schedule satisfies the adjacent-radius budget used by finite chaining

Packages the total-bounded dyadic net schedule as a FiniteDyadicNetSequence under global projection-pair hypotheses

Packages the total-bounded dyadic net schedule as a FiniteDyadicDudleyInstance when global coarse-budget and projection-pair hypotheses are available

Finite dyadic entropy-at-radius upper sum sampled at lower annulus endpoints

Finite entropy-at-radius upper sum dominated by a single truncated interval integral

Finite dyadic budget comparison to an entropy-at-radius upper sum

One-step dyadic entropy budget for a constant entropy envelope

Expected supplied supremum controlled through explicit finite-skeleton and terminal-projection errors

Finite expectation adapter from a supplied supremum functional to a projected finite-supremum surrogate

Totally bounded metric spaces admit finite covers at every positive real radius

Extracts the repo's bundled finite-net record from total boundedness

Constant scale budgets remain constant under the finite prefix-sup envelope

Monotone scale budgets equal their finite prefix-sup envelope

Finite ambient supremum controlled by a finite skeleton under pointwise approximation

Finite skeleton supremum controlled by terminal projected finite-net supremum plus explicit error

Finite multiscale chaining decomposition in expectation

Covering-number version for finite net sequences

Projection-pair entropy version for finite net sequences

Radius-bounded finite chaining with square-root entropy budgets

Finite Dudley-style entropy sum with covering-number products

Finite dyadic annulus-budget bridge for covering numbers

Per-scale entropy-budget wrapper for covering numbers

Finite dyadic entropy-integral budget for covering numbers

Finite covering-count wrapper with a monotone prefix-sup entropy envelope

Dyadic/geometric radius schedule for covering numbers

Uniform entropy cap collapses the dyadic covering-number sum to a 2 * radiusScale budget

Finite Dudley-style entropy sum over projection-pair families

Finite dyadic annulus-budget bridge for projection pairs

Per-scale entropy-budget wrapper for projection pairs

Finite dyadic entropy-integral budget for projection pairs

Dyadic/geometric radius schedule for projection pairs

Uniform entropy cap collapses the dyadic sum to a 2 * radiusScale budget for projection pairs

Finite-terminal total-bounded dyadic wrapper composed with the finite Dudley entropy-budget theorem

Epsilonized total-bounded Dudley wrapper from finite-cover and pathwise-modulus certificates

For every positive error budget, a finite skeleton/terminal-scale certificate yields a Dudley bound with + eta

MGF control gives finite expected-sup entropy budget

Optimized finite sub-Gaussian max bound

Projected finite-net-image chaining bound without [Fintype T]

Projected finite-net Dudley wrapper compared to a supplied finite entropy-at-radius integral budget

Projected finite-net Dudley wrapper with a truncated interval-integral entropy budget

Projected finite-net-image Dudley wrapper without [Fintype T]

Total-bounded dyadic wrapper over the terminal projected finite-net image, without [Fintype T]

Total-bounded projected finite-net wrapper compared to a supplied finite entropy-at-radius integral budget

Total-bounded projected finite-net wrapper with one truncated interval-integral entropy budget

Finite projected-supremum chaining without an identity terminal projection

Projected finite-net chaining bound with covering-number entropy budgets

Projected finite Dudley wrapper with a monotone prefix-sup entropy envelope

Total-bounded dyadic wrapper for the terminal projected supremum, without an identity terminal net

Boundary-layer finite Dudley wrapper with explicit finite-skeleton and terminal-projection hypotheses

Total-bounded boundary wrapper with explicit finite-skeleton/dense-net and terminal-projection assumptions

Boundary-layer finite Dudley wrapper for a supplied supremum functional plus terminal error

Total-bounded boundary wrapper for a supplied supremum functional under explicit terminal approximation

Total-bounded Dudley boundary wrapper using approximate witnesses, finite skeleton selectors, and pathwise modulus

Rad(F) <= ε + Rad(N_ε)

Covering plus Massart

Two-scale finite chaining bound

Shifted finite dyadic annulus integrals compose into one truncated interval integral

Finite-cover radius plus pathwise modulus gives the finite-skeleton approximation hypothesis

Supplied supremum functional controlled by an approximate witness and finite skeleton selector

Terminal net radius plus pathwise modulus discharges the terminal-projection approximation hypothesis

Radius-bound variant of terminal pathwise-modulus approximation

Bernoulli mean equals p

Bernoulli(p) probability mass function on Bool

Bernoulli variance equals p(1 - p)

Two-sided Bernstein tail specialized to Bernoulli(p)

Sample mean (1/n) ∑ x i of a finite sample

Two-sided Hoeffding tail for the named sample mean

Population-form sample variance (1/n) ∑ (x i - x̄)²

Variance decomposition Var = E[X²] - x̄²

Sample variance is nonnegative

Discrete metric on Fin n

The finite discrete metric is nonnegative

The finite discrete metric is symmetric

The finite discrete metric satisfies the triangle inequality

Packaged finite dyadic Dudley instance for the Fin n embedded Rademacher process

Explicit adjacent-scale cover-count envelope n * n

Full finite net on Fin n at every dyadic scale

General FiniteDyadicNetSequence instance for Fin n with [Fact (2 ≤ n)]

Adjacent finite-discrete covering-number products are bounded by the n * n envelope

The full finite discrete net has covering number n

Finite discrete nets use the process metric

The embedded Rademacher process packaged as a finite sub-Gaussian process over Fin n

Supremum functional for the embedded Rademacher process over Fin n

Supplied-supremum adapter for the finite-discrete packaged Dudley instance

Supplied-supremum finite Dudley bound for the embedded Rademacher process routed through the packaged finite dyadic Dudley API

Terminal projected-net adapter for the finite-discrete supplied supremum

The supplied supremum is nontrivial: it equals 1 on the positive Rademacher outcome

One-coordinate Rademacher process embedded in the finite discrete family

Arbitrary finite-horizon projected Dudley bound for the embedded Rademacher process routed through the packaged finite dyadic Dudley API

Embedded Rademacher process increments satisfy the sub-Gaussian MGF bound

Bernoulli natural-family base weights on Bool

Bernoulli natural sufficient statistic 1{true}

Bernoulli natural Fisher information equals variance at theta = 0

Bernoulli natural Fisher information at theta = 0 is 1/4

Bernoulli natural A'(0) = 1/2

Bernoulli natural A''(0) = 1/4

Bernoulli natural log-partition at theta = 0 is log 2

Bernoulli natural mean at theta = 0 is 1/2

Bernoulli natural partition sum is 1 + exp(theta)

Both Bernoulli natural atoms have mass 1/2 at theta = 0

Bernoulli natural variance at theta = 0 is 1/4

Concrete Bernoulli witness with mean 1/2, variance 1/4, and Fisher information 1/4

Natural-parameter Fisher information equals finite variance

Direct bridge I(theta) = A''(theta)

Finite exponential-family mean equals the log-partition derivative numerator divided by Z(theta)

Natural-parameter score equals the centered sufficient statistic

Finite exponential-family variance equals log-partition second derivative

Natural-parameter finite exponential-family probability mass

Natural-parameter derivative of the finite exponential-family mass

Derivative of the normalized finite exponential-family mass

Positive base weights give positive normalized masses

Normalized exponential-family masses sum to one

Log-partition function A(theta) = log Z(theta)

Log-partition derivative identity A'(theta) = E_theta[T]

Positive-base wrapper for A'(theta) = E_theta[T]

Log-partition curvature identity A''(theta) = Var_theta(T)

Positive-base wrapper for A''(theta) = Var_theta(T)

Centered second-moment derivative equals finite weighted variance

Differentiating the finite mean gives a centered second moment

Finite exponential-family partition sum Z(theta)

Termwise derivative of the finite partition sum

Positive base weights give positive finite partition sum

Finite-index measure union bound

Supplied finite per-event budgets whose sum is bounded by a total budget

Nonempty finite class with per-event budget α / card has union mass ≤ α

Common per-event budget gives card * β total mass

Explicit per-event budget whose finite sum is bounded by a total budget

Bernoulli Fisher information 1 / (p(1-p))

Concrete witness: identity estimator attains variance 1/4 = 1 / I(1/2)

Concrete witness: I(1/2) = 4

Weighted Cauchy-Schwarz: Cov² ≤ Var · Var

Estimator-score covariance equals the derivative of the estimator mean

Cramér-Rao lower bound 1 / I(θ) ≤ Var(T) for an unbiased estimator

Fisher information as the weighted variance of the score

Score ∂_θ log p(x; θ) as pmfDeriv / pmf

Score has zero mean under regularity (∑ p' = 0)

Finite weighted covariance of two functions

Finite weighted variance of an estimator under a weight vector

Glivenko-Cantelli class predicate: a.s. uniform-deviation convergence to zero

Concrete non-vacuity witness: explicit four-sample uniform empirical-CDF deviation ≤ 1/4

Classical Glivenko-Cantelli for i.i.d. real samples: empirical CDF converges uniformly a.s. to the population CDF

Uniform a.s. GC from pointwise convergence on closed and strict lower rays

Empirical CDF as the lower-ray indicator-class empirical average

Uniform empirical-CDF deviation sup_x abs(F_n(x) - F(x))

Empirical CDF equals the lower-ray indicator empirical average

Finite grid of bracket points that controls every threshold at a chosen mesh

Population lower-ray mass equals the CDF of the pushed-forward law

Deterministic finite-grid bracketing bound on the uniform empirical-CDF deviation

The classical empirical-CDF GC statement is exactly the lower-ray indicator-class GC statement

Closed lower-ray indicator 1{x ≤ z} as the empirical-CDF integrand

Pointwise empirical-CDF strong law at a fixed threshold from the mathlib strong law

Wraps the GC class into the Rademacher ERM generalization surface

Open lower-ray indicator 1{x < z}, the atom-safe upper bracket

Open-upper-bracket pointwise strong law, the atom-safe companion

Wraps the GC class into the finite-class VC/Hoeffding empirical-process surface

Wraps the GC class into the VC/PAC-Bayes hybrid surface

Two-sided Bennett / sub-Gamma tail at a chosen λ for a finite distribution

Two-sided Bernstein tail P(abs X ≥ ε) ≤ 2 exp(-ε²/(2(v + bε/3))) for a finite distribution

Generic two-sided sub-Gaussian tail P(abs X ≥ t) ≤ 2 exp(-t²/(2c)) from an MGF bound

Two-sided Hoeffding tail for the sample mean P(abs (X̄ - E X̄) ≥ t) ≤ 2 exp(-2 n t²/(b-a)²)

Centered two-sided sub-Gaussian tail P(abs (X - E X) ≥ t) ≤ 2 exp(-t²/(2c))

Effective 0-1 loss patterns equal binary traces

Binary VC Sauer-Shelah corollary

Effective-class Massart bound

E[genGap] <= 2 * E[Rad]

Massart plus sharp high-probability Rademacher

P(genGap >= 2 * E[Rad] + ε) <= exp(-ε² n / (2B²))

VC-style one-sided genGap tail with sharp exponent

P(genGap - E[genGap] >= ε) <= exp(-ε² n / (8B²))

P(genGap - E[genGap] >= ε) <= exp(-ε² n / (2B²))

P(f - E[f] >= ε) <= exp(-2ε² / sum_k c_k²)

Rad(H,S) <= B * sqrt(2 * log card(H) / n)

Public wrapper for the sharp product bounded-differences tail

Heterogeneous-law product upper tail with the sharp McDiarmid exponent

Heterogeneous-law product lower tail with the sharp McDiarmid exponent

Lower-tail wrapper obtained from the upper tail applied to -f

Homogeneous recovery from the heterogeneous product theorem by taking a constant law family

sum_{k<=d} C(n,k) <= (en/d)^d

Two-sided finite-class uniform deviation with sharp one-sided tails

VC-style two-sided uniform deviation with sharp one-sided tails

Rad <= B * sqrt(2d * log(en/d) / n)

VC-style ERM excess-risk tail with sharp concentration term

Closed-form VC ERM sample-complexity theorem with explicit 72 * B^2 constant

Finite Bernstein condition: excess-loss second moment controlled by excess risk

Finite coordinate-swap symmetry predicate for explicit sample weights

Deterministic envelope certificate: above rStar, the localized envelope is below the identity

Deterministic localized concentration-event interface for population excess risk versus empirical excess risk

Literal finite iid product-weight absolute expected generalization-gap wrapper

Literal finite absolute expected generalization-gap wrapper under a finite swap identity

Uniform stability gives finite iid two-sided expected stability gap ≤ β

Uniform stability gives finite two-sided expected stability gap ≤ β under a finite swap identity

Product-measure two-sided expected gap ≤ β with bounded-loss integrability discharged

Iid product-weight Bernstein tail with the n * eps^2 exponent

Finite centered bounded-variance Bennett MGF

Sub-Gamma denominator form of the finite Bennett MGF

One-sample finite Bernstein upper-tail bound

Bounded empirical coordinate loss is integrable under μⁿ

Bounded finite-class selected loss is integrable under μⁿ × μ

Bounded coordinate-updated selected loss is integrable under μⁿ × μ

Stability high-probability bound with explicit expected-gap and measurability hypotheses

Bounded-loss finite-class wrapper for the sharp stability high-probability theorem

β = c0 / n stability corollary for the sharp variant

Bounded-loss finite-class β = c0 / n high-probability stability corollary

Fixed-λ Catoni penalty optimized to a square-root budget

Variance proxy for the centered excess-loss deviation is bounded by c * r on the localized class

Continuous prior/posterior certificate with the PAC gate derived by change of measure

Continuous fixed-lambda Catoni change-of-measure bound from a prior log-MGF certificate

Measure-theoretic Donsker-Varadhan bound from Radon-Nikodym tilting

Pointwise Bennett inequality for a centered bounded variable

Literal finite iid product-weight E[R(A(S)) - Rhat_S(A(S))] ≤ β wrapper

Literal finite E[R(A(S)) - Rhat_S(A(S))] ≤ β wrapper under a finite swap identity

Uniform stability gives finite iid product-weight expected gap ≤ β

Uniform stability gives finite expected gap ≤ β under a finite swap identity

Product-measure expected gap ≤ β with bounded-loss integrability discharged

Finite [0,1] Catoni-style PAC-Bayes posterior-risk bad-event bound

Finite per-hypothesis loss measurability gives joint loss measurability

Finite empirical risk for a real-valued loss

Localized deviation plus Bernstein/fixed-point control gives a finite fast-rate shell

Localized deviation plus nonpositive empirical excess risk controls population excess risk by the deviation slack

Fast-rate shell stated through the named sample-dependent upper-deviation event

Sample-dependent localized upper-deviation event payoff for empirical competitors

Event-facing finite fast-rate shell, reducing the remaining localized task to proving the upper-deviation event

Fixed-threshold localized upper-deviation event payoff for empirical competitors

Finite [0,1] fixed-budget McAllester-style bad-event bound

Posterior-dependent finite-grid McAllester wrapper under an explicit bucket certificate

Finite-grid McAllester peeling bound with allocated confidence mass

Finite supplied margin-proxy wrapper with sqrt(2 * Vρ * Cρ) + scale * Cρ penalty form

Posterior-dependent finite Bernstein bad-event wrapper under complexity and penalty certificates

Finite fixed-lambda PAC-Bayes Bernstein bad-event bound

Prior-averaged finite iid empirical-risk-deviation MGF bound

Iid finite product sample weights ∏ k, p (S k)

Finite iid product weights satisfy the coordinate-swap identity

Exact iid product factorization of E exp(lam * (R_i - Rhat_i))

Single-coordinate MGF budget lifts to the finite sample-average MGF

Finite KL divergence is nonnegative under full support

Event membership constructs the deterministic localized deviation certificate

Finite localized empirical Rademacher complexity is monotone under predicate inclusion

Localized empirical Rademacher complexity is nonnegative when the class contains an identically zero excess-loss comparator

Bernstein bridge plus fixed-point certificate controls excess-risk localized empirical complexity by c * r

Bernstein embeds excess-risk localized complexity into second-moment localized complexity

Excess-risk localized empirical Rademacher complexity is nonnegative because the comparator belongs to every nonnegative radius

Conservative finite fast-rate high-confidence wrapper pairing the bounded-excess bad-event mass with the Bernstein/fixed-point payoff

Assumption-facing high-confidence wrapper from supplied centered shifted-moment budgets. Interface only — the budgets it consumes are conservative-only per hypothesis

Assumption-facing high-confidence finite fast-rate wrapper from shifted exponential-moment budgets

Bounded-excess finite-product shifted-moment budget for one hypothesis in the named fast-rate random-threshold event

Algebraic interface: factors the fixed slack out of the shifted moment. Conservative-only (per-hypothesis centered moment ≤ fixed moment); names the whole-supremum obligation, does not discharge it

Finite weighted mass outside the named fast-rate random-threshold localized event

Conservative finite product-mass bound for the named fast-rate event by reduction to the fixed-threshold bounded-excess theorem

Named fast-rate bad-event mass is controlled by the fixed-ε bad-event mass using nonnegativity of the empirical localized complexity

Algebraic interface: bad-event mass via summed centered moments and a fixed-slack denominator. Conservative-only union bound; not a non-conservative concentration result

Named fast-rate bad-event mass controlled by shifted exponential-moment budgets

Named random-threshold event used by the finite fast-rate shell

Finite localized Bernstein high-confidence theorem with bad-event mass bounded by the averaged Bernstein tail and fixed-threshold payoff

Fixed-threshold finite high-confidence localized statement combining bounded-excess bad-event mass with the empirical-competitor payoff

Bounded excess losses in [-1,1] supply the localized one-coordinate MGF budget

Finite weighted mass of one pointwise upper-deviation bad event with a sample-dependent threshold

Pointwise sample-dependent bad-event mass controlled by its shifted exponential moment

Shifted exponential moment for one localized upper-deviation gap with a sample-dependent threshold

Fixed slack added to a sample-dependent threshold factors out of the shifted exponential moment

Sample-dependent shifted moment controlled by a fixed-threshold exponential moment under a pointwise lower bound on the random threshold

Finite weighted mass of one pointwise upper-deviation bad event

Pointwise Markov adapter from an exponential-moment budget to an upper-deviation bad-event mass

Finite weighted exponential moment for one localized upper-deviation gap

Finite iid product MGF bridge for one localized upper-deviation gap from a one-coordinate MGF budget

Supplied-mass high-confidence adapter for sample-dependent localized upper-deviation events

Sample-dependent high-confidence adapter from shifted exponential-moment budgets

Finite weighted mass outside a sample-dependent localized upper-deviation event

Sample-dependent bad-event mass is controlled by a fixed-threshold bad-event mass when the random threshold is pointwise larger

Sample-dependent localized upper-deviation bad-event mass is controlled by pointwise sample-dependent bad-event masses

Sample-dependent localized bad-event mass controlled by summed shifted exponential-moment budgets

Sample-dependent localized bad-event mass controlled by supplied pointwise tail budgets

Sample-dependent localized upper-deviation event for random-threshold arguments

Envelope bound plus fixed-point certificate controls second-moment localized empirical complexity by its radius

Finite localized supremum of population-minus-empirical excess-risk gaps

Finite weighted mass outside the localized upper-deviation event

Delta-form iid product-weight localized concentration bound under pointwise [-1,1] excess-loss assumptions

Iid product-weight localized bad-event mass bound under pointwise [-1,1] excess-loss assumptions

Delta-form finite localized concentration adapter from supplied pointwise tail budgets

Localized bad-event mass controlled by summed pointwise exponential-moment budgets

Finite weighted union bound: localized upper-deviation bad-event mass is controlled by pointwise localized bad-event masses

Localized bad-event mass controlled by supplied pointwise tail budgets

Sample event where the localized upper-deviation statistic is bounded

Iid bounded-differences upper tail with the sharp McDiarmid constant

[0,1] bounded-loss one-coordinate MGF instantiation

Closed PAC-Bayes good-event theorem: with product-sample mass at least 1 - delta, every posterior satisfies the Catoni-form risk bound

Rescaled finite Donsker-Varadhan change-of-measure inequality

Deterministic PAC-Bayes posterior bound from a prior log-MGF certificate

Deterministic sqrt-form bound under a uniform-in-λ MGF certificate

Fixed-λ sub-Gaussian deterministic PAC-Bayes bound

Deterministic fixed-sample PAC-Bayes Bernstein adapter from a prior-moment certificate

Posterior average of a supplied per-hypothesis margin-variance proxy

Deterministic posterior-risk adapter from a prior MGF certificate

Deterministic fixed-budget McAllester-style posterior-risk adapter

Prior-averaged bounded-loss MGF bound

Finite Markov bad-event bound for the prior MGF

Normalized Bernstein prior exponential moment with variance and scale terms

Finite sample-average bounded-loss MGF bound

Uniform stability gives bounded differences for the gen gap scaffold

Uniform stability gives bounded differences for training loss

The two-point discrete metric index type

The two-point discrete metric is nonnegative

The two-point discrete metric is symmetric

The two-point discrete metric satisfies the triangle inequality

Packaged finite dyadic Dudley instance for the two-point Rademacher process

Full two-point finite net with dyadic positive radius

A second concrete FiniteDyadicNetSequence instantiation, independent of [0,1]

Adjacent two-point covering-number products are bounded by the constant cover-count envelope

Adjacent two-point projection-pair families are nontrivial

Adjacent two-point dyadic radii satisfy the geometric chaining budget

The two-point Rademacher process packaged as a finite sub-Gaussian process

Supplied-supremum adapter for the two-point packaged Dudley instance

Supplied-supremum finite Dudley bound routed through the packaged finite dyadic Dudley API

Terminal projected-net adapter for the two-point supplied supremum

Arbitrary finite-horizon projected Dudley bound routed through the packaged finite dyadic Dudley API

One-coordinate Rademacher process increments satisfy the sub-Gaussian MGF bound

Bundled assumptions for the [0,1] finite-class dyadic confidence sequence

Bundled API theorem bounding the named confidence-sequence failure event

Confidence-sequence failure-probability theorem for all natural times and finite hypotheses

Existential-event anytime theorem using the named dyadic confidence radius

Existential-event version of the countable-time finite-class Hoeffding theorem

Countable-time finite-class Hoeffding theorem for [0,1] losses with dyadic per-time radii

Countable-time dyadic absolute-deviation shell with time-varying thresholds

Countable-time finite-class union shell using the standard dyadic schedule

Countable-time finite-class union shell with a supplied summable time-budget sequence

Rewrites a countable time-class indexed union as an existential event

Rewrites failure of an all-times/all-hypotheses strict bound as an existential crossing event

Named ENNReal lower-tail budget produced by the fixed-hypothesis Hoeffding wrapper

Finite-sum range envelope from a pointwise uniform range-width bound

Positive finite-sum denominator certificate from one sampled coordinate with positive range

Combined two-sided empirical-average Hoeffding budget

Algebraic bridge from the concrete finite sum of squared half-ranges to the uniform range proxy

Two-sided Hoeffding tail bridge from a pointwise range-width bound and closed-form proxy

Two-sided Hoeffding tail bridge using pointwise range width and an explicit nondegenerate sample coordinate

Algebraic bridge from a square-root radius condition to the displayed sample-size lower bound

Displayed two-sided Hoeffding budget 2 * exp(-2 * sampleSize * ε^2 / R^2)

Unit-range displayed Hoeffding tail is bounded at the inverted square-root confidence radius

Real log-budget condition implies the displayed Hoeffding tail fits a target budget

Explicit sample-size lower bound implies the displayed Hoeffding tail fits a target budget

Uniform-range two-sided empirical-average Hoeffding budget with one denominator proxy

Algebraic identification between the range-proxy budget and the sample-size display

Named ENNReal upper-tail budget produced by the fixed-hypothesis Hoeffding wrapper

Normalizes the upper-tail Hoeffding range expression to the lower-tail expression

Named failure event for the [0,1] finite-class dyadic confidence sequence

Pointwise absolute-deviation tails imply a simultaneous finite-class bound

Equal-budget absolute-deviation bridge for finite hypothesis classes

Pointwise finite-class bad-event tails imply a simultaneous card * tail bound

Equal split of a target failure budget gives simultaneous mass ≤ δ

Concrete real dyadic class budget maps exactly to the ENNReal dyadic time/class split

Finite-horizon dyadic real-budget monotonicity: the horizon budget is no larger than any prefix time budget

Closed-form rewrite of the finite-horizon dyadic log-budget term

Standard dyadic time-budget schedule δ * 2^(-1-t)

Every finite prefix of the dyadic time-budget schedule sums to at most δ

The full natural-time dyadic schedule has total budget at most δ

Route-facing finite-prefix finite-class Hoeffding deviation theorem with the closed-form sample-size condition

Route-facing finite-prefix finite-class Hoeffding theorem with denominator written directly as (s.card : ℝ)

Route-facing unit-range finite-prefix finite-class Hoeffding theorem with compact log(card/time/budget) / (2 * ε^2) sample-size condition

Route-facing unit-range finite-prefix finite-class Hoeffding theorem with the confidence radius written directly in the deviation event

Route-facing explicit-radius theorem with radius positivity discharged by nonempty sample and strict finite-prefix budget assumptions

Route-facing unit-range finite-prefix finite-class Hoeffding theorem in confidence-radius form

Route-facing explicit-radius theorem for losses bounded in [0,1], removing caller-supplied lower and upper range functions and discharging the negative-integral identity internally

Finite-prefix time-varying dyadic-radius event from supplied pointwise tails and checked dyadic budget conversion

Finite-prefix time-varying dyadic-radius theorem for [0,1] losses with the pointwise tails discharged from Hoeffding

Finite-prefix dyadic finite-class deviation bound from bounded independent empirical-average losses

Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget radius

Shared-sample finite-prefix wrapper using a closed-form horizon/class/budget sample-size condition

Shared-sample finite-prefix wrapper for bounded independent empirical-average losses

Shared-sample finite-prefix wrapper using a radius-style condition and the concrete dyadic real budget

Shared-sample finite-prefix wrapper using one horizon-level radius condition

Shared-sample finite-prefix wrapper using the displayed sample-size Hoeffding budget

Shared-sample finite-prefix wrapper using explicit sample-size lower bounds and the concrete dyadic real budget δ * 2^(-1-t) / card(H)

Shared-sample finite-prefix wrapper using real log budgets below the dyadic ENNReal budget split

Shared-sample finite-prefix wrapper using explicit sample-size lower bounds and real budgets

Shared-sample finite-prefix wrapper using a displayed sample-size Hoeffding budget and time-varying thresholds

Shared-sample finite-prefix wrapper using one combined two-sided Hoeffding budget

Shared-sample finite-prefix wrapper using one uniform range proxy and dyadic time budgets

Shared-sample finite-prefix wrapper with pointwise uniform range width and one closed-form proxy

Shared-sample finite-prefix wrapper with pointwise uniform range width and nondegenerate sample-coordinate certificates

Finite-horizon absolute-deviation shell over all (time, hypothesis) pairs

Finite-prefix absolute-deviation shell using the standard dyadic schedule

Finite-prefix dyadic absolute-deviation shell with time-varying thresholds

Finite-horizon absolute-deviation shell with a supplied time-budget sequence

Finite-horizon absolute-deviation shell with a threshold depending on (time, hypothesis)

Finite-prefix dyadic shell from one-sided upper and lower pointwise tails

Equal-budget union bound over a finite time horizon and finite hypothesis class

Finite-prefix time-class union shell using the standard dyadic schedule

Finite time budgets whose sum is ≤ δ, with each time split across hypotheses

Named dyadic confidence radius for [0,1] finite-class empirical-average deviations

Sample-size lower bound implies the named dyadic confidence radius is at most a target ε

The closed interval [0,1] as a metric index type

Rounded dyadic adjacent-level cover counts are monotone in the scale

Rounded dyadic entropy-at-scale sequence is monotone

Dyadic total-bounded finite net covers the unit interval at the dyadic chaining radius

The reusable dyadic grid center map contains the left endpoint

The reusable dyadic grid center map contains the right endpoint

Floor projection from [0,1] to the level-k dyadic grid

Floor-projected dyadic grid covers [0,1] at spacing radius 1 / 2^k

Generic dyadic finite net has 2^k + 1 centers

Level-1 and level-2 generic dyadic finite-net covering-number product is the first dyadic pair count

Level-1 generic dyadic finite net has 3 centers

Level-2 generic dyadic finite net has 5 centers

Generic dyadic finite net covers [0,1] at spacing radius 1 / 2^k

The first adjacent dyadic grid pair count is 15

Rounded nearest-grid projection from [0,1] to the level-k dyadic grid

Rounded dyadic grid covers [0,1] at half-spacing radius 1 / 2^(k+1)

Rounded dyadic projection fixes the right endpoint

Rounded dyadic projection fixes the left endpoint

Level-k dyadic grid has cardinality 2^k + 1

Rounded generic dyadic finite net has 2^k + 1 centers

Level-1 and level-2 rounded dyadic finite-net covering-number product is the first dyadic pair count

Level-1 rounded dyadic finite net has 3 centers

Level-2 rounded dyadic finite net has 5 centers

Rounded generic dyadic finite net covers [0,1] at half-spacing radius 1 / 2^(k+1)

Total-bounded finite net covers the unit interval at a supplied radius

Explicit half mesh has covering number 3

Explicit three-point mesh covers [0,1] at radius 1/4

Adjacent half/quarter projection-pair family is nontrivial

Half/quarter covering-number product is 15

The half/quarter product is identified with the first adjacent dyadic grid pair count

Explicit quarter mesh has covering number 5

Explicit five-point mesh covers [0,1] at radius 1/8

The packaged finite sub-Gaussian process has the required increment MGF

Supplied-supremum adapter for the packaged rounded unit-interval Dudley instance

The supplied supremum is attained at an endpoint

Coarse finite-horizon m = 0 Dudley bound for the supplied supremum

Constant-envelope first-scale bound evaluated to a scalar expression

First-scale supplied-supremum Dudley bound under an explicit entropy envelope

The supplied supremum has expectation 1/2

The supplied supremum is the least upper bound of the actual process range

The supplied supremum is the least upper bound over the non-finite unit-interval family

Endpoint adapter from the supplied supremum to any rounded dyadic projected finite supremum

The nonzero supplied supremum routes through the projected quarter-mesh Dudley bound

The projected quarter-mesh supplied-supremum bound evaluated to 1 + sqrt 2 * sqrt(log 15)

The nonzero supplied supremum routes through the rounded generic dyadic-grid Dudley bound

The rounded-grid supplied-supremum bound evaluated to 1 + sqrt 2 * sqrt(log 15)

The nonzero supplied supremum routes through the m = 2 rounded dyadic-grid Dudley bound

Named m = 3 supplied-supremum rounded dyadic-grid Dudley corollary

Arbitrary finite-horizon rounded dyadic-grid Dudley bound for the supplied supremum routed through the packaged API

Arbitrary finite-horizon supplied-supremum rounded-grid Dudley bound with the prefix-sup envelope removed

The supplied supremum equals the order supremum of the actual process range

The supplied supremum upper-bounds the full non-finite unit-interval family

Half/quarter projection-pair increment pays the concrete log 15 entropy term

Projected quarter-mesh supremum satisfies the finite-net Dudley bound with a sqrt(log 15) prefix envelope

Projected finite supremum over any rounded dyadic grid equals the supplied supremum

Rounded generic dyadic-grid projected supremum satisfies the finite-net Dudley bound with a sqrt(log 15) prefix envelope

Three-level rounded dyadic-grid projected supremum satisfies the finite-net Dudley bound with reusable adjacent cover counts

Named m = 3 projected rounded dyadic-grid Dudley corollary

Arbitrary finite-horizon rounded dyadic-grid projected supremum Dudley bound routed through the packaged API

Arbitrary finite-horizon projected rounded-grid Dudley bound with the prefix-sup envelope removed

Adjacent-level covering-product envelope for the shifted rounded dyadic sequence

Packaged finite dyadic Dudley instance for the rounded unit-interval grid sequence

Prefix-sup envelope collapses for the rounded dyadic entropy sequence

Shifted rounded dyadic grid index sequence, starting at level 1

Shifted rounded dyadic finite-net sequence for finite-scale Dudley chaining

Adjacent rounded dyadic covering-number product is bounded by the cover-count envelope

Range wrapper for the adjacent rounded-grid covering-product envelope over any finite horizon

Adjacent rounded dyadic covering-number product equals the reusable cover-count envelope

Shifted rounded dyadic finite nets use the Rademacher process metric

Adjacent rounded dyadic projection-pair family is nontrivial at every scale

Range wrapper for nontrivial adjacent projection-pair families over any finite horizon

Adjacent rounded dyadic radii satisfy the geometric chaining radius budget

Range wrapper for the geometric radius budget over any finite horizon

Adjacent rounded dyadic radii have positive sum at every scale

Range wrapper for positive adjacent rounded dyadic radii over any finite horizon

Rademacher linear process increment satisfies the sub-Gaussian MGF bound

The unit interval is totally bounded