Find the theorem before the declaration name.

The wealth of the executable finite wealth-weighted master equals the fixed-prior mixture of supplied expert wealths at every time and path

The finite master competes in log wealth with every positive-prior supplied strategy, paying its explicit log prior-weight cost

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

The exact countable sleeping-expert master is an e-process under legal predictable bets and nonnegative factors

The master competes with every expert after activation, with the explicit dyadic atom cost

The finite active-prefix plus closed-form sleeping tail equals the literal real infinite mixture at every time and path

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

The safe common correction pays at least log |I| on the log scale for the checked diagonal witness

A common positive correction is safe on the diagonal witness exactly when it is at least the catalog cardinality

Exact diagonal-witness characterization: coefficient-corrected selection is safe exactly when the coefficient sum is at most one

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 constructor for e-processes under an explicit product-supermartingale premise

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

One event controls every n >= 4 with the explicit actual-time constant-factor boundary from the polynomially allocated fixed-tilt geometric stitch; the construction is not itself an e-process

Every inclusive block [N,2N] of a nonnegative countable allocation contains an atom no larger than 1/(N+1)

The fair-sign walk exceeds every fixed nonnegative multiple of sqrt n infinitely often almost surely

Gaussian-tail anti-concentration forces an eventual fixed-constant sqrt n boundary floor

Every valid deterministic one-sided fair-sign anytime boundary exceeds every fixed nonnegative sqrt n multiple infinitely often

Conditional reduction from the explicit still-open fair-sign upper-LIL premise to the sharp constant-one limsup floor

Fair-sign normalized sums converge in distribution to the standard Gaussian

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

Positive summable epoch weights pay an explicit iterated-logarithm cost along an unbounded geometric-epoch subsequence

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 finite-grid time-uniform crossing boundary via 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

The telescoping polynomial epoch allocation has total mass exactly one

Exact logarithmic price of the polynomial allocation at geometric epoch times

The countable union of polynomially allocated fixed-tilt geometric-epoch failures has mass at most delta; this confidence allocation is not itself an e-process

The canonical measurable event has probability at least 1 - delta and simultaneously controls the explicit polynomial stitched boundary for every n >= 4

A predeclared-weight correction preserves expectation at most one for an arbitrary observation-dependent selector over a finite nonnegative score catalog

Finite simultaneous tail control under reciprocal corrections satisfying the Kraft budget

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

Concrete positivity and closed-form shape receipt at n = 16, δ = 1/2; no asymptotic-rate conclusion

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

Positive prior weights, legal predictable expert bets, and positive factors make the executable master wealth an e-process

Converts the signed-residual fixed-range event to a supplied pointwise residual envelope, with no empirical-variance term

Gives one fixed-range event simultaneous over positive times, posterior PMFs, and a fixed finite tilt catalog while leaving the encountered signed approximate-Poisson residual explicit

Under true induced-kernel invariance and fixed nuisance inputs, one outer event gives every n >= 2, posterior PMF, and declared finite tilt atom the existing target-policy OPE boundary plus posteriorAverage posterior residualEnvelope

Leaves the encountered signed residual average explicit on one event simultaneous over path, finite tilt atom, posterior PMF, and time, so a second simultaneous event may certify a pathwise residual bound without fixing that bound before the OPE event

Converts a fixed pointwise absolute residual envelope into exactly posteriorAverage posterior residualEnvelope, with no extra importance-ratio, span, horizon, or factor-two multiplier

Identifies the posterior predictable-mean prefix average with (posterior stationary risk + posterior residual average + B) / (C * (1 + 2 * B))

Defines the non-variance-adaptive target-policy OPE boundary with deterministic fixed-range correction lambda / (8 * (1 - lambda / 3))

Averages the true induced-kernel approximate-Poisson residual over the first n encountered states and a posterior PMF

Exposes the raw behavior-law predictable mean as the normalized target-policy Poisson drift at the current observed state, before any exact-Poisson flattening

Arbitrary-measure sub-Gaussian process interface with explicit evaluation measurability and increment/exponential integrability

One-scale square-root entropy bound for an arbitrary finite increment family

Arbitrary-measure projection-pair bound derived from two finite nets and their chosen cardinalities, without MeasureChainingBudget

Nonzero Boolean witness: the one-point-to-full-net projection-pair maximum has exact mean 1/2

Optimized Bochner-integral finite-maximum bound, including singleton families

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

Identifies the complete exported generated candidate table with the three-dimensional table obtained from the compact typed refresh-mixture mass accessor

Derives from the generated refresh-mixture specification that every candidate-kernel cell contains the declared common uniform-refresh mass

Lifts the environment-cell floor through an arbitrary state-Markov target policy to a common uniform minorization of every induced state-kernel row

Bounds the induced target-policy kernel's finite Dobrushin coefficient by the generated candidate weight 5/8, 3/4, or 7/8

Supplies the oscillation-contraction premise used by finite-depth target-policy OPE for every state-Markov target policy

Evaluates the nominal environment under target-policy index 1 as an exact 24-state rational kernel

Identifies every real-valued mass of the constructed PMF with its exact rational table entry

Uses strict Dobrushin contraction to identify the explicit PMF with the canonical noncomputable invariant witness for the corresponding catalog atom

Proves the explicit PMF invariant for the nominal candidate and queue-threshold target policy

Checks that the explicit 24-entry rational mass vector is nonnegative and sums to one

Rewrites the same exact risk through the canonical invariant witness and score stored in the twelve-atom catalog

Evaluates the exact one-step Brier row-risk vector for target-policy index 1 and fixed-predictor index 2

Proves that the explicit stationary Brier risk is exactly 4338268437 / 67816493056, hence below 13/200

For each fixed true refresh parameter and initial observation, intersects the fixed-range risk and persistence events and controls the selected stationary risk at every positive time on one event of complement outer mass at most 1/20

For a true refresh parameter and initial observation fixed beforehand, gives one two-sided persistence-hit event over all positive times with complement outer mass at most the supplied budget

Instantiates the selected controlled-queue risk boundary with the fixed tilt 1/16 and risk budget 1/40, without an empirical-variance term

Combines the selected fixed-range risk boundary with the checked affine refresh-sensitivity residual

Instantiates the scalar persistence-hit radius with tilt 1/64 and persistence budget 1/40

Specializes the twelve-atom approximate target-policy OPE theorem to the generated fixed initial observation (action = 1, state = 1), singleton tilt 1/16, and failure mass at most 1/40; the event is simultaneous over posterior PMFs and times n >= 2

Converts the exact aligned 24 x 2 x 24 suffix-edge-histogram premise into the selected score sum and squared-score sum, preventing the off-by-one ambiguity that those two scalar moments alone cannot detect

Evaluates the selected queue-threshold/nominal-model depth-twelve boundary plus its exact residual envelope below the generated rational d9 receipt

Combines the aligned histogram calculation with the event inequality to prove the selected stationary risk is below 7/100

Combines candidate-drift oscillation, sensitivity oscillation, and a hit-discrepancy budget eta into the residual epsilon + sensitivityBound * eta, with no extra 2 * (1 + B) multiplier

For any true refresh parameter and deterministic initial observation fixed beforehand, intersects the fixed selected-atom risk and persistence events and bounds the stationary target-policy risk on one adaptive-trajectory outer event of complement mass at most 1/20 at every n >= 2

Freezes true gamma = 149/200, initial observation (eco, state 0), horizon 200000, nominal candidate, supplied shifted depth-twelve potential, and queue-threshold/nominal-model Dirac posterior for the stationary target-policy risk on an adaptive trajectory; it is an event theorem, not a trace or numerical receipt

For every fixed admissible refresh parameter under the path law started at (action = 1, state = 1), supplies an outer event of complement mass at most 1/20 on which any path with the aligned retrospective histogram receives the exact sharp endpoint; it is not a simultaneous-in-parameter event or a named-path membership theorem

Certifies the exact rational upper bound 58989951 / 9007199254740992 for the nominal selected candidate drift directly from the candidate, target-policy, score, transition, and shifted depth-twelve potential tables, without the invariant law, stationary risk, or generated residual table

Certifies the exact rational upper bound 831542406207231 / 3236962232172544 for the selected normalized refresh sensitivity

Defines the exact target-policy Poisson-drift slope in the observable persistence-hit coordinate, including the 24/23 conversion from the latent refresh parameter

For any path matching a supplied physical transition histogram at horizon 200000, bounds the frozen sharp primary boundary by the exact count-derived affine-Bessel endpoint with risk log/psi bounds 9 and 1/480 and persistence log/psi bounds 7 and 1/8064; it contains no future histogram or threshold result

Defines the pathwise sharp residual as the two checked oscillation bounds combined with the nominal candidate's scalar persistence budget

Bounds the sharp structured pathwise endpoint by 0.068710707605557... < 0.069 from the aligned retrospective histogram

For each fixed admissible refresh parameter under the path law started at (action = 1, state = 1), bounds by 1/20 the outer mass of the paths on which the aligned frozen histogram occurs while the displayed risk conclusion fails; the failure set is not asserted measurable, and the statement is neither histogram-conditioned nor simultaneous-in-parameter coverage

Derives the selected score moments and persistence-hit count 152266 from the existing aligned 199999-transition suffix histogram

Checks the exact risk-plus-residual ledger against 45318758321311224310665458696783373002366549 / 659558894102351266671449077672292808728248320 using no true parameter, invariant law, or exact stationary risk

Identifies true refresh-family drift minus generated-candidate drift exactly as hit-probability discrepancy times the normalized sensitivity, with no TV factor two

Identifies the catalog's chosen invariant PMF as the unique invariant law for its generated refresh-family kernel; it does not compute a stationary-risk value

Bounds the Dobrushin coefficient of every target-policy kernel in the refresh family by its persistence parameter; it does not claim equality

Uses the strict refresh-parameter bound to prove existence and uniqueness of an invariant PMF for every state-based target policy; it does not compute the PMF

Specializes the adaptive-trajectory risk event to the predeclared 21 candidate--depth atoms, fresh uniform four-tilt allocations, separate 1/40 budgets, and one outer complement of mass at most 1/20

Makes path/time-dependent substitution explicit for candidate--depth atom, risk tilt, persistence tilt, and posterior PMF, all restricted to catalogs fixed before the event

Allocates risk confidence over an arbitrary finite predeclared candidate--depth catalog, intersects those signed-residual OPE events with scalar persistence confidence on the same path, and permits catalog atom, two tilt atoms, posterior, and time selection inside the common event

Checks the fresh uniform 1/21 Lean allocation over all three generated candidates crossed with generated depths [0,1,2,3,5,8,12]

Gives each generated candidate and finite depth its own closed Poisson-potential span using that candidate's checked persistence contraction and the universal fixed-Brier row-risk envelope D = 1

Proves every admitted risk and persistence tilt satisfies the strict < 1 event premise

Binds the admissible generated tilt prefix [1/16,1/8,1/4,1/2] and proves positivity; the generated terminal atom 1 is excluded

Identifies each of the three generated candidate kernels with its corresponding member of the structured refresh family

Gives one outer-mass event, for true gamma and initial observation fixed beforehand, that controls the direct/complement hit statistic at every declared tilt atom and every n >= 2

Transfers the scalar event to simultaneous physical-row TV budgets for all three candidates; candidate, tilt atom, and time are quantified after the common event

Proves that the controlled transition hit statistic has row-independent conditional mean (1 + 23 * gamma) / 24; a hit can also arise from uniform refresh and is not the persistence indicator itself

Constructs the arbitrary-parameter physical kernel (1 - gamma) * Uniform24 + gamma * delta_step for fixed gamma in [0,1) and exposes every real-valued mass

Lifts exact uniform behavior mass 1/2 to pointwise history-interface overlap for all four generated target policies

Lifts the generated target-policy mass bound 3/4 to the exact controlled importance-ratio cap 3/2

Proves the generated normalized control cost lies in [0,1]

Instantiates the generic envelope D = 1 uniformly over all generated candidates, target policies, fixed predictors, and reference PMFs; it does not claim the sharper candidate-specific constants

Identifies each of the three fixed queue predictors with squared error against the generated binary overload outcome

Proves every fixed-predictor Brier score lies in [0,1]; the two causal Beta predictors remain outside this stationary-score interface

Instantiates one 19/20 outer event for the fixed nominal candidate, all twelve posterior atoms, and any depth fixed before the event, under positive visit mass for every augmented source row; the residual is (3/4)^m + 4 (1 + B_m) etaAug

Identifies the uniform prior on the four generated target policies paired with the three fixed Brier predictors as mass 1/12 per atom

Supplies a canonical noncomputable invariant PMF for each true target-policy kernel on the finite physical state space; it proves neither uniqueness nor an explicit stationary-risk value

Specializes the nominal candidate's checked contraction upper bound to 3/4 for every one of the twelve policy--predictor atoms

Checks that the fresh uniform prior covers all 48 * 48 * 2 = 4608 augmented transition coordinates with mass 1/4608 each

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

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

Finite multiscale chaining decomposition in expectation

Finite projected-supremum chaining without an identity terminal projection

Generic totally bounded continuous Dudley capstone with the cardinal-minimal dyadic adjacent-product envelope

Generic totally bounded continuous Dudley capstone with pure genuine minimal-cover entropy in the conclusion, paid by shifted boundary certificates and constants

Generic totally bounded continuous Dudley capstone with the selected-cover-count envelope integrand, not genuine minimal covering number

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 shifted dyadic upper sums are bounded by the pure entropy integral with explicit shift constants

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

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

Projected finite-chain Dudley wrapper threaded through the cardinal-minimal dyadic net schedule

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

The shifted one-radius minimal-cover entropy dominates the finite prefix-envelope sample

Adjacent-product entropy is bounded by sqrt 2 times one shifted minimal-cover entropy

Adjacent cardinal-minimal dyadic cover count equals the product of genuine minimal covering numbers at the sampled radii

Adjacent cardinal-minimal dyadic cover products are bounded by the next smaller-radius minimal covering number squared

The dyadic minimal-net schedule has genuine minimal covering count at each sampled radius

Cardinal-minimal dyadic adjacent-product entropy staircase satisfies the guarded closed-annulus condition

The bundled finite net built from the minimal cover has covering count equal to the genuine minimal covering number

Chooses a cardinal-minimal finite metric cover from the genuine minimal covering-number witness

The chosen finite metric cover has cardinality exactly equal to the genuine minimal covering number

Every finite metric cover has at least as many centers as the chosen minimal cover

Genuine minimal finite metric covering number for a nonempty totally bounded metric index space

Genuine minimal covering numbers are antitone in the positive radius

The genuine minimal covering number is bounded by each selected dyadic finite-net count

Any finite metric cover with at most n centers bounds the genuine minimal covering number by n

The selected dyadic envelope dominates the genuine minimal covering number at sampled dyadic net radii

Nonempty totally bounded spaces have positive genuine minimal covering number at positive radius

The genuine minimal covering number is realized by a finite metric cover

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

The induced entropy staircase satisfies the guarded closed-annulus condition

Dyadic samples dominate the finite entropy prefix envelope used by total-bounded finite wrappers

Half-open real-radius selected-cover-count staircase for the total-bounded dyadic net schedule

The selected-cover-count staircase has a finite ℕ∞ surface

The staircase samples the monotone prefix envelope of selected adjacent dyadic cover-count products at dyadic radii

Minimal-schedule boundary certificates give the guarded dyadic upper-sum input

Boundary certificates give the guarded dyadic upper-sum input for the selected-cover-count entropy profile

Unit-interval non-vacuity witness for the cardinal-minimal dyadic cover-count envelope

Concrete non-vacuity witness for the chosen minimal finite cover on the unit interval

Concrete non-vacuity witness for the genuine minimal covering number on the unit interval

Unit-interval non-vacuity witness for the shifted minimal-cover entropy profile

Concrete non-vacuity witness for the generic selected-cover-count surface on the unit interval

Unit-interval non-vacuity witness for the selected-cover-count envelope surface

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

Identifies the normalized behavior-law predictable mean with target one-step conditional risk at the encountered prefix

Pointwise path/time/posterior-dependent posterior and tilt substitution into the simultaneous event

One outer event controls every n >= 2, posterior PMF, and finite declared tilt atom for a known homogeneous environment

Comparator event for history-dependent targets and a known full-prefix environment kernel

Converts the posterior predictable-mean prefix average to posterior encountered target risk

Exact conditional mean under a known prefix/time-dependent controlled environment

Pointwise selector corollary for the prefix-environment event

Finite source--destination coordinate together with the direct or complement side

Maximum candidate discrepancy plus countable-catalog row radius

Kernel budget vanishes only with positive row frequencies and vanishing candidate discrepancies

Countable-catalog row radius in total-variation scale

Complete row-TV statistical radius vanishes under the same visit-frequency condition

Direct or complement coordinate boundary for one natural-number geometric tilt atom

Explicit geometric-atom coordinate boundary tends to zero along every path

Two-sided countable-catalog coordinate radius normalized by source visits

Normalized coordinate radius vanishes under positive limiting source frequency

Maximum candidate row discrepancy plus statistical radius across all source states

Empirical row discrepancy between a candidate kernel and observed transition frequencies

Visited-row empirical transition frequency

Sum of simultaneous coordinate radii on the probabilists' TV scale

Gives a kernel-wide candidate TV budget when every row is visited

Certifies every candidate row on the same countable event

One outer-mass event controls all times, coordinates, and natural-number tilt atoms

Gives every visited row a normalized countable-catalog frequency band

Selects the explicit sample-size geometric atom and retains coordinate-boundary convergence

Gives one uniform candidate-kernel row-TV budget when every source row has been visited

Certifies a row-TV ball for every candidate kernel introduced after the common event

One outer-mass event gives two-sided predictable-versus-observed bands for every coordinate and time n >= 2

Normalizes the common coordinate event on every row with positive visit mass

Combines selected kernel validity with conditional vanishing of its countable TV budget

Substitutes a selected candidate kernel inside the common event

Substitutes a path- and time-selected candidate row without a new event

Explicit path- and time-selected candidate specialization with no additional selection cost

Combines a selected candidate's empirical row-TV budget with Dobrushin perturbation, true-kernel contraction, and uniqueness among supplied invariant PMFs

Dirac-posterior empirical-Bernstein boundary for one direct or complement coordinate

Two-sided coordinate radius normalized by positive source visit mass

Observed source--destination transition count over the first n transitions

Observed source-state visit count over the first n transitions

Supplies the uniform absolute bound for [0,1] squared losses

Bounds average conditional risk by observed prequential loss plus the declared sub-Gamma boundary outside that event

Establishes integrability under the actual finite Markov path law

Embeds the risk-facing posterior failure event into the generic time-uniform PAC-Bayes process failure event

Gives one measurable exceptional event of ordinary probability at most delta

Proves measurability of the hull used for the public confidence event

Shows that the measurable hull contains every raw posterior-existential violation

Risk-facing event in which some declared tilt, posterior, and positive time violates its exact prior-weight boundary

Embeds the Markov risk-facing event into the finite hypothesis--tilt master-process failure event

Measurable hull of the Markov posterior/time/tilt failure event

Gives one measurable exceptional event containing every all-time/all-posterior/all-tilt violation, with ordinary probability at most delta

Proves measurability of the shared finite-tilt Markov exceptional event

Measurable hull of the shared failure set under the supplied random-initial path law

Bounds the measurable random-initial exceptional event by the unchanged confidence level delta

Proves measurability of the random-initial-law exceptional event

Shows that the measurable hull contains every raw posterior/tilt violation

Shows the raw posterior/time/tilt failure set lies inside the random-initial measurable hull

Controls the raw all-time, all-posterior Markov failure set in outer probability at fixed tilt

Publication-facing finite-catalog theorem with a measurable common event, all-time and all-posterior validity, and explicit KL penalty

Controls the raw all-time, all-posterior, finite-tilt Markov failure set in outer probability through one master e-process

Controls the shared all-time, all-posterior, all-tilt raw failure set under the mixed random-initial path law

Publication-facing measurable certificate simultaneous over all positive times, posteriors, and declared finite tilt atoms

Publication-facing finite-state certificate for any supplied initial PMF, simultaneous over positive times, posteriors, and declared tilt atoms

Mixes the checked deterministic-start finite Markov path laws against a supplied finite-state initial PMF

Registers the mixed random-initial path law as a probability measure

Recovers the deterministic-start Markov path law from a point-mass initial PMF

Transfers a common raw-set mass bound from every deterministic start to any supplied finite initial PMF without a union bound

Outside the common event, controls every posterior and every positive time by empirical prequential risk plus KL and the sub-Gamma boundary

Gives the weighted finite-tilt Markov prequential-risk bound outside the random-initial common event

Permits pointwise post-path selection of one predeclared tilt atom under the random-initial common event

Outside the shared event, every declared tilt and posterior obeys the weighted Markov prequential-risk boundary

Pointwise post-path selection of one predeclared tilt atom on the common event; no measurable or adapted selector and no added optional-stopping result

Gives one measurable all-time finite-grid exceptional event with probability at most delta

Centers observed loss minus transition-row conditional risk under the generated filtration

Conservative unit conditional-second-moment bound retained as a simple compatibility lemma

Sharp universal 1/4 conditional-second-moment bound for the centered [0,1] one-step loss

Derives conditional centering of the risk shortfall from the Markov path-law identity

Transfers the sharp universal 1/4 conditional-second-moment proxy to the risk shortfall

Preserves increment adaptedness under the risk-shortfall sign change

Establishes measurability of every catalog member's risk-shortfall increment

Derives the next-step squared-loss conditional expectation from the finite transition PMF and its Ionescu--Tulcea path law

Identifies the posterior-averaged shortfall with posterior conditional risk minus posterior empirical prequential risk

Identifies the innovation mean with observed prequential risk minus average conditional risk

Reorients the Markov innovation as conditional risk minus observed loss, the sign required for an upper-risk certificate

Rewrites the 1/4-variance sub-Gamma contribution as lambda / (8 * (1 - lambda / 3))

Identifies the normalized behavior-law conditional risk with the declared target-policy transition risk under overlap

Expands the behavior-policy/environment continuation mass into its action and outcome factors

Packages the boundedness, adaptedness, predictable mean, and conditional-expectation interfaces for a finite predeclared target-policy catalog

Proves the exact filtration-conditional mean of the observed normalized one-step importance score

Shows the importance-weighted observation is measurable at the next filtration level

Shows the target-policy transition mean is predictable from the completed prefix

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

Identifies the permutation average of the canonical random-matching statistic with Bessel sample variance

Averaging any fixed nonempty catalog of distinct coordinate pairs over all permutations recovers Bessel sample variance

One-coordinate population-variance Bernstein MGF for arbitrary finite [0,1] losses

Outside the risk event, bounds every posterior risk gap by KL complexity and posterior-averaged population variance

Normalized finite-IID population-risk deviation MGF with exact 1 - lambda/(3n) denominator

Finite union of population-risk bad sets with separately weighted risk budgets

Bounds the separate fixed-lambda population-risk bad event by its declared risk budget

Membership in the risk catalog is equivalent to membership in one fixed-lambda event

A sample is outside the risk catalog exactly when it is outside every fixed-lambda event

Weighted union bound for the finite population-risk tilt catalog

One exceptional set joining the variance and risk catalogs

Bounds the union of variance and risk bad events by deltaVariance + deltaRisk without independence

Combined catalog mass bound deltaVariance + deltaRisk without a Cartesian-pair confidence charge

Per-hypothesis Bessel-corrected empirical loss variance

Every fixed empirical-variance tilt event is contained in the catalog event

Bounds one fixed-sample, fixed-tilt exceptional set by delta; the event is shared by every finite posterior

Finite union of empirical-variance bad sets with separately weighted variance budgets

Exact second-order pair-statistic representation of Bessel empirical variance

Averages the normalized per-hypothesis empirical-variance moment under a finite prior

Source-facing self-bound V_n <= n/(n-1) * Rhat_n for [0,1] losses

Universal 1/2 bound for Bessel empirical variance of a finite [0,1] sample

Random-matching and finite-Jensen lower-tail MGF bound, with the exact disjoint-pair count in its coefficient

All-n >= 2 source-normalized finite-IID empirical-variance MGF inequality

Membership in the variance catalog is equivalent to membership in one fixed-tilt event

Bessel-corrected empirical loss variance is nonnegative for sample size at least two

Moves the deterministic variance penalty inside the exponential to obtain the normalized moment used by change of measure

A sample is outside the variance catalog exactly when it is outside every fixed-tilt event

Unrearranged posterior-uniform variance gap bound for every catalog entry

End-to-end finite-IID unbiasedness of the per-hypothesis Bessel empirical loss variance

Weighted union bound for the finite empirical-variance tilt catalog

Factors the finite-product expectation of a product over disjoint pair blocks into independent two-coordinate expectations

The independent-pair half squared-difference kernel has expectation equal to population variance

Normalized second-order pair-statistic form of empirical variance

Places the population risk of a finite [0,1] loss in [0,1]

Per-hypothesis population loss variance under a finite weight function

Identifies population loss variance with the second moment minus squared risk

Gives the universal 1/4 population-variance bound for finite [0,1] losses

Population loss variance is nonnegative under a finite PMF

Two distinct coordinates of the finite IID product sample have the product marginal

Expected squared loss difference across two distinct IID coordinates is twice the population variance

Plain-sum finite weighted union bound stated through an existential membership cover, avoiding decidable-instance reconciliation

Ordered sum of squared differences across distinct sample indices

Equates the ordered off-diagonal square-difference sum with twice the sample size times the centered sum of squares

Bounds the ordered pair numerator for samples in [0,1]

Outside the shared event, bounds the posterior average of per-hypothesis population variances by the corresponding empirical average and KL-confidence penalty

Rearranged observable variance certificate for every catalog entry and posterior

Valid sample- and posterior-dependent selection from the finite variance-tilt catalog

Final fixed-parameter observable empirical-Bernstein risk bound simultaneous over every finite posterior

Observable risk bound simultaneous over every pair of predeclared variance and risk tilts

Valid sample- and posterior-dependent selection from separate finite variance and risk catalogs

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

Lower-tail score -t * ell i z for a finite bounded loss

Support-aware countable-catalog bad-sample set containing every product-law null sample

Nat-indexed weighted mixture of the fixed-sample prior score moments

Nonnegativity of the countable master mixture under nonnegative weights

The support-aware countable-catalog bad set has product-law mass at most delta

A normalized countable catalog has master-mixture expectation at most one

Expected countable master mixture is at most the total tsum of catalog weights

A good sample has positive product mass and master mixture below 1 / delta

Raw retained-variance posterior-gap inequality for every entry of the predeclared countable tilt-pair catalog

Exact-residual posterior-risk bound for a positive-tilt entry on the same fixed-sample event

Sample- and finite-posterior-dependent natural-index selector with one shared event and one KL term

Every finite-hypothesis posterior and Nat-indexed catalog entry obey the Donsker--Varadhan score bound on the shared event

Outside one countable event, every entry keeps its prior moment within its positive weight share

Summability of the weighted prior-moment series on every positive-product-mass sample

A concrete finite dyadic grid approximates the continuous scale optimizer by (5/4) * sqrt(2AV) + A/2

Partition sum for the specialized lower-tail bounded-loss tilt

The partition sum of a nonnegative bounded-loss lower-tail tilt is at most one

Finite PMF obtained by reweighting with exp (-t * ell i z)

The specialized lower-tail bounded-loss tilt is a PMF without a full-support assumption

Finite-product lower-tail loss change of measure, specialized from the generic identity

One-coordinate lower-tail loss change of measure, specialized from the generic identity

Pointwise density comparison exp (-t) * p z <= q_t z for losses in [0,1]

Negative Bessel empirical-variance moment bound under the lower-tail tilted finite PMF

Retained-affine-factor Bennett bound for the centered lower-tail loss score

Predeclared dyadic scale 2 / 2^j used by the finite optimizer catalog

Direct square-root-plus-linear posterior bound for a finite dyadic grid reaching the optimizer

Rational variance tilt s² / (2(1 + 2s)) satisfying the checked balance condition for 0 < s ≤ 2

Canonical catalog depth clog 2 n for the closed-form endpoint

The fixed depth clog 2 n automatically reaches every posterior's empirical-variance optimizer scale

One shared finite-scale event has product-law mass at most delta

One bad-sample set for the canonical logarithmic scale grid

The canonical logarithmic-grid exceptional set has product-law mass at most delta

Closed-form one-KL empirical-Bernstein PAC-Bayes bound with explicit 5/4 square-root and 5/2 linear constants

Mean tilt s / (1 + 2s) attached to a declared empirical-Bernstein scale

Exact scale-form one-event bound Rhat + L/(sn) + 2L/n + (s/2)Vhat with post-sample posterior and scale selection

Finite partition sum for an arbitrary exponential score under a base weight function

The finite exponential-tilt normalizer is positive under any PMF, without a full-support assumption

Base weight function reweighted by an exponential score and divided by its partition sum

Normalizing an exponential tilt of a finite PMF produces another PMF

Pointwise cancellation recovers the unnormalized exponential weight

Exact one-coordinate finite change-of-measure identity for arbitrary observables

Single catalog bad-sample set thresholding the master mixture at 1 / delta

Linear-minus-quadratic variance coefficient in the fixed-sample joint mean/Bessel-variance exponential moment

Nonnegativity of the joint variance coefficient on the exact range η × n ≤ 2 × (n − 1)

Unnormalized fixed-sample joint lower-tail mean and Bessel empirical-variance exponential-moment bound

Prior-and-catalog master mixture over the weighted per-entry prior score moments

Prior moment of the joint score at one sample and one catalog pair

Bennett coefficient in the retained population-variance residual

Nonnegativity of the Bennett residual coefficient for every real tilt

Retained logarithmic population-variance residual per observation

Transported population-variance coefficient per observation

Nonnegativity of the transported residual rate under a nonnegative joint MGF coefficient

The piecewise residual formula bounds every variance in [0, 1/4]

Per-hypothesis normalized fixed-sample joint mean/empirical-variance score

Exact three-branch maximum of the retained residual on the bounded-loss variance interval

A branchwise maximizer attains the residual envelope on [0, 1/4]

Closed form of the interior-stationary-point residual branch

Closed form of the endpoint-at-one-quarter residual branch

Closed form of the zero-maximizer residual branch

The piecewise formula is the exact greatest retained residual on [0, 1/4]

Nonnegativity of the exact residual maximum

Every declared scale 0 < s ≤ 2 produces an admissible zero-residual joint pair

The explicit rational variance tilt absorbs the joint Bennett residual for 0 ≤ t ≤ 2/5

The single catalog bad set has product-law mass at most delta

Zero-residual coefficient balance absorbs the retained Bennett logarithm at every nonnegative variance

Master mixture expectation is at most the total catalog weight, hence at most one

Normalized fixed-sample joint score has finite-product expectation at most one

Division form of the retained-variance inequality for a strictly positive mean tilt

Division form of the selector endpoint for all-positive mean tilts

Raw retained-variance posterior inequality with the Bennett log at the posterior-averaged variance

Selector endpoint: the catalog entry may depend on the sample and the posterior

Explicit one-KL empirical-Bernstein posterior-risk bound for one balanced catalog entry

Sample- and posterior-dependent selector form of the zero-residual risk bound

One-event one-KL empirical-Bernstein posterior-risk bound with the exact residual penalty

Sample- and posterior-dependent selector form of the exact-residual risk bound

One-KL Donsker-Varadhan score bound for every posterior and entry on the good event

Prior score moment has finite-product expectation at most one

Outside the one event, each entry keeps its prior moment at most 1 / (delta * w c)

Population risk minimizes the finite-PMF weighted squared error

Tilted population variance is at least exp (-t) times the base population variance

Exact finite-product exponential change-of-measure identity for arbitrary sample functionals

Pointwise identity relating the base product weight, the summed exponential score, and the tilted product weight

Exact finite-PMF squared-error decomposition around an arbitrary center

Posterior-averaged bounded-loss population variance remains in [0, 1/4]

Upgrades existence to uniqueness under a strict candidate row-TV contraction certificate

Upgrades finite-state existence to a unique invariant PMF under strict true-kernel Dobrushin contraction

Uses compactness and the vanishing Cesaro defect to construct a simplex fixed point

Every kernel on a nonempty finite state space has an invariant PMF

Noncomputable chosen invariant PMF supplied by finite-state existence

Proves invariance of the chosen finite invariant PMF

Cesaro orbit average packaged in the finite probability simplex

Real coordinate vector of the Cesaro average of the finite-kernel orbit

Iterates the simplex push-forward from a supplied starting distribution

Linear push-forward of real state weights through a finite Markov kernel

Kernel push-forward as a self-map of the finite real probability simplex

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

Rewrites a finite-horizon target payoff as a likelihood-weighted behavior payoff

Proves the exact finite-prefix target-versus-behavior likelihood-ratio identity

Identifies the recursive finite-prefix expectation with the corresponding marginal integral under the actual infinite trajectory law

Bounds the cumulative weight by C ^ n under a supplied one-step ratio cap

Recovers target terminal-state occupancy from the weighted behavior path law

Gives the measurable finite-prefix cylinder probability identity

States the change of measure directly for the actual infinite target and behavior trajectory laws

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

Constructs the depth-m target-policy Poisson potential from a fixed candidate environment and supplied candidate reference PMF, without assuming that reference is invariant

For fixed true and candidate environments, target-policy catalog, candidate references, physical action-row TV radius, oscillation data, and depth, one behavior-law outer event controls every n >= 2, posterior PMF, and declared finite tilt atom by the target-policy OPE boundary plus the posterior average of the constant envelope alpha^m D + 2 (1 + B_m) etaEnv, which equals that envelope for a posterior PMF

Transfers the ordinary finite-depth geometric-decay lemma to the candidate target-policy drift and bounds its oscillation by alpha^m D

Bounds the exact selected continuous-posterior boundary by an observable LIL-order envelope

Proves vanishing selected width under absolute continuity, log-density integrability, and the displayed posterior-KL growth condition

Forms one real-tsum e-process from a positive normalized countable tilt catalog and a probability prior on an arbitrary measurable hypothesis space

Proves that the normalized positive Nat-indexed mixture of finite-hypothesis predictable-residual components is one e-process

Forms one e-process from a fixed normalized countable catalog of legal predictable tilt strategies and a finite model prior

One outer-mass event over an arbitrary measurable hypothesis space controls every n >= 2, eligible posterior measure, and atom of a finite predeclared tilt prior

One event supports path- and time-selected continuous posteriors, exact growing-prefix tilt minimization, ordinary conditional-mean control, and the conditional vanishing conclusion

One outer-mass event controls every n >= 2, declared countable tilt atom, and eligible continuous posterior measure

One outer-mass event controls every n >= 2, finite posterior PMF, and atom of a predeclared positive normalized countable tilt catalog

Allows exact post-data minimization over any declared finite prefix while retaining the single countable master event and explicit atom-weight cost

One event supports ordinary conditional-risk bounds for every declared predictable strategy atom, finite model posterior, and time with positive accumulated exposure

One-event capstone simultaneous over every n >= 2, posterior PMF, and declared finite tilt atom

One atTop event controls every n >= 2 and every atom of a predeclared finite positive tilt catalog

IID risk-facing capstone with the same all-time, all-posterior, all-atom common event

Specializes to path-selected factorized posteriors and displays the model and strategy selection costs separately

Allows an arbitrary joint finite model--strategy posterior to depend on the observed path and reporting time on one common event

Returns an ordinary posterior-averaged conditional-risk bound for every finite model and shared predictable-strategy posterior, with separate KL charges

Uses the polynomial-weight geometric catalog and explicit sample-size selector to obtain simultaneous validity and an exact selected boundary tending to zero

One event combines path-selected finite posteriors, exact growing-prefix tilt minimization, an ordinary unweighted conditional-mean bound, the LIL-order envelope, and vanishing width

Bounds the outer mass of the single master crossing event by delta

Mixes the actual predictable-residual processes over finite full-support hypothesis and tilt priors into one e-process

Allows path-, time-, and posterior-dependent selection of a declared tilt atom, with one hypothesis KL and the atom log-weight penalty

Makes the stochastic distinction explicit: the hybrid Bessel exponential expression is a pointwise lower envelope of the actual e-process

Packages the actual lower-tail predictable-residual exponential process as an e-process under boundedness, adaptedness, and the conditional-mean model

For 0 <= lam < 1, bounds the forward empirical-Bernstein cumulant by lam^2 / (2 * (1 - lam)); the sharp queue slice uses it to certify the fixed 1/16 and 1/64 tilt costs

Bounds the predictable squared-residual penalty by the smaller of two checked Bessel envelopes for every bounded path and n >= 2

Allows the empirical-Bernstein tilt to vary predictably with time and the observed past while preserving the e-process property when 0 <= lambda_k <= L < 1 under the bounded conditional-mean model

Under the same predictable range 0 <= lambda_k <= L < 1, controls the probability that the process crosses 1 / alpha at any time up to an arbitrary finite horizon by alpha

Bounds the selected exact observable hybrid-Bessel boundary by an explicit square-root LIL-order envelope

Proves the selected exact boundary tends to zero for arbitrary time-varying finite posterior PMFs

Derives the per-hypothesis conditional mean from the natural-filtration IID bounded-loss model

Decomposes the KL of a factorized model--strategy posterior against the product prior into separate model and strategy KL terms

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))

Requires a trajectory score to be jointly strongly measurable in the complete prefix and next state on an arbitrary measurable state space

Bounds the centered innovation in absolute value by one for [0,1] scores

Identifies the next-coordinate law of a trajectory continuation with the probability kernel selected by its complete finite prefix

Derives the exact prefix-conditional expectation of an arbitrary fixed [0,1] prefix/next-state score under the generated finite-state path law

Derives the exact prefix-conditional score expectation for deterministic-start arbitrary-state full-prefix kernels

Recovers the existing homogeneous-Markov squared-loss conditional-expectation statement from the prefix-dependent semantic theorem

Identifies the existing finite Markov path measure as a definitional specialization of the prefix-dependent trajectory measure

Proves conditional centering from the trajectory law rather than assuming a martingale-difference property

Proves conditional centering of the arbitrary-state trajectory innovation from the generated path law

Gives the universal 1/4 conditional second-moment bound for the centered [0,1] score

Derives the sharp universal 1/4 conditional second-moment proxy without a finite-state assumption

Shows that observed score minus prefix-conditional risk is measurable at the next filtration level

Identifies the existing Markov squared-loss innovation as a definitional specialization of the general trajectory innovation

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²))

Effective-growth 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

Two-sided homogeneous product bounded-differences tail P(|f - E[f]| >= ε) <= 2 exp(-2ε² / sum_k c_k²)

Two-sided heterogeneous-law product tail P(|f - E[f]| >= ε) <= 2 exp(-2ε² / sum_k c_k²)

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

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

Effective-growth two-sided uniform deviation with sharp one-sided tails

Pointwise effective-growth bound Rad <= B * sqrt(2d * log(en/d) / n)

Effective-growth ERM excess-risk tail with sharp concentration term

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

Bounds the canonical continuous-prior dyadic-scale reverse-epoch event by delta

Gives the closed-form 5/4, 5/2 empirical-Bernstein bound at every prefix for every absolutely continuous posterior with integrable log-likelihood ratio

Measure-KL complexity with the telescoping dyadic-epoch confidence penalty at sample size n

The posterior-independent continuous-prior event on the infinite IID path space has mass at most delta

Outside the stitched event, the 5/2 square-root plus 5 linear bound holds at each n >= 2 for every admissible posterior measure

Integrates a prior-a.e. family of submartingales over an arbitrary probability prior under explicit product-integrability obligations

Bounds the continuous-prior reverse-epoch maximal event without assuming an integrated MGF or crossing bound

Places a predeclared finite tilt catalog inside one continuous-prior reverse-epoch event of mass at most delta

Permits prefix-, path-, and posterior-dependent selection from the fixed tilt catalog for every admissible posterior measure

Derives the continuous-prior reverse joint mean/Bessel-variance mixture submartingale from measurable bounded losses

Researcher-facing one-event theorem simultaneous over all n >= 2 and all admissible posterior measures on an arbitrary measurable hypothesis space

Researcher-facing one-event theorem simultaneous over all sample sizes n >= 2 and all posterior PMFs on the fixed finite hypothesis type

Bounds the canonical dyadic-scale reverse-epoch exceptional event by delta

Closed-form empirical-Bernstein posterior-risk bound at every prefix in one finite reverse epoch

One-KL complexity with the telescoping dyadic-epoch confidence penalty at sample size n

The single stitched infinite-path exceptional event has mass at most delta

Outside the stitched event, the displayed 5/2 square-root plus 5 linear bound holds at each n >= 2 for every finite posterior

Shows that a finite prefix of the infinite IID product stream has the corresponding finite product law

Pulls countably many finite-prefix failure sets to the infinite product space and sums their mass budgets

Identifies the shorter-prefix Bessel variance with the conditional expectation of the next-prefix variance under the reverse exchangeable filtration

Packages prefix Bessel variances as a finite reverse martingale

Bounds one finite reverse-epoch event that is simultaneous over every prefix in the epoch and every finite posterior

Mixes a predeclared finite tilt catalog inside one reverse-epoch maximal event of mass at most delta

Permits prefix-, sample-, and posterior-dependent selection from the fixed reverse-epoch tilt catalog

Exponentiates the reverse joint mean/Bessel-variance score into the nonnegative submartingale used by the epoch maximal argument

Gives the retained-variance posterior-risk inequality at every prefix outside the reverse-epoch event

Intersects the signed-residual OPE event with empirical transition confidence for the augmented behavior chain; under exact behavior mass 1/2, every visited augmented row yields a physical action-row budget 2 * etaAug and the final residual alpha^m D + 4 (1 + B_m) etaAug, outside the importance-weighted OPE boundary

Selected boundary combining hybrid-Bessel/KL, endpoint, candidate residual, and row-TV transfer terms

Displays the candidate--depth--geometric-tilt confidence allocation in the logarithmic term

Countable union of depth-atom failures for one candidate

Sums the polynomial depth allocation for one candidate

Unit-normalized trajectory score for one declared candidate and depth

Keeps every declared candidate--depth corrected score in [0,1]

Risk failure set for one declared candidate and finite depth

Charges one candidate--depth atom its declared share of risk-event outer mass

Finite union of candidate failures for the predeclared risk catalog

Bounds the full predeclared catalog risk event by deltaRisk

Candidate-specific finite-depth potential fixed by the declared catalog

Closed candidate-specific span bound at a declared finite Poisson depth

Gives every candidate, depth, risk tilt, time, and finite posterior its stationary-risk bound outside the common risk event

Intersects the risk catalog and same-path transition confidence at total cost deltaRisk + deltaTransition

Removes the supplied invariant premise by targeting the chosen finite invariant PMF

Permits path- and time-selected candidate, depth, both tilts, and posterior substitution on visited rows

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

Integration against the Mathlib PMF induced by a FormalSLT finite PMF equals the corresponding finite weighted sum

Convert a FormalSLT finite nonnegative real PMF into Mathlib's PMF type

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

Finite Bennett MGF with the affine variance factor retained

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