TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

VC-subgraph covering entropy with its finite-r logarithmic bound

Statement

Let $(X, A, Q)$ be a probability space, let $1 \leq r < \infty$ , and let $F$ be a nonempty VC-subgraph class of measurable real functions with finite VC index $V$ . Suppose a measurable envelope $F$ satisfies $∣ f (x) ∣ \leq F (x)$ for every $f \in F$ and $x \in X$ , and

$0 < ∥ F ∥_{Q, r} : = {(\int F^{r} d Q)}^{1 / r} < \infty .$

For every $0 < ϵ < 1$ , put $K_{0} : = 3 e^{2} / (e - 1)$ and $K : = 4 K_{0}$ . Then

$N ⁣ (ϵ ∥ F ∥_{Q, r}, F, L^{r} (Q)) \leq {[K (2 / ϵ)^{r} \log ⁣ (3 e (2 / ϵ)^{r})]}^{V - 1} \leq {(\frac{A}{ϵ})}^{A r V}, A : = 12 e K + 2.$

The exponent in the first bound is the finite-r logarithmic form. No Axiom of Choice or Countable Choice is used in this proof.

Facts & Assumptions

Given: A probability measure $Q$ , a nonempty VC-subgraph class $F$ with index $V$ , an envelope $F$ with $0 < ∥ F ∥_{Q, r} < \infty$ , $1 \leq r < \infty$ , and $0 < ϵ < 1$ .

[F1]

The subgraph of $f$ is $C_{f} = {(x, t) : t < f (x)}$ , and the class has first-unshattered index $V$ (VC-subgraph classes, envelopes, and the first-unshattered index).

[F2]

$L^{r} (Q)$ distance is $∥ f - g ∥_{Q, r}$ ; covering centers belong to the covered class (Covering, packing, bracketing numbers, and metric entropy).

[F3]

A nonempty measurable set class of finite VC index $W$ satisfies $N (δ, C, L^{1} (μ)) \leq {[K_{0} δ^{- 1} \log (3 e / δ)]}^{W - 1}$ for $0 < δ < 1$ and any probability measure $μ$ (Logarithmic L-r covering bound for VC classes of sets).

[F4]

If $h \geq 0$ is measurable, then $h d Q$ is a measure with total mass $\int h d Q$ (The measure with density $f$ relative to $μ$ , The indefinite integral of a nonnegative measurable function is a measure).

[F5]

Finite products of sigma-finite measures have the rectangle formula, and Tonelli permits iterated integration of nonnegative measurable functions (The product sigma-algebra and its finite iterates, For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique, Tonelli's theorem for nonnegative measurable functions on a sigma-finite product).

[F6]

For the finite grid $U_{J}$ with trapezoidal weights from A finite uniform grid approximates interval length, every interval $[a, b) \subseteq [- 1, 1]$ has grid mass within $1 / J$ of $(b - a) / 2$ .

[F7]

Coordinate lifts on a product space are measurable, and arithmetic and order operations on measurable real functions preserve measurability; strict threshold sets of measurable real functions are measurable (The product sigma-algebra and its finite iterates, Arithmetic and lattice operations preserve measurability whenever they are defined, Threshold characterisations of real-valued and extended-real-valued measurability).

[F8]

For $r > 0$ , $t \mapsto t^{r}$ is increasing on $[0, \infty)$ and sends nonnegative measurable functions to measurable functions (Positive real powers preserve measurability).

[F9]

For each $δ > 0$ , there is an integer $J \geq 1$ with $1 / J \leq δ$ (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ ).

[F10]

Positive-base real powers obey the product and exponent laws (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[F11]

The logarithm is increasing, $\log e = 1$ , and $\log (a b) = \log a + \log b$ for positive $a, b$ ; its derivative is $1 / u$ , so the mean value theorem applies to it on positive compact intervals (The natural logarithm as the inverse of the exponential function, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , The mean value theorem, as the case $g (x) = x$ of Cauchy's: for $f$ continuous on $[a, b]$ with $a < b$ and differentiable on $(a, b)$ there is $c \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[F12]

$e = \exp (1) > 1$ , since the exponential is strictly increasing and $\exp (0) = 1$ (The real exponential function and the number $e$ by a power series, The exponential function is strictly increasing).

Proof

Given: The objects and hypotheses of the statement.

1.1F4F7F8givenalgebra

Put $M : = \int F^{r} d Q = ∥ F ∥_{Q, r}^{r}$ . By [F8] $F^{r}$ is measurable; the hypotheses give $0 < M < \infty$ . By [F7], the density $F^{r} / M$ is measurable. Define $R$ by $d R = (F^{r} / M) d Q$ ; its total mass is one by [F4].

2.1F5F6F9givenalgebrastep 1.1

Set $δ : = ϵ^{r} / 2^{r + 1}$ . Then $0 < δ < 1$ , so [F9] supplies an integer $J \geq 1$ with $1 / J \leq δ$ . Use the grid $U_{J}$ and probability $ν_{J}$ of [F6], and form the product probability $\tilde{Q} : = R \otimes ν_{J}$ on $X \times U_{J}$ using [F5].

3.1F1F7givenstep 2.1

Let $X_{+} : = {x : F (x) > 0}$ and define $A_{f} : = {(x, u) : x \in X_{+}, u F (x) < f (x)}$ for $f \in F$ . The coordinate projections are measurable because their preimages of measurable sets are rectangles; hence [F7] makes $X_{+}$ and each $A_{f}$ product-measurable. On $X_{+} \times U_{J}$ , the map $ψ (x, u) : = (x, F (x) u)$ is injective and $A_{f} = ψ^{- 1} (C_{f})$ . If a finite set of pairs is shattered by ${A_{f} : f \in F}$ , its image under $ψ$ is a same-size set shattered by ${C_{f} : f \in F}$ . Thus the nonempty set class $C_{J} : = {A_{f} : f \in F}$ has finite VC index $V_{J} \leq V$ .

4.1F6F8step 1.1step 3.1given

Fix $f, g \in F$ . For $x \in X_{+}$ , put $a (x) : = \min (f (x), g (x)) / F (x)$ and $b (x) : = \max (f (x), g (x)) / F (x)$ . The envelope gives $- 1 \leq a (x) \leq b (x) \leq 1$ , and the section $(A_{f} △ A_{g})_{x}$ is exactly ${u \in U_{J} : a (x) \leq u < b (x)}$ . By [F6], its $ν_{J}$ -mass differs from $∣ f (x) - g (x) ∣ / (2 F (x))$ by at most $1 / J$ . The set $X ∖ X_{+}$ has $R$ -measure zero, since the density $F^{r} / M$ vanishes there.

4.2F3F12givenchoosestep 2.1step 3.1

Apply [F3] to $C_{J}$ under $\tilde{Q}$ at radius $δ$ . Since $e > 1$ , $K_{0} = 3 e^{2} / (e - 1) > 1$ , and $δ < 1$ makes $\log (3 e / δ) > 1$ ; thus the bracketed base is greater than one, so $V_{J} \leq V$ yields $N (δ, C_{J}, L^{1} (\tilde{Q})) \leq {[K_{0} δ^{- 1} \log (3 e / δ)]}^{V - 1} < \infty$ . Choose a cover with this many centers $A_{g_{1}}, \dots, A_{g_{k}}$ , each represented by some $g_{j} \in F$ . The cover uses finitely many centers, so this uses only finite choice.

5.1F2F5F8F10step 1.1step 4.1algebra

Integrating the section estimate under $R$ and using [F5] gives $∣ \tilde{Q} (A_{f} △ A_{g}) - \frac{1}{2} \int_{X_{+}} \frac{∣ f - g ∣}{F} d R ∣ \leq \frac{1}{J}$ . For $x \in X_{+}$ , put $a : = ∣ f (x) - g (x) ∣ \leq 2 F (x)$ . If $a = 0$ the inequality $a^{r} \leq 2^{r - 1} F (x)^{r - 1} a$ is immediate; if $a > 0$ and $r > 1$ , [F8] raises $a \leq 2 F (x)$ to the positive power $r - 1$ and multiplication by $a$ gives it; for $r = 1$ it is equality. Hence [F2] gives $∥ f - g ∥_{Q, r}^{r} \leq 2^{r - 1} M \int_{X_{+}} \frac{∣ f - g ∣}{F} d R \leq 2^{r} M (\tilde{Q} (A_{f} △ A_{g}) + \frac{1}{J})$ . The last inequality uses the discrepancy bound and the definition of $R$ .

6.1step 2.1step 5.1step 4.2algebra

For every $f \in F$ , some center satisfies $\tilde{Q} (A_{f} △ A_{g_{j}}) \leq δ$ . Steps 5.1 and 2.1 then give $∥ f - g_{j} ∥_{Q, r}^{r} \leq 2^{r} M (δ + 1 / J) \leq 2^{r + 1} M δ = ϵ^{r} M$ . Thus the function class is covered by the same $k$ centers at radius $ϵ ∥ F ∥_{Q, r}$ , and its covering number is no larger than the set covering number in step 4.2.

7.1F11F12step 4.2step 6.1algebra

Put $L : = \log (3 e (2 / ϵ)^{r})$ . From $δ^{- 1} = 2 (2 / ϵ)^{r}$ and $\log (3 e / δ) = L + \log 2 \leq 2 L$ (since $3 e (2 / ϵ)^{r} > 2$ , so $L > \log 2$ ), the base in step 4.2 is at most $4 K_{0} (2 / ϵ)^{r} L = K (2 / ϵ)^{r} L$ . Since this base exceeds one, step 6.1 proves the first asserted entropy bound.

8.1F11F12step 7.1algebra

Put $η : = (ϵ / 2)^{r} \in (0, 1)$ . For $u \geq 1$ , the function $h (u) : = u - \log u$ has $h (1) = 1$ and $h^{'} (u) = 1 - 1 / u \geq 0$ ; the mean value theorem [F11] gives $\log u \leq u$ . Hence $K η^{- 1} \log (3 e / η) \leq 3 e K η^{- 2} = 3 e K (2 / ϵ)^{2 r}$ . Let $A : = 12 e K + 2$ . From [F12], $e - 1 < e$ , so $K_{0} = 3 e^{2} / (e - 1) > 3 e > 3$ and $K = 4 K_{0} > 4$ . Thus $x : = 3 e K > 1$ and $A / 2 = 6 e K + 1 \geq x$ , whence $(A / 2)^{2 r} \geq x^{2 r} \geq x$ because $r \geq 1$ . This gives $3 e K (2 / ϵ)^{2 r} \leq (A / ϵ)^{2 r}$ .

9.1step 7.1step 8.1algebra∎

The first bound is the step 7.1 base raised to $V - 1$ . Since $A / ϵ > 1$ , $A \geq 2$ , and $V \geq 1$ , we have $2 r (V - 1) \leq A r V$ . Thus the first bound is at most $(A / ϵ)^{A r V}$ , proving the second inequality.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

98 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Jon A. Wellner, Empirical Processes: Theory and Applications, Chapter 1, Theorem 8.2 (standard reference, not scraped)
David Pollard, Probability Tools, Tricks, and Miracles, 2026 manuscript, Section 14.5 (standard reference, not scraped)