Measurable function: checking every preimage by complete enumeration, with composition, indicators and the image-set trap

Goal and scope

X={0,1,2,3}, Σ_X={∅,{0,1},{2,3},X}; Y={0,1,2}, Σ_Y={∅,{0},{1,2},Y}; Z={0,1} with Σ_Z the power set. (1) Prove by complete enumeration that f=(0↦0,1↦0,2↦1,3↦2) is measurable and g=(0↦0,1↦1,2↦1,3↦2) is not; (2) prove that a composite of measurable maps is measurable, and read φ∘f back as an indicator function; (3) prove that an indicator 1_E is measurable exactly when E∈Σ_X; (4) use m and k to show that 'checking images' can both wrongly reject and wrongly accept.

Treats only the finite measurable spaces and complete total-map tables of G1 to G5 (MKO assumption a1). Complete finite enumeration establishes only these instances; the composition lemma and the indicator lemma are proved for arbitrary measurable spaces. Measurability does not imply continuity, integrability or measure preservation (a2). The canonical MKO and its English edition are not changed.

Givens and symbols

• image_preimage_def
• set_operations_def
• function_def
• composition_def
• set_extensionality

• G1 — X={0,1,2,3}, Σ_X={∅,{0,1},{2,3},X}.
• G2 — Y={0,1,2}, Σ_Y={∅,{0},{1,2},Y}.
• G3 — Complete map tables: f(0)=0, f(1)=0, f(2)=1, f(3)=2; g(0)=0, g(1)=1, g(2)=1, g(3)=2.
• G4 — Z={0,1}, Σ_Z={∅,{0},{1},Z}; φ:Y→Z with φ(0)=0, φ(1)=1, φ(2)=1.
• G5 — Image-trap examples: m:X→Y with m(0)=0, m(1)=0, m(2)=1, m(3)=1; k:X→Z with k(0)=0, k(1)=1, k(2)=1, k(3)=1.

• (X,\Sigma_X) — the source measurable space, X={0,1,2,3}
• (Y,\Sigma_Y) — the target measurable space, Y={0,1,2}
• (Z,\Sigma_Z) — Z={0,1} with Σ_Z the power set
• f,g,m:X\to Y — the total maps to be checked
• \varphi:Y\to Z,\ k:X\to Z — the map used for composition and the image-trap example
• u^{-1}(B) — the preimage {x ∣ u(x)∈B}
• \mathbf{1}_E — the indicator function of E

Rules and sources

• image_preimage_def · prerequisite — Image and preimage: f(S)={f(a) ∣ a∈S}; f⁻¹(T)={a∈A ∣ f(a)∈T}. The preimage notation does not presuppose that f has an inverse.
• set_operations_def · prerequisite — Set operations: x∈A∪B ⇔ x∈A or x∈B; x∈A∩B ⇔ x∈A and x∈B; x∈A∖B ⇔ x∈A and x∉B; in a universe U, Aᶜ=U∖A.
• function_def · prerequisite — Function: f:A→B assigns to each a∈A exactly one f(a)∈B. Two functions are equal ⇔ they have the same domain and codomain and agree at every a.
• composition_def · prerequisite — Composition: for f:A→B and g:B→C, g∘f:A→C is defined by (g∘f)(a)=g(f(a)).
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• def_unfold · prerequisite — Unfolding a definition: replacing a defined term by its definition (or folding it back) does not change whether a statement is true.
• case_analysis · prerequisite — Proof by cases: if P∨Q holds and both P⇒R and Q⇒R are proved, then R holds. The cases must cover every possibility.
• set_builder · prerequisite — Set-builder notation: x∈{y∈A ∣ P(y)} if and only if x∈A and P(x).
• forall_intro · prerequisite — ∀-introduction (generalization): if a statement is proved for an arbitrary element x, with no extra assumption on x, it holds for every x in the domain.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• forall_elim · prerequisite — ∀-elimination (instantiation): if ∀x∈D, P(x) holds and a∈D, then P(a) holds.
• iff_intro · prerequisite — Biconditional: P⇔Q holds exactly when both P⇒Q and Q⇒P hold.
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• mko_measurable_def · cited — Given finite measurable spaces (X,Σ_X) and (Y,Σ_Y), a total function f:X→Y is measurable if f⁻¹(B) belongs to Σ_X for every B in Σ_Y. This slice checks each preimage by complete finite enumeration. · mko-measurable-function
• mko_sigma_def · cited — On a set X, a sigma-algebra contains the empty set and is closed under complements and countable unions; a complete finite carrier permits reduction of the countable obligations to finitely many distinct sets. · mko-sigma-algebra-measure-space
• p_indicator_def · prerequisite — For E⊆X, the indicator 1_E:X→{0,1} has 1_E(x)=1 if x∈E and 1_E(x)=0 otherwise.
• L_comp_meas · lemma — For arbitrary measurable spaces, if u:(A,𝒜)→(B,ℬ) and ψ:(B,ℬ)→(C,𝒞) are measurable, then (ψ∘u)⁻¹(D)=u⁻¹(ψ⁻¹(D)) for every D⊆C, and ψ∘u is measurable.
• L_indicator · lemma — For any measurable space (X,Σ) and E⊆X, with the power set of {0,1} as target sigma-algebra, 1_E is measurable ⇔ E∈Σ.

Main derivation

u:(X,\Sigma_X)\to(Y,\Sigma_Y)\ \text{measurable}

\forall B\in\Sigma_Y:\ u^{-1}(B)\in\Sigma_X

\Sigma_X,\ \Sigma_Y,\ \Sigma_Z

\text{each is a}\ \sigma\text{-algebra on its carrier}

f:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto2

f:X\to Y\ \text{total}

u:X\to Y\ \text{total}

u^{-1}(\emptyset)=\emptyset\in\Sigma_X,\quad u^{-1}(Y)=X\in\Sigma_X

f^{-1}(\{0\})

\{x\mid f(x)=0\}=\{0,1\}\in\Sigma_X

f^{-1}(\{1,2\})

\{x\mid f(x)\in\{1,2\}\}=\{2,3\}\in\Sigma_X

B\in\{\emptyset,\{0\},\{1,2\},Y\}

f^{-1}(B)\in\Sigma_X\ \text{for every}\ B\in\Sigma_Y:\ f\ \text{measurable}

g^{-1}(\{0\})

\{0\}\notin\Sigma_X:\ g\ \text{not measurable}

u,\ \psi\ \text{measurable}

(\psi\circ u)^{-1}(D)=u^{-1}(\psi^{-1}(D)),\ \ \psi\circ u\ \text{measurable}

\varphi:\ 0\mapsto0,\ 1\mapsto1,\ 2\mapsto1

\varphi^{-1}(\{0\})=\{0\},\ \varphi^{-1}(\{1\})=\{1,2\}\in\Sigma_Y:\ \varphi\ \text{measurable}

\varphi\circ f

\varphi\circ f:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto1,\ \ \text{measurable}

\mathbf{1}_E:(X,\Sigma)\to(\{0,1\},\mathcal{P}(\{0,1\}))

\mathbf{1}_E\ \text{measurable}\iff E\in\Sigma

\varphi\circ f=\mathbf{1}_{\{2,3\}},\ k=\mathbf{1}_{\{1,2,3\}}

\mathbf{1}_{\{2,3\}}\ \text{measurable};\ \mathbf{1}_{\{0\}},\ k\ \text{not measurable}

m:\ 0\mapsto0,\ 1\mapsto0,\ 2\mapsto1,\ 3\mapsto1

m\ \text{measurable, yet}\ m(\{2,3\})=\{1\}\notin\Sigma_Y

k:X\to Z,\ \Sigma_Z=\mathcal{P}(Z)

k(A)\in\Sigma_Z\ \text{for every}\ A\in\Sigma_X,\ \text{yet}\ k^{-1}(\{0\})=\{0\}\notin\Sigma_X

\text{S07 to S15}

f,\ \varphi,\ \varphi\circ f,\ m\ \text{measurable};\ g,\ k\ \text{not}

Substeps and lemmas

\Sigma_X=\{\emptyset,\{0,1\},\{2,3\},X\}

\emptyset\in\Sigma_X;\ \emptyset^c=X,\ \{0,1\}^c=\{2,3\};\ \{0,1\}\cup\{2,3\}=X

\Sigma_Y=\{\emptyset,\{0\},\{1,2\},Y\},\ \Sigma_Z=\mathcal{P}(Z)

\Sigma_Y,\ \Sigma_Z\ \text{are}\ \sigma\text{-algebras}

x\in(\psi\circ u)^{-1}(D)

x\in u^{-1}(\psi^{-1}(D))

D\in\mathcal{C}

\psi^{-1}(D)\in\mathcal{B}\ \Rightarrow\ u^{-1}(\psi^{-1}(D))\in\mathcal{A}

\mathbf{1}_E^{-1}(C),\ C\subseteq\{0,1\}

\emptyset\mapsto\emptyset,\ \{1\}\mapsto E,\ \{0\}\mapsto X\setminus E,\ \{0,1\}\mapsto X

\{\emptyset,E,X\setminus E,X\}\subseteq\Sigma

\iff E\in\Sigma

Reverse audits

• S16 · premise_audit · S07, S08, S11, S13 — Only conjoins conclusions already proved; they concern the instances of G1 to G5, while the two lemmas hold for general measurable spaces.
• S15 · premise_audit · image_preimage_def, S13 — Each counterexample refutes one direction of implication.
• S14 · premise_audit · image_preimage_def, S04 — Measurability is decided by preimages; an image outside Σ_Y is irrelevant to it.
• S13 · premise_audit · L_indicator, G1 — Deciding whether E lies in Σ_X needs only a comparison with the four members of Σ_X.
• S12.2 · inverse_equivalence · iff_intro, mko_sigma_def — Both directions have reasons: ⇒ uses one preimage, ⇐ uses closure of the sigma-algebra under complements.
• S12.1 · inverse_equivalence · p_indicator_def, image_preimage_def — All four preimages are determined both ways by the definitions.
• S12 · premise_audit · L_indicator — The target sigma-algebra is the power set; with only {∅,{0,1}} as target every function would be measurable, and the lemma would read differently.
• S11 · premise_audit · L_comp_meas, S07, S10 — Both hypotheses of the lemma have been checked; the direct read-back is an independent cross-check.
• S10 · premise_audit · image_preimage_def, case_analysis — All four members of Σ_Z are enumerated.
• S09.2 · premise_audit · S09.1, forall_elim, forall_intro — Two instantiations; the intermediate set ψ⁻¹(D) must lie in ℬ for the measurability of u to apply.
• S09.1 · inverse_equivalence · image_preimage_def, composition_def, set_extensionality — The whole chain holds both ways; no map needs to be invertible.
• S09 · premise_audit · L_comp_meas — Needs each map to be measurable; nothing is claimed when only one of them is.
• S08 · premise_audit · quantifier_negation, image_preimage_def — Refuting a universal statement needs one counterexample B={0}; g differs from f only at 1, and that is enough to break measurability.
• S07 · premise_audit · S04, S05, S06, case_analysis — This is a complete verification of a finite universal statement, for this f only (MKO assumption a2).
• S06 · inverse_equivalence · image_preimage_def, set_extensionality — Complete enumeration; the two computations agree and check each other.
• S05 · inverse_equivalence · image_preimage_def, set_extensionality — All four points are checked, and the preimage set is determined both ways by the definition.
• S04 · premise_audit · image_preimage_def, function_def — u⁻¹(Y)=X uses that u is total; a partial function would break this step.
• S03 · premise_audit · function_def, G3 — If the table missed a point, preimages could not be computed completely; all 4 points are listed.
• S02.2 · premise_audit · set_operations_def, G2, G4 — A power set is always a sigma-algebra; the check of Σ_Y corresponds item by item to S02.1.
• S02.1 · premise_audit · set_operations_def, G1 — All C(4,2)=6 pairwise unions are covered (N1); a countable union from a finite family equals a finite union.
• S02 · premise_audit · mko_sigma_def — The finite reduction is valid only for finite families; each family here has 4 members.
• S01 · premise_audit · mko_measurable_def — Only unfolds the definition; the direction is preimages, not images (see S14, S15).

Error controls and negative controls

Check preimages, not images

One misconception named by the MKO is to check images instead of preimages. The map m of S14 is measurable although its image m({2,3})={1} is not in Σ_Y; the map k of S15 has all its images in Σ_Z yet is not measurable because k⁻¹({0})={0}∉Σ_X. The direction of measurability is: take preimages of measurable target sets and land in the source sigma-algebra.

Measurable is not measure preserving

MKO assumption a2 warns that measurability does not imply continuity, integrability or measure preservation. For example, take μ_X({0,1})=μ_X({2,3})=1/2 on Σ_X and μ_Y({0})=1/3, μ_Y({1,2})=2/3 on Σ_Y (both given by atom weights with total 1, N3, N4); f is measurable, but μ_X(f⁻¹({0}))=μ_X({0,1})=1/2≠1/3=μ_Y({0}) (N5), so f is not measure preserving.

Check the sigma-algebras before measurability

The definition of measurability presupposes sigma-algebras on both sides (S02). If Σ_X were miswritten as {∅,{0,1},X} (missing {2,3}, the complement of {0,1}), it would not be a sigma-algebra, and the conclusion of S06 that f⁻¹({1,2})={2,3}∈Σ_X would fail; the fault would lie in the family, not in the function.

• m({2,3})={1} is not in Σ_Y, so m is not measurable → reject — Measurability concerns preimages: m⁻¹({0})={0,1} and m⁻¹({1,2})={2,3} are both in Σ_X (S14).
• Every image of k lies in Σ_Z, so k is measurable → reject — k⁻¹({0})={0}∉Σ_X (S15).
• g differs from f at only one point, so g is measurable too → reject — g⁻¹({0})={0}∉Σ_X (S08); measurability is not stable under changing a single point.
• f is measurable, so μ_X(f⁻¹(B))=μ_Y(B) for any measures μ_X, μ_Y → reject — The measures of error control 2 give 1/2≠1/3; measurability does not imply measure preservation.

Result and limitations

f is measurable (f⁻¹({0})={0,1}, f⁻¹({1,2})={2,3}); g is not (g⁻¹({0})={0}∉Σ_X). Composites of measurable maps are measurable, and φ∘f=1_{{2,3}} is measurable; 1_E is measurable ⇔ E∈Σ_X, so 1_{{0}} and k=1_{{1,2,3}} are not. m is measurable although m({2,3})={1}∉Σ_Y, and k has all images in Σ_Z but is not measurable: an image check cannot replace the preimage check.

• The measures μ_X and μ_Y of error control 2 are given by atom weights; that they are measures follows the atom construction of the sigma-algebra and measure-space entry and is not re-proved here.
• Simple functions, integration and convergence of measures (the MKO's formal next) are out of scope.

Verification and source binding

5 declared checks for this guide; only the listed expressions are covered.

• source commit: b28a5edbd46279b1db2a3f3f48bb3f447e18899f
• adopted source SHA-256: b30cc3fb4fd89f6219b80c50db6bfa4bdd2524d76e965a40117637009646bdf0
• original source SHA-256: b30cc3fb4fd89f6219b80c50db6bfa4bdd2524d76e965a40117637009646bdf0
• Lean: NOT_RUN · independent AI: NOT_MEASURED

Same-source full JSON (formulas, ASTs, controls and revision log)