Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-27
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 Lebesgue integral is linear on L1(μ)

Statement

The class L1(μ) is a complex vector space, and the Lebesgue integral is complex-linear on it: (αf+βg)dμ=αfdμ+βgdμ(α,βC, f,gL1(μ)).

Facts & Assumptions

Given: Integrable functions f,gL1(μ) and scalars α,βC.

[L1]

Real and complex integrability, together with the decomposition into positive and negative parts and into real and imaginary parts, is defined in Integrable real and complex functions, and their integrals.

[L2]

The nonnegative integral is additive (Additivity of the nonnegative Lebesgue integral).

[L3]

The nonnegative integral is monotone and homogeneous (Monotonicity and nonnegative homogeneity of the nonnegative integral).

[L4]

Sums and real scalar multiples of measurable real-valued functions are measurable (Closure properties of measurable functions used by the integral).

Proof

technique · direct
1.1

First treat real-valued f,g and put h:=f+g. By [L4], the function h is measurable. Also h+f++g+,hf+g, so [L2] and [L3] give h+dμf+dμ+g+dμ<+,hdμfdμ+gdμ<+. Hence h is integrable. Since h++f+g=h+f++g+, another application of [L2] yields h+dμ+fdμ+gdμ=hdμ+f+dμ+g+dμ, which rearranges to (f+g)dμ=fdμ+gdμ.

L1L2L3L4algebra
1.2

Now let cR and let f be real-valued. By [L4], cf is measurable. If c0, then (cf)+=cf+,(cf)=cf; if c<0, then (cf)+=(c)f,(cf)=(c)f+. In both cases [L3] shows that cf is integrable and that (cf)dμ=cfdμ.

L1L3L4algebra
2.1

Let h=u+ivL1(μ) and γ=a+ibC. Then γh=(aubv)+i(av+bu). The real-valued functions aubv and av+bu are integrable by steps 1.1 and 1.2, and their real-linear integral formulas combine into (γh)dμ=γhdμ. Writing αf=h1+ik1 and βg=h2+ik2 with real-valued integrable hj,kj, step 1.1 gives (αf+βg)dμ=(h1+h2)dμ+i(k1+k2)dμ=h1dμ+ik1dμ+h2dμ+ik2dμ=αfdμ+βgdμ.

L1step 1.1step 1.2algebra

Depends on

Used by

Dependency tree · two levels

11 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