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

Mixed-derivative formula for smooth Hardy–Krause variation

Statement

Let $d \geq 1$ and let $f : [0, 1]^{d} \to R$ be the continuous extension to the closed cube of a function on $(0, 1)^{d}$ whose mixed partial derivatives of every order at most $d$ exist and extend continuously to $[0, 1]^{d}$ . This is the $C^{d}$ hypothesis here, including agreement of the boundary values of $f$ with its order-zero extension. For $u = {j_{1} < \dots < j_{q}}$ , write $\partial_{u} f$ for the iterated derivative $\partial_{j_{q}} \dots \partial_{j_{1}} f$ , interpreted on the closed cube by its continuous extension. For each nonempty $u$ , let $f_{u} (x_{u}) = f (x_{u}; 1_{- u})$ be the restriction to the face adjacent to the upper corner. Then $V_{H K, 1} (f) = \sum_{\emptyset \neq u \subseteq {1, \dots, d}} \int_{[0, 1]^{∣ u ∣}} ∣ \partial_{u} f (x_{u}; 1_{- u}) ∣ d x_{u},$ where $V_{H K, 1}$ is the upper-anchor variation of Hardy–Krause variation anchored at the upper corner, and $\partial_{u}$ differentiates once in each coordinate in $u$ .

Facts & Assumptions

Given: The cube dimension and the stated continuous mixed-partial hypothesis on $f$ .

[F1]

The upper-anchor Hardy–Krause variation is the sum of the Vitali variations of the face restrictions $f_{u} (x_{u}) = f (x_{u}; 1_{- u})$ over all nonempty coordinate subsets $u$ . (Hardy–Krause variation anchored at the upper corner)

[F2]

If $G$ is continuous on $[a, b]$ , differentiable on $(a, b)$ , and its interior derivative has a Riemann-integrable extension, then its integral is $G (b) - G (a)$ . (Newton–Leibniz needs only continuity on $[a, b]$ , differentiability on $(a, b)$ , and a Riemann-integrable extension of the interior derivative)

[F3]

The closed cube is compact in the Euclidean metric, continuous extensions of the mixed partials are uniformly continuous there, and on $q$ coordinates $d_{2} (x, y)^{2} = \sum_{j = 1}^{q} ∣ x_{j} - y_{j} ∣^{2}$ . (Heine-Borel in $R^{n}$ : with the Euclidean metric a subset of $R^{n}$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line, Heine-Cantor: a continuous map from a compact metric space to any metric space is uniformly continuous, Each $∥ \cdot ∥_{p}$ is a norm on $R^{n}$ , and the induced metrics are exactly $d_{1}$ , $d_{2}$ and $d_{\infty}$ of the published metric-spaces page)

[F4]

A continuous real function on a closed nondegenerate rectangle is Riemann integrable. (Every continuous function on a closed nondegenerate rectangle in $R^{m}$ is Riemann integrable)

[F5]

Iterated Riemann integrals of a Riemann-integrable function on a product rectangle equal its multiple integral whenever the sections in the iterated order are integrable; continuous functions have such sections. (Riemann--Fubini on product rectangles, with lower and upper section integrals and content-zero exceptional sections)

[F6]

Riemann integrals are linear and monotone, satisfy the absolute-value estimate, and are additive under each interior coordinate cut; a constant $c$ integrates over $R$ to $c vol (R)$ by the Darboux definition and rectangle-volume convention. (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in $R^{m}$ , The lower and upper Darboux integrals over a nondegenerate rectangle in $R^{m}$ , Axis-parallel rectangles in $R^{m}$ and their volume)

[F7]

For a bounded Riemann-integrable function, all tagged grid sums converge with mesh to its integral. (The multidimensional Darboux and tagged-mesh definitions of the Riemann integral agree)

[F8]

For every $η > 0$ there is a positive integer $n$ with $1 / n < η$ . (For every $ε > 0$ in a complete ordered field there is a natural $n \geq 1$ with $1 / n < ε$ )

[F9]

The real numbers form an ordered field, and for real $a, b$ , $∣ a + b ∣ \geq ∣ a ∣ - ∣ b ∣$ , obtained from the reverse triangle inequality by applying it to $a + b$ and $a$ . (The reals form a totally ordered field, The reverse triangle inequality)

Proof

1.1F2F3F4F5F6given

Fix a nonempty $u = {j_{1} < \dots < j_{q}}$ and a product cell $R = \prod_{j \in u} [a_{j}, b_{j}]$ in a finite coordinate grid of its face. Put $g = f_{u}$ and $h = \partial_{j_{q}} \dots \partial_{j_{1}} g$ , using the continuous derivative extension. Apply [F2] successively in coordinates $j_{1}, \dots, j_{q}$ . If a line lies on the boundary because some other coordinates are fixed at $0$ or $1$ , approximate those fixed coordinates by interior values and pass to the limit: every intermediate mixed partial and its derivative have continuous extensions, hence are uniformly continuous by [F3]. The integrands therefore converge uniformly along the line, so the integral difference is bounded by the interval length times a uniform error tending to zero; endpoint values converge as well. At each application the finite alternating differences in the remaining coordinates commute with the integral, yielding exactly the alternating sum over the $2^{q}$ vertices. By [F4] and [F5] this iterated integral equals the product-rectangle Riemann integral, so $Δ (g; R) = \int_{R} h$ . Consequently $∣ Δ (g; R) ∣ \leq \int_{R} ∣ h ∣$ . Summing over cells and using the absolute-value estimate and finite grid-cell additivity from [F6] gives $\sum_{R} ∣ Δ (g; R) ∣ \leq \int_{[0, 1]^{q}} ∣ h ∣$ . Taking the supremum over grids proves $V_{V} (g) \leq \int ∣ h ∣$ .

2.1F1F3F4F6F7F8F9step 1.1algebra

Conversely, fix $ε > 0$ . By [F3], choose $δ_{1} > 0$ so that $∣ h (x) - h (y) ∣ < ε / 2$ whenever $d_{2} (x, y) < δ_{1}$ . By [F7] applied to the continuous, hence integrable, function $∣ h ∣$ ([F4]), choose $δ_{2} > 0$ so every tagged grid of mesh below $δ_{2}$ has sum within $ε / 2$ of $\int ∣ h ∣$ . By [F8], choose $n$ with $η = 1 / n < \min {δ_{1} / (q + 1), δ_{2}}$ and take the uniform product grid of side width $η$ . For any two points in one cell, each coordinate difference is at most $η$ , so [F3] gives $d_{2} (x, y)^{2} \leq q η^{2} < δ_{1}^{2}$ because $q < (q + 1)^{2}$ ; hence $d_{2} (x, y) < δ_{1}$ . Tag each cell at its lower corner $ξ_{R}$ . By [F6], linearity and the constant-integral formula give $\int_{R} h = h (ξ_{R}) vol (R) + \int_{R} (h - h (ξ_{R}))$ . Since $∣ h (x) - h (ξ_{R}) ∣ < ε / 2$ throughout $R$ , monotonicity and the absolute-value estimate in [F6] give $∣ \int_{R} (h - h (ξ_{R})) ∣ \leq \int_{R} ∣ h - h (ξ_{R}) ∣ \leq (ε / 2) vol (R)$ . Applying [F9] to $a = h (ξ_{R}) vol (R)$ and $b = \int_{R} (h - h (ξ_{R}))$ yields $∣ \int_{R} h ∣ \geq ∣ h (ξ_{R}) ∣ vol (R) - (ε / 2) vol (R)$ . Summing, using that cell volumes total $1$ , and applying [F7] to the chosen tags gives $\sum_{R} ∣ \int_{R} h ∣ \geq \sum_{R} ∣ h (ξ_{R}) ∣ vol (R) - ε / 2 \geq \int ∣ h ∣ - ε$ . The variation supremum is at least this sum, and arbitrary $ε$ gives $V_{V} (g) \geq \int ∣ h ∣$ .

3.1F1step 1.1step 2.1∎

Thus $V_{V} (f_{u}) = \int ∣ \partial_{u} f (x_{u}; 1_{- u}) ∣$ for each nonempty $u$ . Summing these finitely many equalities and using [F1] gives the displayed formula.

Depends on

Used by

A smooth finite-variation integrand and its deterministic error bound Example

Dependency tree · two levels

92 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 end notes (standard reference, not scraped)
Harald Niederreiter, Random Number Generation and Quasi-Monte Carlo Methods, Chapter 2 §2.2 (standard reference, not scraped)
Lukas Einkemmer, Quasi-Monte Carlo Methods, §2.3 (standard reference, not scraped)