Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicableSession-authored (Fable 5 assisted)judge 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.

The lower and upper Darboux integrals of a bounded ff on [a,b][a,b] as supPL(f,P)\sup_P L(f,P) and infPU(f,P)\inf_P U(f,P), Darboux integrability as their equality, and the notation abf\int_a^b f

Definition

Let a<ba < b be reals and let f:[a,b]Rf : [a,b] \to \mathbb{R} be bounded (Lower bound, bounded below, bounded set). Write P\mathcal{P} for the set of all partitions of [a,b][a,b] (Partition of [a,b][a,b] as a finite strictly increasing list a=t0<t1<<tn=ba = t_0 < t_1 < \dots < t_n = b, its subintervals and their lengths, its mesh, refinement, and the common refinement of two partitions) and put

L  :=  {L(f,P) : PP},U  :=  {U(f,P) : PP}\mathcal{L} \;:=\; \{\, L(f,P) \ : \ P \in \mathcal{P} \,\}, \qquad \mathcal{U} \;:=\; \{\, U(f,P) \ : \ P \in \mathcal{P} \,\}

for the sets of lower and of upper Darboux sums (For bounded ff on [a,b][a,b] and a partition PP: the infimum mim_i and supremum MiM_i of ff on the ii-th subinterval, and the lower and upper Darboux sums L(f,P)=imiΔiL(f,P) = \sum_i m_i \Delta_i and U(f,P)=iMiΔiU(f,P) = \sum_i M_i \Delta_i).

Both extrema exist

P\mathcal{P} is nonempty: the pair (1,t)(1, t) with t0:=at_0 := a and tk:=bt_k := b for k1k \ge 1 is a partition of [a,b][a,b], since a<ba < b. So L\mathcal{L} and U\mathcal{U} are nonempty.

L\mathcal{L} is bounded above and U\mathcal{U} is bounded below. Fix any QPQ \in \mathcal{P}. By claim 2 of 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)L(f,P) \le L(f,P') \le U(f,P') \le U(f,P) when PP' refines PP, and L(f,P)U(f,Q)L(f,P) \le U(f,Q) for arbitrary partitions PP and QQ; moreover the two changes are at most 2M(nn)P2M(n' - n)\|P\|, L(f,P)U(f,Q)L(f,P) \le U(f,Q) for every PPP \in \mathcal{P}, so U(f,Q)U(f,Q) is an upper bound of L\mathcal{L}; and L(f,Q)U(f,P)L(f,Q) \le U(f,P) for every PP, so L(f,Q)L(f,Q) is a lower bound of U\mathcal{U}.

Hence a nonempty set bounded above has a supremum (Complete ordered field (least-upper-bound property)) and a nonempty set bounded below has an infimum (Every nonempty set bounded below has an infimum, Greatest lower bound (infimum)), each unique (Suprema and infima are unique). The lower and upper Darboux integrals of ff over [a,b][a,b] are the real numbers

abf  :=  supL  =  supPL(f,P),abf  :=  infU  =  infPU(f,P).\underline{\int_a^b} f \;:=\; \sup \mathcal{L} \;=\; \sup_{P} L(f,P), \qquad \overline{\int_a^b} f \;:=\; \inf \mathcal{U} \;=\; \inf_{P} U(f,P) .

The lower integral never exceeds the upper one

abf    abf.\underline{\int_a^b} f \;\le\; \overline{\int_a^b} f .

Indeed, for each fixed QPQ \in \mathcal{P} the number U(f,Q)U(f,Q) is an upper bound of L\mathcal{L}, so the least upper bound satisfies abfU(f,Q)\underline{\int_a^b} f \le U(f,Q). As QQ was arbitrary, abf\underline{\int_a^b}f is a lower bound of U\mathcal{U}, and the greatest lower bound satisfies abfabf\underline{\int_a^b} f \le \overline{\int_a^b} f (Greatest lower bound (infimum)).

Moreover, for every partition PP,

L(f,P)    abf    abf    U(f,P),L(f,P) \;\le\; \underline{\int_a^b} f \;\le\; \overline{\int_a^b} f \;\le\; U(f,P) ,

the outer inequalities because a member of a set is at most its supremum and at least its infimum.

Integrability

ff is Darboux integrable on [a,b][a,b], and on this page simply integrable, when

abf  =  abf,\underline{\int_a^b} f \;=\; \overline{\int_a^b} f ,

and then the common value is written

abforabf(x)dx,\int_a^b f \qquad \text{or} \qquad \int_a^b f(x)\,\mathrm{d}x ,

the integral of ff over [a,b][a,b]. It is a single well-determined real number, being the common value of two numbers each of which is unique (Suprema and infima are unique). Without the displayed equality the symbol abf\int_a^b f is not defined and is never written.

The inequality above is the whole difficulty. By the previous paragraph integrability is never a question of one integral exceeding the other, only of the gap abfabf0\overline{\int_a^b} f - \underline{\int_a^b} f \ge 0 being 00; and by Riemann's criterion: a bounded ff on [a,b][a,b] is Darboux integrable if and only if for every real ε>0\varepsilon > 0 there is a partition PP with U(f,P)L(f,P)<εU(f,P) - L(f,P) < \varepsilon that gap is 00 exactly when a single partition can be found making U(f,P)L(f,P)U(f,P) - L(f,P) small. Whether that is possible is settled completely, in terms of the discontinuities of ff, by Lebesgue's criterion for Riemann integrability: a bounded ff on [a,b][a,b] is Riemann integrable if and only if its set of discontinuities has measure zero.

"Riemann integrable" means the same thing here. The definition above is Darboux's. Riemann's own definition, in terms of tagged partitions of small mesh, is Tagged partitions of [a,b][a,b], with a tag ξi\xi_i in each subinterval, and the Riemann sum S(f,P,ξ)=if(ξi)ΔiS(f,P,\xi) = \sum_i f(\xi_i)\,\Delta_i, and the two define the same class of functions with the same integral by The Darboux and Riemann definitions agree: a bounded ff on [a,b][a,b] is Darboux integrable with integral II if and only if for every real ε>0\varepsilon > 0 there is a real δ>0\delta > 0 such that S(f,P,ξ)I<ε|S(f,P,\xi) - I| < \varepsilon for every tagged partition of mesh below δ\delta. Until that theorem is proved the two phrases are kept apart; after it they are used interchangeably, as they are throughout the literature.

Remarks

Depends on

Used by

…and 27 more results.

Dependency tree · next 3 levels

Direct dependencies and their dependencies through the next three levels: 57 results over 14 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.

Sources