TheoremStatement: Literature-sourcedProof: AI-generatedPipeline-generated

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.

Uniform distribution integrates Riemann-integrable functions

Statement

Let $(x_{n})_{n \geq 0}$ be any sequence in $[0, 1)^{d}$ such that $D_{N}^{*} (x_{0}, \dots, x_{N - 1}) ⟶ 0 (N \to \infty) .$ Then for every bounded Riemann-integrable $f : [0, 1]^{d} \to R$ , $\frac{1}{N} \sum_{n = 0}^{N - 1} f (x_{n}) ⟶ I_{d} (f) .$ Here $D_{N}^{*}$ and $I_{d}$ have the conventions of Star discrepancy, digital nets, and digital sequences.

Facts & Assumptions

Given: A sequence with star discrepancy tending to zero and a bounded Riemann-integrable function on the cube.

[F1]

Star discrepancy is the supremum of the empirical-minus-volume error over all anchored boxes $\prod_{j} [0, u_{j})$ , with $u \in [0, 1]^{d}$ . (Star discrepancy, digital nets, and digital sequences)

[F2]

A coordinate grid partitions the cube into finitely many rectangular cells; the lower and upper Darboux sums are the sums of cell infima and suprema times cell volumes. (Grid partitions of a rectangle in $R^{m}$ , their cells, refinements and mesh, Lower and upper Darboux sums over a grid partition in $R^{m}$ )

[F3]

Riemann integrability is equivalent to the existence, for every positive tolerance, of a grid with Darboux gap below that tolerance. (Riemann's criterion on a nondegenerate rectangle in $R^{m}$ : integrability is equivalent to arbitrarily small Darboux gaps) For integrable $f$ , the Darboux definition gives $L (f, G) \leq \sup_{P} L (f, P) = I_{d} (f) = \inf_{P} U (f, P) \leq U (f, G)$ for every grid $G$ . (The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ )

Proof

1.1F1F2F3algebra

Fix $ε > 0$ . By [F3], choose a finite grid $G$ with $U (f, G) - L (f, G) < ε / 2$ . For each closed grid cell $R_{k} = \prod_{j} [t_{j, k_{j}}, t_{j, k_{j} + 1}]$ , write $m_{k} = \inf_{R_{k}} f$ and $M_{k} = \sup_{R_{k}} f$ ; assign empirical points using the disjoint half-open cells $C_{k} = \prod_{j} [t_{j, k_{j}}, t_{j, k_{j} + 1})$ . The empirical frequency error of $C_{k}$ is the alternating sum of the anchored-box errors at its $2^{d}$ vertices, by inclusion–exclusion; hence $∣ N^{- 1} # {n < N : x_{n} \in C_{k}} - vol (C_{k}) ∣ \leq 2^{d} D_{N}^{*}$ .

2.1F2F3step 1.1algebra

Summing $m_{k} \leq f (x_{n}) \leq M_{k}$ over the cells and using step 1.1 gives $L (f, G) - 2^{d} D_{N}^{*} \sum_{k} ∣ m_{k} ∣ \leq N^{- 1} \sum_{n < N} f (x_{n}) \leq U (f, G) + 2^{d} D_{N}^{*} \sum_{k} ∣ M_{k} ∣$ . The grid is fixed and finite, so both finite sums of absolute extrema are finite. For all sufficiently large $N$ , the two discrepancy terms are less than $ε / 2$ . Since $I_{d} (f)$ lies between $L (f, G)$ and $U (f, G)$ by [F3], the empirical average is within $ε$ of $I_{d} (f)$ .

3.1step 2.1∎

As $ε > 0$ was arbitrary, the empirical averages converge to $I_{d} (f)$ .

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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

Art B. Owen, Monte Carlo Book: The Quasi-Monte Carlo Parts, Chapter 15 §15.4, Theorem 15.3 (standard reference, not scraped)
Harald Niederreiter, Random Number Generation and Quasi-Monte Carlo Methods, Chapter 2 §2.1 (standard reference, not scraped)