DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-01

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.

Tagged grid partitions and Riemann sums in $R^{m}$

Definition

A tagging of a grid $P$ assigns to every cell $Q_{i}$ a point $ξ_{i} \in Q_{i}$ . The lower corner is a canonical tagging, so taggings exist without choice. The Riemann sum is $S (f, P, ξ) : = \sum_{i} f (ξ_{i}) vol (Q_{i}),$ with the iterated sum convention of Grid partitions of a rectangle in $R^{m}$ , their cells, refinements and mesh.

The tagged sums converge with mesh to $I$ if for every $ε > 0$ some $δ > 0$ makes $∣ S (f, P, ξ) - I ∣ < ε$ for every tagged grid with mesh below $δ$ . Finite cellwise selections used in proofs are licensed by Every natural-number-indexed list of nonempty sets has a choice function on its family of values and Choice function, not by countable choice.

For bounded $f$ , each tag lies in its cell, so termwise inequalities and nonnegative volumes give $L (f, P) \leq S (f, P, ξ) \leq U (f, P)$ (Lower and upper Darboux sums over a grid partition in $R^{m}$ , Lower bound, bounded below, bounded set).

Tagged grid partitions and Riemann sums in $R^{m}$

Definition

Depends on

Dependency tree · 2 levels

Sources

Tagged grid partitions and Riemann sums in RmRm

Definition

Depends on

Dependency tree · 2 levels

Sources

Tagged grid partitions and Riemann sums in $R^{m}$