Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passverified 2026-08-10 (gpt-5.6-terra-codex-subscription)
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.

Integrable functions on [a,b] form a set closed under sums and scalar multiples, and ∫ab(λf+μg)=λ∫abf+μ∫abg

Statement

Let a<b be reals and let f,g:[a,b]→R be integrable (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). Then:

  1. f+g is integrable on [a,b] and ∫ab(f+g)=∫abf+∫abg;
  2. for every real λ, λf is integrable on [a,b] and ∫abλf=λ∫abf;
  3. consequently, for all reals λ,μ the function λf+μg is integrable and ∫ab(λf+μg)  =  λ∫abf  +  μ∫abg;
  4. the same identity holds with oriented limits: if u,v∈[a,b] and f,g are integrable between u and v (The integral with oriented limits: ∫aaf:=0 and ∫baf:=−∫abf), then ∫uv(λf+μg)=λ∫uvf+μ∫uvg.

Linearity of the integral is not linearity of the Darboux sums, and the proof of claim 1 has to squeeze rather than compute. On a subinterval the inequality sup⁡(f+g)≤sup⁡f+sup⁡g can be strict — take f(x)=x and g(x)=−x on [0,1], where the left side is 0 and the right side is 1 — so U(f+g,P) is in general strictly below U(f,P)+U(g,P) and no identity between upper sums is available. Claim 2, by contrast, is an identity at the level of the sums, with the roles of sup⁡ and inf⁡ exchanged when λ<0.

Facts & Assumptions

Given: Reals a<b, integrable f,g:[a,b]→R, reals λ,μ, and a real ε>0.

[L1]

Riemann's criterion: a bounded h on [a,b] is integrable if and only if for every real η>0 there is a partition P with U(h,P)−L(h,P)<η (Riemann's criterion: a bounded f on [a,b] is Darboux integrable if and only if for every real ε>0 there is a partition P with U(f,P)−L(f,P)<ε).

[L2]

For every partition P and bounded h: L(h,P)≤∫ab‾h≤∫ab‾h≤U(h,P), and h is integrable exactly when the two integrals agree, their common value being ∫abh; the lower integral is sup⁡PL(h,P) and the upper is inf⁡PU(h,P) (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, Suprema and infima are unique).

[L3]

L(h,P)=∑i<nmi(h)Δi and U(h,P)=∑i<nMi(h)Δi, where mi(h)=inf⁡h[Ii] and Mi(h)=sup⁡h[Ii] over the subintervals Ii of P=(n,t), with Δi>0; an integrable function is bounded, and a sum of two bounded functions and a scalar multiple of a bounded function are bounded (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, 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, Lower bound, bounded below, bounded set).

[L5]

Finite sums are additive and homogeneous: ∑i<n(xi+yi)=∑i<nxi+∑i<nyi and ∑i<nλxi=λ∑i<nxi (Finite sums and finite products, by recursion, Laws of finite sums and finite products, clauses 1 and 2).

[L6]

A supremum is the least upper bound and an infimum the greatest lower bound; both exist for a nonempty bounded set and are unique (Complete ordered field (least-upper-bound property), Greatest lower bound (infimum), Suprema and infima are unique).

[L7]

Reflection: writing −S={−s:s∈S}, a real u is an upper bound of S exactly when −u is a lower bound of −S, and conversely; hence sup⁡(−S)=−inf⁡S and inf⁡(−S)=−sup⁡S for nonempty bounded S, by [L6] (Reflection through zero exchanges upper and lower bounds).

[L9]

Ordered-field arithmetic: adding a constant and multiplying by a positive quantity preserve an inequality, the order is total and transitive, and a real x with ∣x∣<η for every real η>0 is 0 (Ordered field, Complete ordered field (least-upper-bound property)). These order facts are used in their nonstrict form as well, obtained by adjoining the case of equality.

[L10]

With oriented limits, ∫vuh=−∫uvh and ∫uuh=0 (The integral with oriented limits: ∫aaf:=0 and ∫baf:=−∫abf).

Proof

technique · direct
1.1

f, g, f+g and λf are bounded on [a,b], so all their Darboux sums and integrals are defined.

givenL3
1.2

For every partition P=(n,t) and every i<n: f(x)+g(x)≤Mi(f)+Mi(g) for x∈Ii, so Mi(f)+Mi(g) is an upper bound of (f+g)[Ii] and Mi(f+g)≤Mi(f)+Mi(g) by [L6]; dually mi(f+g)≥mi(f)+mi(g).

L3L6
1.3

Fix partitions P1 and P2 with U(f,P1)−L(f,P1)<ε⋅2−1 and U(g,P2)−L(g,P2)<ε⋅2−1, and put P:=P1∨P2.

givenL1L4choose
1.4

Claim 2, the case λ=0. Then λf is the constant function 0, integrable with integral 0=0⋅∫abf.

L8
1.5

Claim 2, the case λ>0. For every partition P and every i<n, λMi(f) is an upper bound of (λf)[Ii], and any upper bound w of (λf)[Ii] gives the upper bound w/λ of f[Ii], whence Mi(f)≤w/λ and λMi(f)≤w; so Mi(λf)=λMi(f) by [L6], and dually mi(λf)=λmi(f).

L3L6L9
1.6

Claim 2, the case λ=−1. For every P and i<n, (−f)[Ii]=−(f[Ii]), so Mi(−f)=−mi(f) and mi(−f)=−Mi(f) by [L7].

L3L7
2.1

By [L4], U(f,P)−L(f,P)<ε⋅2−1 and U(g,P)−L(g,P)<ε⋅2−1.

step 1.3L4
2.2

Summing the inequalities of step 1.2 over i<n against the positive weights Δi and using [L5] gives L(f,P)+L(g,P)≤L(f+g,P)≤U(f+g,P)≤U(f,P)+U(g,P).

step 1.2L3L5L9
2.3

With step 1.5 and [L5], U(λf,P)=λU(f,P) and L(λf,P)=λL(f,P) for λ>0; hence U(λf,P)−L(λf,P)=λ(U(f,P)−L(f,P)), which [L1] makes smaller than any prescribed positive number by choosing P suitably, so λf is integrable.

step 1.5L1L3L5L9
2.4

With step 1.6 and [L5], U(−f,P)=−L(f,P) and L(−f,P)=−U(f,P), so U(−f,P)−L(−f,P)=U(f,P)−L(f,P) and −f is integrable by [L1]; and by [L7] applied to the sets of Darboux sums, ∫ab‾(−f)=−∫ab‾f and ∫ab‾(−f)=−∫ab‾f, so ∫ab(−f)=−∫abf.

step 1.6L1L2L5L7
3.1

Hence U(f+g,P)−L(f+g,P)≤(U(f,P)−L(f,P))+(U(g,P)−L(g,P))<ε, so f+g is integrable by [L1], ε>0 having been arbitrary.

step 1.1step 2.1step 2.2L1L9
3.2

Moreover the set of lower sums of λf is λ times the set of lower sums of f, and a supremum scales by a positive factor, by the argument of step 1.5 applied to that set; so ∫ab‾λf=λ∫ab‾f, and likewise for the upper integrals, giving ∫abλf=λ∫abf.

step 1.5step 2.3L2L6L9
4.1

Both ∫ab(f+g) and ∫abf+∫abg lie in the interval from L(f,P)+L(g,P) to U(f,P)+U(g,P): the first by [L2] and step 2.2, the second by [L2] applied to f and to g separately.

step 2.1step 2.2step 3.1L2
4.2

Claim 2 for λ<0. Then −λ>0 and λf=(−λ)(−f), so steps 2.3, 2.4 and 3.2 give integrability and the required identities and ∫abλf=(−λ)∫ab(−f)=(−λ)(−∫abf)=λ∫abf.

step 2.3step 3.2step 2.4L9
5.1

That interval has length less than ε by step 2.1, so ∣∫ab(f+g)−∫abf−∫abg∣<ε; as ε>0 was arbitrary the difference is 0, which is claim 1.

step 2.1step 4.1L9
5.2

Claim 2 is now proved in all three cases λ=0, λ>0 and λ<0, which are exhaustive by trichotomy.

step 1.4step 2.3step 3.2step 4.2L9
6.1

Claim 3. By claim 2 the functions λf and μg are integrable with integrals λ∫abf and μ∫abg, and by claim 1 their sum is integrable with the sum of those integrals.

step 5.1step 5.2
7.1

Claim 4. If u<v then u,v∈[a,b] and claim 3 applies verbatim on [u,v]; if u=v both sides are 0 by [L10]; and if u>v then applying the case u<v to the pair (v,u) and multiplying by −1 gives the identity, by [L10].

step 6.1L10∎

Remarks

Depends on

Used by

Dependency tree · two levels

41 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