Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (z-ai/glm-5.2)audited 2026-07-29
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 integral with oriented limits: ∫aaf:=0 and ∫baf:=−∫abf

Definition

Why this item is first. The published definition of the integral does not cover this page. The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf is stated for reals a<b, because the partitions it quantifies over are those of 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, whose standing hypothesis is a<b: with a=b the chain a=t0<⋯<tn=b is unsatisfiable. So ∫abf is an undefined symbol whenever a≥b, and every additivity statement below would be ill-formed as it is usually written. This item extends the notation, and nothing else: the object it names is still the Darboux integral of The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf.

Let u,v∈R and write

[u∧v, u∨v]  :=  the closed interval with endpoints u and v

(Intervals of R: the nine order-convex forms, nondegeneracy, and length). Let f be a real-valued function whose domain contains that interval. Say that f is integrable between u and v when either u=v, or u≠v and the restriction of f to [u∧v, u∨v] is bounded (Lower bound, bounded below, bounded set) and Darboux integrable there (The lower and upper Darboux integrals of a bounded f on [a,b] as sup⁡PL(f,P) and inf⁡PU(f,P), Darboux integrability as their equality, and the notation ∫abf, For bounded f on [a,b] and a partition P: the infimum mi and supremum Mi of f on the i-th subinterval, and the lower and upper Darboux sums L(f,P)=∑imiΔi and U(f,P)=∑iMiΔi). For such f define

∫uvf  :=  {the Darboux integral of f over [u,v]if u<v,0if u=v,−∫vufif u>v.

There is nothing to check for consistency. The three clauses are indexed by the three cases of trichotomy, u<v, u=v and u>v, which are mutually exclusive and exhaustive; no pair of them ever applies to the same (u,v). In particular the first clause is untouched, so on u<v this is the published integral verbatim and every published theorem about it applies unchanged.

The middle clause is a stipulation, not a computation. It is not claimed that 0 is a value forced by the u<v definition in any limiting sense; that definition simply says nothing at u=v, and ∫uuf:=0 is what is written there. It is also unconditional: no hypothesis on f beyond being defined at u is asked for, since the case u=v never refers to a partition.

The two consequences used throughout the page

Antisymmetry, for every pair. For all reals u,v with f integrable between them,

∫uvf  =  −∫vuf.

Indeed if u<v then v>u and the third clause reads ∫vuf=−∫uvf, which rearranges to the display; if u=v both sides are 0; and if u>v the third clause is the display itself.

Absolute values agree. Consequently ∣∫uvf∣=∣∫vuf∣ for every such pair.

An obligation recorded here and discharged elsewhere. With this convention the additivity identity

∫uvf  +  ∫vwf  =  ∫uwf

holds for every arrangement of u,v,w in an interval on which f is integrable, not only for u<v<w. That is a theorem and not part of this definition; it is proved as the last clause of For a<c<b: f is integrable on [a,b] if and only if it is integrable on [a,c] and on [c,b], and then ∫abf=∫acf+∫cbf; with the oriented form for arbitrary a,b,c, and nothing on this page uses it before it is proved there.

Remarks

  • This is notation, and it is a real notation. Without it the substitution theorem could not be stated with the limits φ(c) and φ(d) in the order the map produces them, since a differentiable φ need be neither injective nor monotone; and the integral function x↦∫axf would be undefined at x=a.

  • One published inequality is not orientation-invariant, and that is a trap. The estimate ∣∫uvf∣≤∫uv∣f∣ is guaranteed only for u≤v: at u>v the right-hand side is −∫vu∣f∣≤0 while the left-hand side is ≥0, so the inequality fails whenever ∫vu∣f∣>0. The form valid for every pair is ∣∫uvf∣≤∣∫uv∣f∣∣, and this is stated where it is proved (If f,g are integrable on [a,b] then so are ∣f∣, f2, fg, max⁡(f,g) and min⁡(f,g), and ∣∫abf∣≤∫ab∣f∣).

  • Integrability is a property of the unordered pair. By construction, f is integrable between u and v if and only if it is integrable between v and u, since both refer to the same closed interval; only the sign of the value remembers the order.

Depends on

Used by

…and 12 more results.

Dependency tree · two levels

29 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