Finite sub-Gaussian chaining foundations #
This module starts the finite-process side of the chaining ladder. It is finite-index throughout: finite outcome space, finite index class, finite nets, and finite sums for expectation.
Main declarations:
FiniteNet: a finite ε-net with an explicit nearest-net projection.FiniteSubGaussianProcess: a finite weighted process with an abstract sub-Gaussian MGF increment condition.FiniteSubGaussianProcess.projection_increment_mgf: the MGF bound along a chain of finite projections.chain_telescope: the multiscale telescoping identity.finite_chaining_decomposition: pointwise finite chaining by suprema.finite_expectedSup_le_of_shifted_mgf: finite-max entropy budget from shifted coordinate MGF bounds.finite_chaining_expectation_bound: finite weighted-expectation chaining once each scale increment has an expected-sup budget.FiniteSubGaussianProcess.finite_dudley_entropy_sum_projection_pairs: finite Dudley-style entropy sum over realized projection-pair families.FiniteSubGaussianProcess.finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget: finite dyadic entropy-integral budget wrapper for covering-number nets.FiniteSubGaussianProcess.finite_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope: finite covering-count wrapper with a monotone prefix-sup entropy envelope.FiniteSubGaussianProcess.finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_entropy_integral_comparison: projected finite-net wrapper comparing the finite dyadic budget with a supplied entropy-at-radius upper-sum/integral budget.FiniteSubGaussianProcess.finiteDyadicEntropyAtRadiusUpperSum_le_two_mul_shifted_intervalIntegral_sum: analytic dyadic upper-sum domination by a finite shifted-annulus interval integral budget under antitonicity and interval-integrability assumptions.
This is not a continuous Dudley integral or a generic metric entropy theorem. It records the finite decomposition and expectation bookkeeping needed for later entropy estimates.
Weighted expectation over a finite outcome space. The caller supplies the weights and their probabilistic assumptions separately.
Equations
- FormalSLT.Covering.FiniteSubGaussianChaining.finiteExpectation p X = ∑ ω : Ω, p ω * X ω
Instances For
Supremum over a finite nonempty index type.
Equations
Instances For
A finite ε-net with an explicit nearest-net projection. A is the finite
type of net points, center realizes a net point in T, and project chooses
a nearest-net index for each target point.
Instances For
The nearest-net projection as a map back into the ambient index type.
Equations
- N.projection t = N.center (N.project t)
Instances For
The projection selected by a finite net is within the net radius.
The cardinality of the finite net, i.e. the discrete covering number represented by this chosen net.
Equations
- _N.coveringNumber = Fintype.card A
Instances For
The finite set of net indices actually hit by the projection map. This is
a finite replacement for taking a supremum over an ambient index type T.
It is useful when T is not finite but a projected supremum only ranges over
the image of a finite net.
Instances For
Equations
A chosen ambient source point whose projection realizes a projected net index. The choice is finite-image bookkeeping only; later theorems use it to build chains without assuming the ambient type is finite.
Equations
Instances For
The chosen source projects to the projected net index.
Projecting the chosen source point gives the center indexed by the projected net index.
Two finite net projections of the same point are within the sum of their radii, assuming the shared distance is symmetric and satisfies the triangle inequality. This is the finite-net geometry step used to turn net radii into projection-chain increment radii.
The finite family of projection pairs realized by projecting the same ambient point into two finite nets. This lets finite chaining pay entropy for the realized increment family rather than for the full ambient index type.
Instances For
Equations
The projection pair selected by a point.
Instances For
The realized projection-pair family is bounded by the product of the two finite covering numbers.
Log-cardinality of realized projection pairs is bounded by the log of the product of the two finite covering numbers.
Every realized projection pair inherits the sum-of-radii distance bound from the shared point whose projections produced it.
A finite weighted process with sub-Gaussian increment MGF control.
The process is indexed by a finite type T and observed on a finite outcome
space Ω. The MGF field is intentionally abstract: later modules can derive it
from concrete Gaussian/Rademacher constructions, while this module only needs a
clean finite-process interface.
Instances For
The sub-Gaussian increment MGF bound packaged as a theorem.
Radius-bounded form of the sub-Gaussian increment MGF bound for a single increment. This is the reusable finite-process primitive behind the finite max/entropy estimates below.
The sub-Gaussian increment MGF bound along one level of a projection chain.
Radius-bounded version of projection_increment_mgf. If a projection
level moves every index point by at most r, the same MGF increment is bounded
using r in place of the pointwise distance.
Finite expectation algebra #
Additivity of finite weighted expectation.
Finite expectation adapter from a supplied supremum functional to a projected finite-supremum surrogate, under an explicit terminal approximation error.
This is only finite expectation bookkeeping. It deliberately does not define
or prove measurability for a supremum over an arbitrary class: callers must
supply the scalar supFunctional and the pointwise approximation hypothesis.
Finite-skeleton terminal approximation adapter. If every point in a finite
separable skeleton is pointwise controlled by its terminal finite-net
projection up to terminalError, then the skeleton supremum is controlled by
the projected finite-net supremum up to the same error.
This is still a finite statement: K is a finite skeleton supplied by the
caller, and N is a finite terminal net. It does not construct a supremum over
an arbitrary infinite class.
Pointwise projected-sup adapter for a supplied supremum functional.
The caller supplies a scalar supFunctional, a finite skeleton K, and two
explicit approximation hypotheses:
- a separability/dense-net budget from
supFunctionalto the finite skeleton; - a terminal projection budget from the finite skeleton to the terminal net.
The conclusion is exactly the hterminal hypothesis required by the
finite-expectation boundary theorem. No arbitrary measurable supremum is
defined here.
Finite expectation form of the separable/dense-net boundary adapter.
This is a reusable projected-sup-to-true-sup bridge: the true supremum is represented by a caller-supplied scalar functional, and all continuous content is isolated in the explicit finite-skeleton and terminal-approximation hypotheses.
Terminal-projection approximation from a pathwise modulus at the terminal net radius.
This is the direct helper for the hterminalApprox assumption in the
finite-skeleton Dudley adapter: if each sample path is one-sided continuous at
the terminal-net radius, then every skeleton point is controlled by its
terminal projection plus terminalError.
Terminal-projection approximation from a pathwise modulus at a larger radius budget. This is useful when the modulus is stated with a named radius bound rather than the exact net radius.
Finite dense-skeleton approximation for a finite ambient supremum.
If every ambient point is controlled by a selected skeleton point up to
skeletonError, then the finite supremum over the ambient type is controlled
by the finite skeleton supremum plus the same error. This is a finite,
measurability-free version of the dense-net step.
Finite-skeleton approximation for a caller-supplied supremum functional.
The caller supplies an approximate maximizer witness : Ω → T for the scalar
supFunctional, and a finite skeleton selector nearest : T → K. If the
witness is within witnessError of the supplied supremum and every ambient
point is within skeletonError of its skeleton representative, then
hseparable follows with error witnessError + skeletonError.
This avoids defining an arbitrary measurable supremum: all continuous content is exposed as explicit witness and finite-skeleton hypotheses.
Pull a finite sum through finite weighted expectation.
Pull a finite sum over an arbitrary finite index type through finite weighted expectation.
Shift an exponential inside finite weighted expectation.
A shifted exponential-moment bound controls the finite weighted mean. This is the elementary Chernoff step used below to convert finite-max MGF control into an expected-supremum budget.
Multiscale chaining decomposition #
Finite-max entropy budget from shifted coordinate MGF bounds. If each
coordinate has shifted exponential moment at most 1 / |T|, then the expected
finite supremum is at most budget.
Finite-max entropy bound from coordinate MGF control. If every coordinate
has moment generating function at most exp q at a fixed positive λ, then
the expected finite supremum is bounded by (log |T| + q) / λ.
This is the standalone finite-index bridge from an MGF condition to an expected-supremum budget; later chaining theorems apply it to projection increments.
Optimizing L / λ + λq / 2 at λ = sqrt (2L/q), written in the
algebraic form used by the finite sub-Gaussian max bound.
Pull the finite entropy term out of the square root in the form used by
the Dudley-style finite entropy-sum corollaries. The radius parameter is a
finite net radius or a sum of adjacent finite net radii, not a limiting
scale.
Optimized finite sub-Gaussian max bound from coordinate MGF control. If
each coordinate satisfies E exp(λ Y_t) ≤ exp(λ²σ²/2) for every λ, then the
expected supremum over the finite index type is at most
sqrt (2σ² log |T|).
This is finite-index and finite-support only; it is the entropy-budget lemma that feeds the later multiscale chaining statements.
Optimized finite sub-Gaussian max bound, including singleton index families.
The existing square-root optimizer needs 1 < Fintype.card T so that
log |T| > 0. This wrapper keeps that branch unchanged and adds the singleton
case. When |T| = 1, the log-cardinality bound is available for every positive
λ; sending λ to zero through arbitrary positive slack gives the zero
entropy bound. This is the finite max brick needed before dyadic chaining can
allow singleton projection-pair layers.
Telescoping identity for a chain of projections. The projection sequence is
indexed by natural-number levels; level 0 is the coarse approximation and
level m is the terminal approximation.
Telescoping identity for a projection chain parameterized by an arbitrary
finite domain. The process is still indexed by T; the chain is evaluated
along a finite parameter type such as a projected net image.
Pointwise finite multiscale chaining: the supremum of a process is bounded by the supremum at the coarse projection plus the sum of suprema of scale increments.
Finite weighted-expectation chaining bound. If every scale increment has
expected finite supremum at most budget j, then the expected supremum of the
full finite process is bounded by the expected coarse supremum plus the sum of
the scale budgets.
This is the finite-process scaffold that later sub-Gaussian increment estimates feed into; it is not the continuous Dudley entropy integral.
Pointwise finite projected chaining. This is the same finite telescoping
bookkeeping as finite_chaining_decomposition, but it stops at the terminal
projection π m instead of requiring π m t = t.
This is the finite projected-supremum scaffold used before passing to a continuous or measurable supremum.
Finite weighted-expectation projected chaining bound. It bounds the
expected supremum over the terminal projection π m, without assuming that
the terminal projection is the identity.
This is intentionally finite-index and finite-scale. It does not construct a measurable supremum over an arbitrary class.
Pointwise projected chaining over an arbitrary finite parameter domain.
The process itself may be indexed by an ambient type T; only the parameter
domain U over which the projected supremum is taken must be finite.
This is the finite-image bridge used to avoid assuming [Fintype T] for
projected finite-net suprema.
Finite weighted-expectation projected chaining over an arbitrary finite
parameter domain U. The ambient process index type T need not be finite.
Chaining bound specialized to a finite sub-Gaussian process record. The
sub-Gaussian MGF field is carried by P; the present theorem consumes the
finite expected-sup budgets for each scale, which later entropy lemmas will
derive from that MGF condition.
Projected chaining bound specialized to a finite sub-Gaussian process.
The left side is the expected finite supremum over the terminal projection
π m, so no identity-terminal assumption is required.
Projected chaining bound for a finite parameter domain U, specialized to
a finite sub-Gaussian process over an ambient index type T. This is the
version used for projected finite-net images when T itself is not finite.
Expected supremum budget for one projection-increment level of a finite
sub-Gaussian process. The hypothesis
exp(λ²σ²r²/2 - λ·budget) ≤ 1 / |T| is the finite entropy accounting step:
the radius-bounded sub-Gaussian MGF leaves enough room for a union bound over
the finite index type.
Log-cardinality version of
projection_increment_expectedSup_le_of_radius. This is the finite
sub-Gaussian max bound for one projection-increment level:
E sup_t Δ_j(t) ≤ (log |T| + λ²σ²r²/2) / λ.
Square-root version of the one-level finite sub-Gaussian max bound,
obtained by optimizing the positive λ parameter in
projection_increment_expectedSup_le_of_radius_log.
Square-root projection-increment bound, including singleton index families.
This is the projection-increment form of
finite_expectedSup_le_of_subGaussian_mgf_sqrt_nonempty. It removes the
1 < card side condition from the one-level bound; singleton projection
families pay zero entropy.
Log-cardinality finite-max bound for an arbitrary finite family of
sub-Gaussian increments. The index family I is finite but otherwise
abstract; this is still a finite-sample, finite-class statement, not a
measurable separability or Talagrand contraction theorem.
Optimized square-root finite-max bound for an arbitrary finite family of
sub-Gaussian increments:
E sup_i (X_{right i} - X_{left i}) ≤ sqrt(2 σ² r² log |I|).
The theorem is deliberately finite-index and finite-family.
Square-root finite-max bound for an arbitrary finite family of sub-Gaussian increments, including singleton families.
This removes the 1 < card side condition from
increment_family_expectedSup_le_of_radius_sqrt; singleton increment families
pay zero entropy through finite_expectedSup_le_of_subGaussian_mgf_sqrt_nonempty.
Finite chaining bound with radius/MGF-derived scale budgets. Each scale
budget is justified by a radius bound and the finite entropy condition
exp(λ²σ²r_j²/2 - λ·budget_j) ≤ 1 / |T|; the existing chaining theorem then
sums those budgets.
Log-cardinality finite chaining bound. Radius-bounded sub-Gaussian
projection increments yield the explicit finite entropy budget
(log |T| + λ²σ²r_j²/2) / λ at each scale, and the finite chaining theorem
sums those budgets.
Square-root finite chaining bound. This is the optimized finite-index sub-Gaussian chaining form for radius-bounded projection increments.
Finite chaining with an explicit finite increment family at each scale.
For each level j, the maps left j, right j describe a finite family of
candidate increments indexed by I j, and select j says every projection
increment in the chain is represented in that finite family. The result
combines finite chaining with the finite-max sub-Gaussian entropy budget
sqrt(2 σ² r_j² log |I_j|).
This is a finite-sample, finite-index chaining theorem; it is a tutorial-grade stepping stone toward Dudley-style arguments, not a continuous entropy integral.
Finite chaining with explicit finite increment families, including singleton increment families at any scale. Singleton families pay zero entropy.
Projected finite chaining over a finite parameter domain U, with an
explicit finite increment family at each scale. The process is indexed by an
ambient type T, which need not be finite.
Projected finite chaining over a finite parameter domain, including singleton increment families at any scale.
Projected finite chaining with an explicit finite increment family at each scale. This version bounds the terminal projected supremum and therefore does not require the final projection to be the identity.
Projected finite chaining with explicit increment families, including singleton increment families at any scale.
One-step square-root entropy bound for increments between two finite-net
projections, paying log of the realized projection-pair family. This is the
finite-net entropy version of the one-level sub-Gaussian max bound.
One-step square-root entropy bound for increments between two finite-net projections, including singleton projection-pair families.
The old net_increment_expectedSup_le_pair_sqrt theorem required
1 < card ProjectionPair. This variant uses the singleton-safe finite-max
bound, so collapsed projected-pair layers pay zero entropy instead of forcing a
separation witness.
One-step finite-net entropy bound using the product of the two finite covering numbers. This is a readable corollary of the sharper projection-pair bound.
One-step finite-net entropy bound using the product of the two finite covering numbers, including singleton projection-pair families.
Finite multiscale chaining for a sequence of finite nets, with each scale paying entropy for the realized projection-pair family between consecutive nets. This is a finite, scalar, finite-sample chaining statement and remains short of the continuous Dudley entropy integral.
Finite multiscale chaining for a sequence of finite nets, including singleton realized projection-pair families at any scale.
Finite multiscale chaining for a sequence of finite nets, stated with the
product of consecutive covering numbers at each scale. This follows from the
projection-pair version plus the finite cardinality bound
|pairs_j| ≤ N_j * N_{j+1}.
Finite multiscale chaining for a sequence of finite nets, stated with products of consecutive covering numbers and allowing singleton projection-pair families.
Projected finite multiscale chaining for a sequence of finite nets, stated
with products of consecutive covering numbers. The left side is the expected
supremum after the terminal projection (N m).projection, not the full
finite supremum of the original process.
Projected finite multiscale chaining with products of consecutive covering numbers, including singleton projection-pair families.
Projected finite multiscale chaining over the terminal finite-net image.
The ambient process index type T is not assumed finite; the finite supremum
ranges over the indices actually hit by the terminal net projection.
This is a projected-net boundary lift toward total-bounded Dudley: finite terminal image, finite scale range, scalar process, no measurable supremum over arbitrary classes.
Projected finite multiscale chaining over the terminal finite-net image, including singleton projection-pair families at any scale.
Finite Dudley-style entropy sum over realized projection-pair families. For a finite sub-Gaussian process and a finite sequence of finite nets, the expected finite supremum is bounded by a coarse-net term plus a finite entropy sum. Each scale pays the adjacent-radius coefficient times the square root of the log-cardinality of the realized projection pairs between consecutive nets.
This is a finite, scalar-valued, finite-index theorem. It is not the continuous Dudley entropy integral; infinite classes, separability, and measurable suprema over arbitrary function classes remain outside this statement.
Finite Dudley-style entropy sum stated with products of consecutive finite
covering numbers. This is the public-facing finite entropy-sum corollary of the
projection-pair theorem: each scale pays the adjacent-radius coefficient times
sqrt (log (N_j * N_{j+1})).
The statement is intentionally finite: finite support, finite index set, finite nets, finite number of scales, and scalar real-valued processes only. It is not the continuous Dudley integral.
Finite Dudley-style entropy sum over realized projection-pair families
with an explicit geometric radius schedule. If each adjacent pair of finite
nets moves by at most radiusScale / 2^j, the entropy sum can be stated using
that dyadic radius budget directly.
This is still a finite theorem: finite support, finite index set, finitely many nets, scalar real-valued process, and a finite sum. It is a bridge from the projection-pair finite entropy sum toward a later Dudley-style integral, not a continuous entropy integral.
Finite Dudley-style entropy sum with products of consecutive finite
covering numbers and an explicit geometric radius schedule. If each adjacent
pair of finite nets moves by at most radiusScale / 2^j, each scale pays that
dyadic radius budget times the square root of the log product of adjacent
finite covering numbers.
The statement is intentionally finite; continuous Dudley, infinite classes, separability, and measurability of arbitrary suprema remain outside this statement.
Finite Dudley-style projection-pair entropy bound with a geometric radius
schedule and an explicit per-scale entropy envelope. This packages the finite
dyadic sum in a form suited for later comparison with entropy integrals:
provide entropyBudget j above the square-root log-cardinality at each finite
scale, and the theorem pays the finite weighted sum of those budgets.
This is not a continuous Dudley integral. The process, nets, index family, and number of scales are all finite.
Finite Dudley-style covering-number entropy bound with a geometric radius
schedule and an explicit per-scale entropy envelope. At each finite scale,
entropyBudget j upper-bounds sqrt (log (N_j * N_{j+1})); the conclusion is
a finite dyadic entropy-budget sum.
This remains finite and scalar-valued. It is a preparation lemma for a later Dudley-style integral comparison, not an infinite-class or continuous-entropy theorem.
Finite dyadic geometric-series budget used by the public discrete Dudley
corollaries. It records the elementary fact ∑_{j < m} 2^{-j} ≤ 2 in the
same real-valued denominator form as the radius schedules below.
Dyadic annulus identity for the geometric radius schedule. The radius at
scale j is twice the width of the dyadic annulus between scales j and
j + 1. This is the elementary bridge used to rewrite finite Dudley-style
dyadic sums in integral-comparison language.
Nonnegativity of dyadic annulus widths under a nonnegative top radius.
The dyadic annulus at scale j has twice the width of the next lower
annulus. This is the elementary constant-loss in the shifted integral
comparison for antitone entropy profiles.
If a function is bounded below by a constant on an interval, then its interval integral dominates the rectangle with that height. This is a small analysis adapter used to keep the Dudley integral-comparison hypotheses explicit.
For an antitone entropy profile, the value at the upper endpoint of a shifted dyadic annulus is a lower bound throughout that annulus, so the corresponding rectangle is bounded by the interval integral over the annulus.
This is finite-scale analysis only; it does not assert a continuous Dudley integral or any measurable-supremum theorem.
Finite dyadic entropy-integral budget. This is an upper Riemann-style sum
over dyadic annuli, not a continuous Dudley entropy integral. The term at
scale j is the annulus width
radiusScale / 2^j - radiusScale / 2^(j+1) times a supplied finite entropy
envelope.
Equations
- One or more equations did not get rendered due to their size.
Instances For
One-step dyadic entropy budget for a constant entropy envelope.
Finite dyadic entropy-at-radius upper sum. The value
entropyAtRadius (radiusScale / 2^(j+1)) is sampled at the lower endpoint of
the dyadic annulus (radiusScale / 2^(j+1), radiusScale / 2^j].
This is a finite Riemann-style upper sum used as an interface to later entropy-integral estimates. It is not a definition of a continuous integral.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Analytic domination of the finite dyadic entropy-at-radius upper sum by a finite shifted-annulus interval-integral budget.
For antitone entropy profiles, the lower-endpoint upper sum on annulus j is
controlled by twice the interval integral over annulus j + 1. The theorem is
therefore a finite dyadic Riemann-step bridge toward Dudley-style integral
language. It is not a continuous Dudley integral theorem, does not involve
separability, and does not claim measurable suprema over arbitrary classes.
Scalar-budget wrapper for the shifted-annulus interval-integral comparison. The caller supplies the finite integral budget, which later can be discharged from a true continuous entropy-integral estimate.
This theorem remains finite-scale and finite-sum; it is the analytic domination layer needed before a continuous Dudley wrapper can be stated.
The shifted dyadic annuli used by
finiteDyadicEntropyAtRadiusUpperSum_le_two_mul_shifted_intervalIntegral_sum
compose into one truncated interval. This is a finite adjacent-interval
identity only: it does not assert any continuous Dudley theorem, separability
statement, or measurable supremum over an arbitrary class.
The finite shifted-annulus interval-integral budget is exactly the interval
integral over the truncated dyadic range [radiusScale / 2^(m+1), radiusScale/2].
This is the analytic bookkeeping bridge from a finite dyadic annulus budget to a single truncated interval integral. It remains finite-scale and makes no continuous Dudley, separability, or arbitrary measurable-supremum claim.
Finite dyadic entropy-at-radius upper sum dominated by one truncated interval integral. This composes the shifted-annulus comparison with adjacent-interval additivity.
The statement is deliberately finite: a finite dyadic scale range, scalar entropy profile, explicit antitonicity and interval-integrability hypotheses, and no continuous Dudley, separability, or arbitrary measurable-supremum claim.
Finite prefix-sup entropy envelope. At scale j, this records the maximum
of the first j + 1 scale budgets. It is a finite, discrete monotone envelope;
it is not a continuous metric-entropy function.
Equations
- FormalSLT.Covering.FiniteSubGaussianChaining.FiniteSubGaussianProcess.finitePrefixSupEnvelope entropyAtScale j = (Finset.range (j + 1)).sup' ⋯ entropyAtScale
Instances For
The finite prefix-sup envelope of a constant scale budget is constant.
Each scale budget is bounded by its finite prefix-sup envelope.
A monotone finite scale budget is already equal to its prefix-sup envelope.
The finite prefix-sup envelope is monotone in the scale index.
Compare the finite dyadic entropy budget with an entropy-at-radius upper sum. The hypothesis only samples the external entropy envelope at the lower dyadic endpoint for each finite annulus.
This is a finite upper-sum comparison, not a continuous Dudley integral theorem and not an infinite-class statement.
Compare the finite dyadic entropy budget with a supplied scalar upper
budget. A later analytic layer can discharge hupperSum from an actual
entropy-integral estimate; this theorem itself remains finite and discrete.
Finite discrete Dudley-style projection-pair bound with a uniform entropy
cap across dyadic scales. If every scale's projection-pair entropy term is at
most entropyCap, the finite dyadic entropy-budget sum is bounded by the
geometric-series budget 2 * sqrt(2σ²) * radiusScale * entropyCap.
This is still finite-index, finite-net, and scalar-valued. It is a discrete finite entropy bound, not a continuous entropy integral.
Finite discrete Dudley-style covering-number bound with a uniform entropy
cap across dyadic scales. If
sqrt (log (N_j * N_{j+1})) ≤ entropyCap at every finite scale, the dyadic
covering-number entropy sum is bounded by
2 * sqrt(2σ²) * radiusScale * entropyCap.
This is the finite discrete refinement of the entropy-budget wrapper. It does not introduce a continuous entropy integral or infinite-class assumptions.
Finite discrete Dudley-style projection-pair bound rewritten through
dyadic annulus budgets. The hypothesis hannulus says each scale's
annulus width * entropyBudget is bounded by an explicit finite budget; the
conclusion pays 2 * sqrt(2σ²) times the finite sum of those budgets.
This is an integral-comparison bridge for the finite chaining scaffold. It is not a continuous entropy integral and does not introduce infinite classes, separability assumptions, or arbitrary measurable suprema.
Finite discrete Dudley-style covering-number bound rewritten through
dyadic annulus budgets. This is the covering-number version of
finite_dudley_entropy_sum_projection_pairs_geometric_annulus_budget.
The theorem remains finite: finite outcome support, finite index class, finite nets, scalar-valued process, and a finite dyadic scale range.
Finite discrete Dudley-style projection-pair bound controlled by a finite
dyadic entropy-integral budget. The supplied entropyEnvelope dominates each
finite projection-pair entropy term, and the conclusion pays the finite
upper Riemann-style annulus sum
finiteDyadicEntropyIntegralBudget radiusScale m entropyEnvelope.
This is still finite-index, finite-net, scalar-valued chaining. It is a bridge toward Dudley-style integral language, not the continuous Dudley integral and not an infinite-class theorem.
Finite discrete Dudley-style covering-number bound controlled by a finite
dyadic entropy-integral budget. This is the covering-number version of
finite_dudley_entropy_sum_projection_pairs_geometric_integral_budget.
The theorem remains finite: finite outcome support, finite index class, finite nets, scalar-valued process, and a finite dyadic scale range.
Finite discrete Dudley-style covering-number bound where the entropy
envelope is constructed from finite covering-number upper bounds. The
coverCount j values are external finite upper bounds on the product
N_j * N_{j+1} at each dyadic scale; the theorem uses their finite prefix sup
as a monotone entropy envelope inside finiteDyadicEntropyIntegralBudget.
This is still finite-index, finite-net, scalar-valued chaining over finitely many scales. It packages the finite entropy envelope needed for the Dudley-style upper-sum wrapper; it is not a continuous Dudley integral and not an infinite-class result.
Projected finite Dudley-style covering-number bound with a dyadic
entropy-integral budget. The conclusion controls the finite supremum after the
terminal projection (N m).projection; unlike the full finite Dudley theorem,
it does not require (N m).projection t = t.
This remains a finite-index, finite-net, finite-scale theorem. It is a bridge toward total-bounded Dudley statements, not a continuous Dudley integral and not a measurable supremum over an arbitrary class.
Projected finite-net Dudley-style covering-number bound with a dyadic
entropy-integral budget. The ambient index type T need not be finite: the
left side ranges over the finite image of the terminal net projection.
This is a finite-image, finite-scale bridge toward total-bounded Dudley statements. It does not assert a continuous Dudley integral, separability, or a measurable supremum over an arbitrary class.
Projected finite-net Dudley-style covering-number bound with a dyadic entropy-integral budget, without a nontrivial projection-pair cardinality hypothesis.
This variant uses the singleton-safe projected-net chaining bound. Collapsed projection-pair layers pay zero entropy in the finite chaining step, and positivity of the covering-number product follows from the nonempty ambient type and the finite-net projection maps.
A reusable finite dyadic net sequence for projected finite-net Dudley bounds.
The bundle records only finite-scale data: a sequence of finite nets, adjacent cover-count bounds, a dyadic radius scale, and the metric hypotheses needed by the chaining theorem. It does not assert total boundedness, separability, or a continuous entropy integral.
- radiusScale : ℝ
- coverCount_le (j : ℕ) : (self.N j).coveringNumber * (self.N (j + 1)).coveringNumber ≤ self.coverCount j
Instances For
Projected finite-net Dudley bound from a bundled dyadic net sequence.
The conclusion is the same finite projected-net supremum controlled by
finite_projectedNet_dudley_entropy_sum_coveringNumbers_geometric_integral_budget_prefix_envelope,
but callers instantiate one reusable sequence object instead of restating the
geometry and cover-count hypotheses at every use site.
Supplied-supremum finite-budget Dudley bound from a bundled dyadic net sequence.
The caller supplies the terminal finite-net approximation of supFunctional.
This is the finite-budget analogue of the later integral-boundary adapters and
keeps the same limitation: no arbitrary measurable supremum is constructed.
A reusable finite-dyadic Dudley instance for a fixed finite sub-Gaussian process.
This packages the data that examples otherwise repeat at every use site:
the dyadic net sequence, a coarse expected-supremum budget, positivity of the
variance proxy, and the proof that the terminal projected image at scale m
has the stated coarse budget. Supplied suprema are optional and are packaged by
FiniteDyadicDudleyInstance.SupremumAdapter.
- netSequence : P.FiniteDyadicNetSequence A
- coarseBudget : ℝ
- coarse_bound (m : ℕ) : (finiteExpectation P.weight fun (ω : Ω) => finiteSup fun (u : (self.netSequence.N m).ProjectedIndex) => P.X ω ((self.netSequence.N 0).projection (FiniteNet.ProjectedIndex.source (self.netSequence.N m) u))) ≤ self.coarseBudget
Instances For
Optional terminal adapter from a supplied supremum functional to the
terminal projected finite-net supremum of a FiniteDyadicDudleyInstance.
- supFunctional : Ω → ℝ
- terminalError : ℝ
- terminal_bound (m : ℕ) (ω : Ω) : self.supFunctional ω ≤ (finiteSup fun (u : (I.netSequence.N m).ProjectedIndex) => P.X ω ((I.netSequence.N m).center ↑u)) + self.terminalError
Instances For
Projected finite-net Dudley bound from a packaged
FiniteDyadicDudleyInstance.
Supplied-supremum finite Dudley bound from a packaged
FiniteDyadicDudleyInstance and its optional terminal adapter.
Projected finite-net Dudley-style covering-number bound compared against a
finite entropy-at-radius upper-sum/integral budget. The hypothesis
hentropyAtRadius says the finite prefix-sup covering envelope at scale j is
controlled by an external entropy function sampled at the lower dyadic
endpoint. The hypothesis hupperSum is where a later analytic layer can bound
that finite upper sum by a scalar integral budget.
This is still a finite-image, finite-scale theorem. It does not prove a continuous Dudley integral, separability, infinite classes, or measurable suprema over arbitrary index families.
Projected finite-net Dudley-style covering-number bound with the supplied finite entropy-at-radius upper sum discharged by a shifted-annulus interval integral budget.
The analytic hypotheses are explicit: entropyAtRadius is antitone, it is
interval-integrable on each shifted dyadic annulus used by the comparison, and
the finite sum of those annulus integrals is bounded by integralBudget.
The extra factor 2 comes from comparing each dyadic upper-sum rectangle to
the next lower dyadic annulus.
This is still finite-image and finite-scale. It is an analytic bridge toward Dudley-style integral language, not a continuous Dudley theorem, not a separability theorem, and not a measurable arbitrary-supremum theorem.
Projected finite-net Dudley-style covering-number bound with the finite entropy-at-radius upper sum discharged by one truncated interval integral.
This composes the shifted-annulus comparison with adjacent-interval additivity:
the finite shifted-annulus integral budget is the integral over
[radiusScale / 2^(m+1), radiusScale / 2]. The statement is still finite-image
and finite-scale. It is a bridge toward continuous Dudley language, not a
continuous Dudley theorem, not a separability theorem, and not a measurable
arbitrary-supremum theorem.
Projected finite-net Dudley-style covering-number bound compared against a supplied finite entropy-at-radius budget, including singleton projection-pair families.
Projected finite-net Dudley-style covering-number bound with a shifted annulus integral budget, including singleton projection-pair families.
Projected finite-net Dudley-style covering-number bound with a single truncated interval integral, including singleton projection-pair families.
Boundary adapter from projected finite-net Dudley to a supplied supremum functional.
The caller supplies supFunctional : Ω → ℝ together with the explicit terminal
approximation hypothesis that it is pointwise bounded by the terminal projected
finite-net supremum plus terminalError. This keeps the theorem at the finite
continuous-boundary interface: no arbitrary measurable supremum, no
separability theorem, and no infinite-class supremum is constructed here.
Boundary adapter from projected finite-net Dudley to a supplied supremum functional through an explicit finite skeleton.
This is the next continuous-boundary layer after
finite_supFunctional_dudley_entropy_sum_coveringNumbers_geometric_entropy_truncatedIntervalIntegral_comparison.
Instead of asking callers to provide the final terminal approximation in one
bundled hypothesis, it separates the assumptions:
hseparablebounds the supplied supremum functional by a finite skeleton, with errorseparabilityError;hterminalApproxbounds each skeleton point by its terminal net projection, with errorterminalError.
The theorem remains finite-scale and scalar-valued. It does not construct an arbitrary measurable supremum, prove separability, or claim a full continuous Dudley theorem.
Boundary adapter from projected finite-net Dudley to a supplied supremum functional, including singleton projection-pair families.
Boundary adapter from projected finite-net Dudley to a supplied supremum functional through a finite skeleton, including singleton projection-pair families.
One-step square-root entropy bound for increments between two finite-net projections. This packages the finite-net geometry lemma with the optimized sub-Gaussian max bound.