LemmaStatement: AI-adaptedProof: 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.

A finite uniform grid approximates interval length

Statement

Let $J \geq 1$ be an integer, put $u_{j} = - 1 + 2 j / J$ for $j = 0, \dots, J$ , and give the finite set $U_{J} = {u_{0}, \dots, u_{J}}$ the probability weights

$ν_{J} ({u_{0}}) = ν_{J} ({u_{J}}) = \frac{1}{2 J}, ν_{J} ({u_{j}}) = \frac{1}{J} (1 \leq j < J) .$

For all $- 1 \leq a \leq b \leq 1$ ,

$∣ ν_{J} ([a, b)) - \frac{b - a}{2} ∣ \leq \frac{1}{J} .$

Facts & Assumptions

Given: An integer $J \geq 1$ , the grid $U_{J}$ , and its specified weights.

[F1]

A measure on a finite power-set space is a nonnegative set function that vanishes on the empty set and is countably additive (Measures on sigma-algebras). It is a probability measure when its total mass is one (Probability measures and probability spaces).

[F2]

Finite sums are additive and obey the usual recursive sum law (Finite sums and finite products, by recursion, Laws of finite sums and finite products).

Proof

Given: An integer $J \geq 1$ , the grid $U_{J}$ , and its specified weights.

1.1F1F2givenalgebra

The weights are nonnegative and sum to $1 / (2 J) + (J - 1) / J + 1 / (2 J) = 1$ . Their finite weighted sum therefore defines a probability measure $ν_{J}$ on the full power set of $U_{J}$ ; countable additivity reduces to finite additivity because $U_{J}$ is finite.

1.2F2givenalgebra

Define $G_{J} (t) : = ν_{J} ({u \in U_{J} : u < t})$ . If $t = u_{k}$ , the included weights have sum $0$ for $k = 0$ and $(k - \frac{1}{2}) / J$ for $1 \leq k \leq J$ , while $(t + 1) / 2 = k / J$ ; the difference is at most $1 / (2 J)$ . If $u_{k} < t < u_{k + 1}$ , then $G_{J} (t) = (k + \frac{1}{2}) / J$ and $(t + 1) / 2 \in (k / J, (k + 1) / J)$ , again giving difference at most $1 / (2 J)$ . The endpoint $t = - 1$ has both values zero and $t = 1$ is the grid-point case $k = J$ .

2.1step 1.2algebra∎

For $a \leq b$ , the grid points in $[a, b)$ are those with $u \geq a$ and $u < b$ , so $ν_{J} ([a, b)) = G_{J} (b) - G_{J} (a)$ . Subtracting $(b - a) / 2$ and applying step 1.2 at each endpoint gives absolute error at most $1 / (2 J) + 1 / (2 J) = 1 / J$ .

Depends on

Used by

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

Dependency tree · two levels

29 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, Section 8 (standard reference, not scraped)