Alphabeta Math
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-26
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.

The divergence at a point is the limit of outward flux per unit volume

Statement

Let O⊆R3 be open, let F:O→R3 be C1 and let p∈O. For each m∈N let a finite gluing of elementary solid regions be given whose union E(m) satisfies E(m)⊆O, p∈E(m) and cont⁡(E(m))>0, and suppose diam⁡(E(m))→0. Then

lim⁡m→∞1cont⁡(E(m))∬∂E(m)⟨F,n⟩=div⁡F(p),

that is: for every rational ε>0 there is M such that every m≥M satisfies

∣1cont⁡(E(m))∬∂E(m)⟨F,n⟩−div⁡F(p)∣<ε.

Positive content is required only so that the quotient is defined; no relation between the content and the diameter is assumed.

Facts & Assumptions

Given: The open O⊆R3, the C1 field F on O, the point p∈O, and for each m the finite gluing with union E(m)⊆O containing p, of positive content, with diam⁡(E(m))→0.

[F1]

The divergence of a C1 field is div⁡G=∑i<n∂iGi; a C1 map has continuous first partial derivatives, so div⁡G is continuous (Divergence and curl of a C1 vector field, Ck Euclidean maps and diffeomorphisms).

[F3]

For a nonempty bounded A in a metric space, diam⁡(A)=sup⁡{d(a,b):a,b∈A} (Bounded subset, diameter, distance from a point to a set, and distance between two sets in a metric space), the metric on R3 being d(a,b)=∥a−b∥2 (The Euclidean inner product ⟨x,y⟩=∑k<nxkyk on Rn).

[F4]

A map between metric spaces is continuous at a point when for every real ε>0 there is a real δ>0 such that points within δ of it have images within ε (Continuity of a map between metric spaces, at a point and globally, in the ε-δ form).

[F5]

A sequence of reals converges to x when for every rational ε>0 there is K with ∣xk−x∣<ε for all k≥K (Limits and Cauchy sequences of reals).

[L1]

For a finite gluing with union E and outer presentation Σout and a C1 field G on an open set containing E, ∭Ediv⁡G=∬∂E⟨G,n⟩ (The divergence theorem for finite gluings of elementary solid regions).

[L3]

For integrable f,g on a nondegenerate rectangle and scalars α,β: αf+βg is integrable with integral α∫f+β∫g; if f≤g then ∫f≤∫g; and ∣f∣ is integrable with ∣∫f∣≤∫∣f∣ (Linearity, monotonicity, the absolute-value estimate and coordinate-slice additivity for the Riemann integral in Rm).

[L4]

Every continuous real function on a compact Jordan measurable set is Riemann integrable over it (A continuous real function on a compact Jordan measurable set is Riemann integrable over that set).

Proof

technique · direct
1.1givenF1L1L2L4

For each m the set E(m) is compact and Jordan measurable by [L2], and div⁡F is continuous on O by [F1], hence integrable over E(m) by [L4]. Since F is C1 on the open O⊇E(m), [L1] gives ∬∂E(m)⟨F,n⟩=∫E(m)div⁡F.

1.2givenF1F3F4F5

Let ε>0 be rational. The function div⁡F is continuous at p by [F1], so [F4] with the real number ε/2 supplies δ>0 such that every q∈O with ∥q−p∥2<δ satisfies ∣div⁡F(q)−div⁡F(p)∣<ε/2. Since diam⁡(E(m))→0, there is M with diam⁡(E(m))<δ for every m≥M.

2.1step 1.1step 1.2F2F3L3

Fix m≥M. Since p∈E(m), every q∈E(m) has ∥q−p∥2≤diam⁡(E(m))<δ by [F3], so step 1.2 bounds ∣div⁡F−div⁡F(p)∣ by ε/2 on E(m). By [L3] and [F2], ∫E(m)div⁡F(p)=div⁡F(p)cont⁡(E(m)), and ∣∫E(m)div⁡F−div⁡F(p)cont⁡(E(m))∣=∣∫E(m)(div⁡F−div⁡F(p))∣≤∫E(m)ε2=ε2cont⁡(E(m)).

3.1step 2.1F5∎

Dividing the estimate of step 2.1 by the positive number cont⁡(E(m)) and substituting step 1.1 gives ∣1cont⁡(E(m))∬∂E(m)⟨F,n⟩−div⁡F(p)∣≤ε2<ε for every m≥M. As ε was an arbitrary positive rational, [F5] gives the asserted limit.

Remarks

  • No shape hypothesis is needed. The content cancels between the estimate and the quotient, so nothing forces the solids to be balls, cubes or comparable to their diameters. What is needed is that each carries the gluing data, that each contains p, and that the diameters vanish.

  • Positive content is a hypothesis about the quotient, not about the estimate. Step 2.1 holds whatever cont⁡(E(m)) is; step 3.1 divides by it. A solid of content zero would make the left-hand side undefined rather than make the estimate fail.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

76 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