Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-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.

Arithmetic and lattice operations preserve measurability whenever they are defined

Statement

Let (X,A) be a measurable space and let f,g:XR be measurable. Then:

  1. cf is measurable for every real scalar c;
  2. max(f,g), min(f,g), f, f+, and f are measurable;
  3. if f+g is pointwise defined, then f+g is measurable;
  4. with the convention of The convention 0=0 is used only for pointwise products of measurable functions, the pointwise product fg is measurable.

Facts & Assumptions

Given: A measurable space (X,A) and measurable functions f,g:XR.

[L1]

Extended-real measurability is equivalent to measurability of the threshold sets {h>a}. (Threshold characterisations of real-valued and extended-real-valued measurability)

[L2]

The positive and negative parts are h+=max(h,0) and h=max(h,0). (The positive and negative parts of a function)

[A1]

In this proof, the pointwise product uses the page convention 0(+)=0()=0.

Proof

technique · direct
1.1

Scalar multiples are measurable. If c>0, then [given, L1] {cf>a}={f>a/c}; if c<0, then {cf>a}={f<a/c}; and if c=0, the function is constant. So [L1] gives measurability of cf, and in particular of f.

givenL1
2.1

The threshold identities

step 1.1L1L2

{max(f,g)>a}={f>a}{g>a},{min(f,g)>a}={f>a}{g>a}

show via [L1] that max(f,g) and min(f,g) are measurable. By [L2], this proves measurability of f+ and f; replacing g by f also gives f=max(f,f). [step 1.1, L1, L2]

3.1

Assume f+g is pointwise defined. For every real a,

step 2.1L1

{f+g>a}=qQ({f>q}{g>aq}).

The inclusion from right to left is immediate. For the converse, if f(x)+g(x)>a then either f(x)=+, in which case any rational q>ag(x) works, or f(x) is finite and one may choose a rational q with ag(x)<q<f(x). Thus [L1] gives measurability of f+g. [step 2.1, L1]

4.1

Suppose first that u,v:X[0,+] are nonnegative and measurable. [step 3.1, L1, A1] If a<0, then {uv>a}=X. If a0, then

{uv>a}=qQ,q>0({u>q}{v>a/q}).

Again the inclusion from right to left is immediate. For the converse, if u(x)v(x)>a, choose a rational q with 0<q<u(x) and a/q<v(x); this is possible because either u(x) is finite positive and the rationals are dense, or u(x)=+, in which case any sufficiently large positive rational works. Hence nonnegative products are measurable by [L1]. [step 3.1, L1, A1]

5.1

For general measurable f and g, step 2.1 gives measurable nonnegative [step 2.1, step 3.1, step 4.1, L2, A1] functions f+,f,g+,g. By step 4.1 the four products f+g+,fg,f+g,fg+ are measurable. Put

h+:=f+g++fg,h:=f+g+fg+.

At each point, at least one of h+ and h is zero, because at least one of f+,f and at least one of g+,g is zero. So the difference h+h is pointwise defined without the forbidden form, and step 3.1 makes it measurable. By the usual sign decomposition, h+h=fg, with the convention [A1] at the 0 points. [step 2.1, step 3.1, step 4.1, L2, A1]

6.1

Steps 1.1 through 5.1 prove all four claims.

step 1.1step 2.1step 3.1step 4.1step 5.1

Depends on

Used by

Dependency tree · two levels

7 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