Alphabeta Math
DefinitionDefinition: AI-adaptedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-28
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.

Partition of [a,b] as a finite strictly increasing list a=t0<t1<⋯<tn=b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions

Definition

Standing hypothesis for this page. Throughout, R is the complete ordered field (Complete ordered field (least-upper-bound property), Ordered field), N is the set of natural numbers and contains 0 (The natural numbers N (von Neumann), Order on the natural numbers), ι:N→R is the canonical natural (The canonical natural ι(n)=n⋅1F of a field), and a,b are reals with

a  <  b.

Intervals and their lengths are those of Intervals of R: the nine order-convex forms, nondegeneracy, and length; finite sums are those of Finite sums and finite products, by recursion, indexed as ∑i<n over i∈N.

Partitions

A partition of [a,b] is a pair P=(n,t) consisting of a natural number n≥1 and a sequence t:N→R (Sequences of reals: bounded, eventually, frequently, tails, subsequences) with

t0=a,ti<ti+1  for every i<n,tk=b  for every k≥n.

The tail convention on the third clause is bookkeeping only: it makes t a genuine sequence, so that the finite-sum laws of Laws of finite sums and finite products apply to it verbatim, and it costs nothing because no index above n is ever read. The first two clauses say exactly that

a  =  t0  <  t1  <  …  <  tn  =  b,

the last equality because tn=b by the third clause. In particular i↦ti is strictly increasing, hence injective, on { i∈N:i≤n } (Injection, surjection, bijection), and a≤ti≤b for every i≤n.

The point set of P is the finite set

pts⁡(P)  :=  { ti : i≤n }  ⊆  [a,b],a,b∈pts⁡(P).

The subintervals of P are

Ii  :=  [ ti, ti+1 ](i<n),

and their lengths are Δi:=ti+1−ti. Each Δi>0, so each Ii is a nondegenerate closed bounded interval (Intervals of R: the nine order-convex forms, nondegeneracy, and length). There are n of them and they are indexed from i=0, not from i=1: the first subinterval is [t0,t1]=[a,t1].

The lengths sum to b−a. By the telescoping law, clause 5 of Laws of finite sums and finite products,

∑i<nΔi  =  ∑i<n(ti+1−ti)  =  tn−t0  =  b−a.

The mesh. The set { Δi:i<n } is a nonempty finite set of reals, nonempty because n≥1, so it has a maximum (Every nonempty finite set of reals has a maximum and a minimum, Maximum and minimum of a set). The mesh of P is

∥P∥  :=  max⁡{ Δi : i<n }  >  0,

and Δi≤∥P∥ for every i<n.

The uniform partition. For a natural N≥1, the uniform partition of [a,b] into N parts is UN:=(N,t) with

ti  :=  a+ι(i) b−aι(N)(i≤N),tk:=b(k≥N).

This is a partition: t0=a; tN=a+(b−a)=b; and ti+1−ti=(b−a)/ι(N)>0 for i<N, because ι(N)>0 and ι(i+1)=ι(i)+1 (Canonical naturals are positive and strictly increasing, The canonical natural ι(n)=n⋅1F of a field). Its subinterval lengths are all equal to (b−a)/ι(N), so

∥UN∥  =  b−aι(N).

A partition is determined by its point set

Claim. If P=(n,t) and P′=(n′,t′) are partitions of [a,b] with pts⁡(P)=pts⁡(P′), then n=n′ and ti=ti′ for every i≤n.

Proof. First, ti=ti′ for every i≤min⁡{n,n′}, by induction on i (The principle of mathematical induction). For i=0 both equal a. Suppose tj=tj′ for all j≤i and i+1≤min⁡{n,n′}. The set S:={ x∈pts⁡(P):x>ti } has ti+1 as its least element: ti+1∈S, and any x∈S is tj for some j≤n with tj>ti, which forces j>i because t is increasing on indices ≤n, hence j≥i+1 and x=tj≥ti+1. The same argument in P′ makes ti+1′ the least element of { x∈pts⁡(P′):x>ti′ }, which is the same set S, since the point sets agree and ti′=ti. A set has at most one least element (Maximum and minimum of a set), so ti+1=ti+1′.

Second, n=n′. If n<n′ then tn′=tn=b by the previous paragraph, while tn′<tn′′=b because t′ is increasing on indices ≤n′ and n<n′; that is impossible. Exchanging the roles of P and P′ rules out n′<n. □

So the map P↦pts⁡(P) is injective, and a partition may be named by its point set whenever one is exhibited.

Inserting a point

Let P=(n,t) be a partition of [a,b] and let c∈[a,b]. Define a partition P+c of [a,b] as follows.

  • If c∈pts⁡(P), put P+c:=P.
  • Otherwise c≠a and c≠b, so a<c<b. The set T:={ ti:i≤n and ti<c } is a nonempty finite set of reals, nonempty because t0=a<c, so it has a maximum (Every nonempty finite set of reals has a maximum and a minimum); let i0≤n be the unique index with ti0=max⁡T, unique because t is injective on indices ≤n. Then i0<n, since tn=b>c puts tn∉T; and ti0  <  c  <  ti0+1, the right inequality because ti0+1≠c (as c∉pts⁡(P)) and ti0+1<c would put ti0+1∈T with ti0+1>ti0=max⁡T. Put P+c:=(n+1,s) with si:=ti (i≤i0),si0+1:=c,si:=ti−1 (i0+2≤i≤n+1),sk:=b (k≥n+1).

In both cases P+c is a partition of [a,b] and

pts⁡(P+c)  =  pts⁡(P)∪{c},∥P+c∥  ≤  ∥P∥.

The displayed identity is immediate from the two cases. For the mesh: in the first case nothing changes; in the second the list of subinterval lengths of P+c is that of P with Δi0 replaced by the two numbers c−ti0 and ti0+1−c, each of which is smaller than Δi0=(c−ti0)+(ti0+1−c) because the other is positive. So every length of P+c is at most a length of P, and the maximum cannot increase. Finally the index count grows by exactly 1 in the second case and not at all in the first.

Refinement and the common refinement

P′ refines P, and is a refinement of P, when

pts⁡(P)  ⊆  pts⁡(P′).

Let P=(n,t) and Q=(m,s) be partitions of [a,b]. Applying the recursion theorem (The recursion theorem) to the set N×P[a,b], where P[a,b] is the set of partitions of [a,b], with starting element (0,P) and the map (j,R)↦(j+1, R+sj) — legitimate because sj∈[a,b] for every j∈N — gives a unique family (Rj)j∈N of partitions with R0=P and Rj+1=Rj+sj. The common refinement of P and Q is

P∨Q  :=  Rm+1.

Its point set is the union. By induction on j (The principle of mathematical induction), pts⁡(Rj)=pts⁡(P)∪{ sl:l<j }; taking j=m+1 gives

pts⁡(P∨Q)  =  pts⁡(P)∪pts⁡(Q).

Hence P∨Q refines both P and Q; by the uniqueness claim above it is the only partition with that point set, so P∨Q=Q∨P, and

P′ refines P⟹P∨P′=P′,

since then pts⁡(P)∪pts⁡(P′)=pts⁡(P′).

Two size bounds, both used later. Writing nR for the first component of a partition R:

∥P∨Q∥  ≤  ∥P∥,nP∨Q  ≤  nP+nQ−1.

The first is the mesh bound above applied m+1 times. For the second, each insertion raises the index count by at most 1, and the two insertions of s0=a and sm=b raise it by 0, since a and b already lie in pts⁡(P) and hence in pts⁡(Rj) for every j; so at most m−1 of the m+1 insertions increase it.

The index map of a refinement

Let P′=(n′,t′) refine P=(n,t). For each i≤n the point ti lies in pts⁡(P′), so there is exactly one φ(i)≤n′ with tφ(i)′=ti, uniqueness because t′ is injective on indices ≤n′. The resulting map φ satisfies

φ(0)=0,φ(n)=n′,φ(i)<φ(i+1)  (i<n),

the first two because t0′=a=t0 and tn′′=b=tn together with injectivity, and the third because ti<ti+1 and t′ is increasing on indices ≤n′. In particular n≤n′. Moreover, for i<n and φ(i)≤j<φ(i+1),

Ij′  =  [ tj′, tj+1′ ]  ⊆  [ ti, ti+1 ]  =  Ii,

because ti=tφ(i)′≤tj′ and tj+1′≤tφ(i+1)′=ti+1.

The blocks are counted by telescoping. By clause 5 of Laws of finite sums and finite products, ∑i<n(φ(i+1)−φ(i))=φ(n)−φ(0)=n′, so, subtracting ∑i<n1=n,

∑i<n(φ(i+1)−φ(i)−1)  =  n′−n,

a sum of n nonnegative integers, one for each block, which vanishes exactly at the blocks consisting of a single index. This identity is the whole content of the quantitative bound in Refining a partition raises the lower Darboux sum and lowers the upper one, and every lower sum is at most every upper sum: L(f,P)≤L(f,P′)≤U(f,P′)≤U(f,P) when P′ refines P, and L(f,P)≤U(f,Q) for arbitrary partitions P and Q; moreover the two changes are at most 2M(n′−n)∥P∥, and it is also why n≤n′.

Finally, the lengths inside a block sum to the length of the block:

∑j=φ(i)φ(i+1)−1Δj′  =  tφ(i+1)′−tφ(i)′  =  ti+1−ti  =  Δi(i<n),

again by telescoping, applied to the sequence l↦tφ(i)+l′ and read through the index-shift convention of Finite sums and finite products, by recursion.

Remarks

Depends on

Used by

…and 36 more results.

Dependency tree · two levels

34 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