Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck 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:X→R‾ 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:X→R‾.

[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.1givenL1

Scalar multiples are measurable. If c>0, then {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.

2.1step 1.1L1L2

The threshold identities [step 1.1, L1, L2] {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.1step 2.1L1

Assume f+g is pointwise defined. For every real a, [step 2.1, L1] {f+g>a}=⋃q∈Q({f>q}∩{g>a−q}). 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>a−g(x) works, or f(x) is finite and one may choose a rational q with a−g(x)<q<f(x). Thus [L1] gives measurability of f+g. [step 2.1, L1].

4.1step 3.1L1A1

Suppose first that u,v:X→[0,+∞] are nonnegative and measurable. [step 3.1, L1, A1] If a<0, then {uv>a}=X. If a≥0, then {uv>a}=⋃q∈Q, 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.1step 2.1step 3.1step 4.1L2A1

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+,f−g−,f+g−,f−g+ are measurable. Put h+:=f+g++f−g−,h−:=f+g−+f−g+. 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.1step 1.1step 2.1step 3.1step 4.1step 5.1∎

Steps 1.1 through 5.1 prove all four claims. [step 1.1, step 2.1, step 3.1, step 4.1, step 5.1].

Depends on

Used by

…and 29 more results.

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