Sigma-algebras and measure spaces: an atom-generated sigma-algebra and a probability measure on a four-point carrier

Goal and scope

On X={0,1,2,3}, the 8 sets generated by the atoms A_1={0}, A_2={1,2}, A_3={3} form Σ, and μ(∪_{i∈I}A_i)=Σ_{i∈I}m_i with m_1=1/2, m_2=1/3, m_3=1/6. Prove that Σ is a sigma-algebra (with the finite reduction of countable unions), that μ is a measure (with the finite reduction of countable additivity) and a probability measure; then show that 𝒢={∅,{0},{1},X} is not a sigma-algebra and that ν, which changes a single value, is not a measure.

Treats only the finite measure space specified by G1 to G4 and two counterexamples (MKO assumptions a1, a2). Countable unions and countable additivity are reduced to finite cases only for this finite Σ; nothing is extended to arbitrary infinite sigma-algebras or extended-real-valued measures. The finite/cofinite example in the error controls is only a contrast. The canonical MKO and its English edition are not changed.

Givens and symbols

• set_operations_def
• set_extensionality
• finite_sum_rules
• finite_counting_basics
• nat_induction

• G1 — Carrier X={0,1,2,3}; atoms A_1={0}, A_2={1,2}, A_3={3}.
• G2 — Complete canonical set family Σ={∅,{0},{1,2},{3},{0,1,2},{0,3},{1,2,3},X}, described as Σ={E_I ∣ I⊆{1,2,3}} with E_I=∪_{i∈I}A_i (MKO assumption a1).
• G3 — Exact nonnegative rational weights m_1=1/2, m_2=1/3, m_3=1/6; define μ(E_I)=Σ_{i∈I}m_i.
• G4 — Counterexamples: 𝒢={∅,{0},{1},X}; ν is defined on Σ and equals μ everywhere except ν({0,1,2})=1.

• X=\{0,1,2,3\} — the finite carrier
• A_1,A_2,A_3 — the atoms {0}, {1,2}, {3}
• E_I=\bigcup_{i\in I}A_i — the union of atoms indexed by I⊆{1,2,3}
• \Sigma — the 8 sets of G2
• \mu,\ m_i — the measure and atom weights 1/2, 1/3, 1/6
• \mathcal{G},\ \nu — counterexamples: a family that is not a sigma-algebra and a set function that is not a measure

Rules and sources

• 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.
• set_extensionality · prerequisite — Set equality: A=B if and only if A⊆B and B⊆A, i.e. they have the same elements.
• finite_sum_rules · prerequisite — Finite sums: Σ_{i=1}^{0} a_i=0 and Σ_{i=1}^{n+1} a_i=Σ_{i=1}^{n} a_i + a_{n+1}; Σ(a_i+b_i)=Σa_i+Σb_i; Σ c·a_i=c·Σa_i.
• finite_counting_basics · prerequisite — Finite counting: for disjoint finite sets A, B, |A∪B|=|A|+|B|; |A×B|=|A|·|B|; there is a bijection between finite sets ⇔ they have the same number of elements.
• nat_induction · prerequisite — Principle of induction: for a family P(n) starting at n₀, if P(n₀) holds and P(n)⇒P(n+1) for every n≥n₀, then P(n) holds for every n≥n₀.
• 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.
• contradiction · prerequisite — Proof by contradiction: if assuming ¬P leads to a contradiction (a statement and its negation both hold), then P holds.
• numeric_evaluation · prerequisite — Exact evaluation of an explicit integer or rational expression; independently recomputable.
• subset_def · prerequisite — Subset: A⊆B means every element of A is an element of B, i.e. ∀x (x∈A⇒x∈B).
• and_intro_elim · prerequisite — Conjunction: from P and Q infer P∧Q; from P∧Q infer P and infer Q.
• def_intro · prerequisite — Introducing a definition: a statement, expression or object may be given a name, after which the name and what it stands for are interchangeable.
• order_basics · prerequisite — Order of the reals: exactly one of u<v, u=v, u>v holds; u<v and v<w give u<w; u<v gives u+w<v+w; u<v and w>0 give uw<vw; u<v and w<0 give uw>vw.
• injective_surjective_def · prerequisite — Injective: f(a)=f(a′) ⇒ a=a′. Surjective: every b∈B has some a∈A with f(a)=b. Bijective: both; then there is a unique inverse f⁻¹ with f⁻¹∘f=id_A and f∘f⁻¹=id_B.
• quantifier_negation · prerequisite — Negating quantifiers: ¬(∀x, P(x)) is equivalent to ∃x, ¬P(x), and ¬(∃x, P(x)) is equivalent to ∀x, ¬P(x).
• mko_sigma_def · cited — On a set X, a sigma-algebra contains the empty set and is closed under complements and countable unions. A measure assigns nonnegative values to measurable sets, is zero on the empty set and is countably additive on pairwise disjoint countable families. A complete finite carrier permits reduction to finitely many distinct sets. · mko-sigma-algebra-measure-space
• L_rep_unique · lemma — For the atoms of G1, if E_I=E_J then I=J.
• L_complement · lemma — For every I⊆{1,2,3}: X∖E_I=E_{I'}, where I'={1,2,3}∖I.
• L_union · lemma — For all I, J⊆{1,2,3}: E_I∪E_J=E_{I∪J}.
• L_countable_reduce · lemma — For every sequence (E_k)_{k≥1} in Σ, the set D={E_k ∣ k≥1} is a finite subfamily of Σ, ∪_k E_k=∪_{E∈D}E, and this union belongs to Σ.
• L_fin_add · lemma — For E, F∈Σ with E∩F=∅: μ(E∪F)=μ(E)+μ(F).
• L_ctbl_add · lemma — For a pairwise disjoint sequence (E_k)_{k≥1} in Σ: the series Σ_k μ(E_k) converges and μ(∪_k E_k)=Σ_k μ(E_k).
• p_finite_support_series · prerequisite — If all but finitely many terms of a real series are 0, the series converges and its sum is the (finite) sum of the nonzero terms.

Main derivation

(X,\Sigma,\mu)\ \text{is a measure space}

\emptyset\in\Sigma;\ E\in\Sigma\Rightarrow X\setminus E\in\Sigma;\ E_k\in\Sigma\Rightarrow\bigcup_{k\ge1}E_k\in\Sigma;\ \mu\ge0,\ \mu(\emptyset)=0,\ \mu\Big(\bigcup_k E_k\Big)=\sum_k\mu(E_k)\ \text{(pairwise disjoint)}

A_1=\{0\},\ A_2=\{1,2\},\ A_3=\{3\}

A_i\neq\emptyset,\ \ A_i\cap A_j=\emptyset\ (i\neq j),\ \ A_1\cup A_2\cup A_3=X

\Sigma=\{E_I\mid I\subseteq\{1,2,3\}\}

|\Sigma|=8:\ \emptyset,\{0\},\{1,2\},\{3\},\{0,1,2\},\{0,3\},\{1,2,3\},X

I=\emptyset

E_{\emptyset}=\emptyset\in\Sigma

E_I\in\Sigma

X\setminus E_I=E_{I'}\in\Sigma,\ \ I'=\{1,2,3\}\setminus I

E_I,\ E_J\in\Sigma

E_I\cup E_J=E_{I\cup J}\in\Sigma

(E_k)_{k\ge1},\ E_k\in\Sigma

\bigcup_{k\ge1}E_k=\bigcup_{E\in D}E\in\Sigma,\ \ D=\{E_k\mid k\ge1\}

\emptyset\in\Sigma,\ \text{complements},\ \text{countable unions}

\Sigma\ \text{is a}\ \sigma\text{-algebra on}\ X

\mu(E_I)=\sum_{i\in I}m_i

\mu:\ 0,\tfrac12,\tfrac13,\tfrac16,\tfrac56,\tfrac23,\tfrac12,1\ \text{on}\ \emptyset,\{0\},\{1,2\},\{3\},\{0,1,2\},\{0,3\},\{1,2,3\},X

m_i\ge 0

\mu(E)\ge 0\ \ (E\in\Sigma),\quad \mu(\emptyset)=\sum_{i\in\emptyset}m_i=0

E,F\in\Sigma,\ E\cap F=\emptyset

\mu(E\cup F)=\mu(E)+\mu(F)

(E_k)_{k\ge1}\subseteq\Sigma\ \text{pairwise disjoint}

\mu\Big(\bigcup_{k\ge1}E_k\Big)=\sum_{k\ge1}\mu(E_k)

\mu(X)=\tfrac12+\tfrac13+\tfrac16

\mu(X)=1:\ (X,\Sigma,\mu)\ \text{is a probability space}

\mathcal{G}=\{\emptyset,\{0\},\{1\},X\}

X\setminus\{0\}=\{1,2,3\}\notin\mathcal{G}:\ \mathcal{G}\ \text{is not a}\ \sigma\text{-algebra}

\nu=\mu\ \text{except}\ \nu(\{0,1,2\})=1

\nu(\{0\}\cup\{1,2\})=1\neq\tfrac56=\nu(\{0\})+\nu(\{1,2\})

Substeps and lemmas

E_I=E_J

I=J

I\mapsto E_I\ \text{injective on}\ \mathcal{P}(\{1,2,3\})

|\Sigma|=2^3=8

x\in X\setminus E_I

x\in E_{I'}

x\in E_{I'}

x\in X\setminus E_I,\ \text{hence}\ X\setminus E_I=E_{I'}

x\in E_I\cup E_J

x\in E_{I\cup J}

D=\{E_k\mid k\ge1\}

D\subseteq\Sigma,\ \ |D|\le 8

x\in\bigcup_{k\ge1}E_k

x\in\bigcup_{E\in D}E

D\subseteq\Sigma\ \text{finite}

\bigcup_{E\in D}E\in\Sigma

E=E_I,\ F=E_J,\ E\cap F=\emptyset

I\cap J=\emptyset

I\cap J=\emptyset

\mu(E_I\cup E_J)=\mu(E_{I\cup J})=\sum_{i\in I\cup J}m_i=\sum_{i\in I}m_i+\sum_{j\in J}m_j

K=\{k\mid E_k\neq\emptyset\},\ E_k=E_{I_k}

I_k\neq\emptyset,\ I_k\cap I_l=\emptyset\ (k\neq l\in K),\ \ |K|\le 3

\sum_{k\ge1}\mu(E_k)

\sum_{k\in K}\mu(E_k)

\bigcup_{k\ge1}E_k

\mu\Big(\bigcup_{k\in K}E_k\Big)=\sum_{k\in K}\mu(E_k)

Reverse audits

• S15 · premise_audit · G4, numeric_evaluation — One failing pair of disjoint sets refutes additivity; a pair is a special case of a countable family (pad with ∅).
• S14 · premise_audit · G4, set_operations_def — Refuting a universal closure property needs one counterexample; two are given here.
• S13 · premise_audit · S08, S10, S12, numeric_evaluation — The measure-space conclusion needs every obligation; a probability measure also needs μ(X)=1, which is an exact rational computation, not an approximation.
• S12.3 · premise_audit · S11, S06, set_extensionality — The previous union is disjoint from the new member because the new member is disjoint from each earlier member; S11 is only ever applied to two sets.
• S12.2 · premise_audit · S12.1, S10, p_finite_support_series — Convergence comes from having only finitely many nonzero terms, not from general series theory.
• S12.1 · premise_audit · S11.1, finite_counting_basics — This injects K into {1,2,3} (each k picks one index from I_k); an injection into a 3-element set gives |K|≤3.
• S12 · premise_audit · L_ctbl_add, S11 — The reduction here uses the three-atom bound and hence finiteness of Σ, not finiteness of every atom or of the carrier itself. It also works on an infinite carrier with a finite atom partition and its union family. Error control 2 only shows that finite additivity on arbitrary infinite event families need not imply countable additivity.
• S11.2 · premise_audit · S11.1, S06, finite_sum_rules — Splitting the sum needs disjoint index sets; with overlap the shared weights would be counted twice.
• S11.1 · premise_audit · S02, set_operations_def — Uses that atoms are nonempty; the converse (I∩J=∅ implies E∩F=∅) also holds but is not needed here.
• S11 · premise_audit · L_fin_add — The condition E∩F=∅ cannot be dropped: {0,1,2} and {0,3} intersect, and 5/6+2/3 exceeds μ({0,1,2,3})=1.
• S10 · premise_audit · finite_sum_rules, order_basics — Requires every weight m_i≥0; with a negative weight, nonnegativity could fail.
• S09 · premise_audit · L_rep_unique, G3, numeric_evaluation — Unique representation guarantees well-definedness for this construction; in general it is enough that different representations give the same value. The 8 values can be recomputed independently through N2 to N5.
• S08 · premise_audit · S04, S05, S07 — None of the three obligations may be omitted; containing ∅ and X is not enough (S14).
• S07.3 · premise_audit · S04, S06, nat_induction — The induction runs only over finite |D|; it does not prove closure under arbitrary infinite unions, a step replaced by the finiteness of S07.1.
• S07.2 · inverse_equivalence · set_extensionality, set_operations_def — ⇒: if x∈E_k take E=E_k∈D; ⇐: E∈D means E=E_k for some k. Both directions hold.
• S07.1 · premise_audit · S03, subset_def — A subset of a finite set is finite; no claim is made that the sequence itself is finite.
• S07 · premise_audit · L_countable_reduce, S06 — The key premise is that Σ is finite (S03); in an infinite sigma-algebra a countable union cannot be reduced to a finite union this way.
• S06.1 · inverse_equivalence · set_operations_def, set_extensionality — Each link is a two-way rewriting of a definition, so the whole chain holds both ways; this step does not need the atoms to be disjoint.
• S06 · premise_audit · L_union, S03 — Closure under binary unions is a necessary part of closure under countable unions but is not enough on its own; S07 handles the countable case.
• S05.2 · premise_audit · S02, S05.1, set_extensionality — Uses that every point lies in at most one atom (pairwise disjoint); only the two inclusions together give equality.
• S05.1 · premise_audit · S02, set_operations_def — Uses that every point lies in at least one atom (the union is X).
• S05 · premise_audit · L_complement, S03 — Depends on the atoms forming a partition (S02); for an arbitrary family, complements need not stay in the family (see S14).
• S04 · premise_audit · S03, def_unfold — Uses only the definition of the empty union.
• S03.2 · premise_audit · S03.1, finite_counting_basics — Injectivity together with the explicit listing gives |Σ|=8 and agreement with the list.
• S03.1 · premise_audit · S02, contradiction, set_operations_def — Nonemptiness supplies the point a and disjointness pins j down to i; neither condition can be dropped.
• S03 · premise_audit · S02, L_rep_unique, G2 — Injectivity depends on the atoms being nonempty and pairwise disjoint (S02); with overlapping atoms one set could have two index sets.
• S02 · premise_audit · G1, set_operations_def — Three pairwise intersections and one union form a complete finite check; nonemptiness is needed in S03.1 and S12.1.
• S01 · premise_audit · mko_sigma_def — Only unfolds the definition and produces no new fact; this list is the set of obligations to be discharged item by item.

Error controls and negative controls

Containing ∅ and the whole set is not enough

One misconception named by the MKO is to call a family a sigma-algebra just because it contains ∅ and the whole set. A sigma-algebra must also be closed under complements and countable unions. The family 𝒢 of S14 contains ∅ and X but lacks the complement {1,2,3} of {0} and lacks {0}∪{1}. (The family {∅,X} itself is a sigma-algebra, but that is because it passes every closure check, not because it contains ∅ and X.)

Finite additivity does not extend unconditionally

The reductions of S07 and S12 use that Σ is finite with only 3 atoms. An infinite carrier alone does not prevent this reduction: the four-event sigma-algebra generated by the even and odd integers still permits it. The reduction cannot instead be assumed for an arbitrary infinite event family: on the family of finite or cofinite subsets of ℕ define λ(A)=0 for finite A and λ(A)=1 for cofinite A. Two disjoint sets cannot both be cofinite (the intersection of two cofinite sets is cofinite, hence nonempty), from which finite additivity of λ can be checked; but ℕ is the countable disjoint union of the singletons {n}, and λ(ℕ)=1 while Σλ({n})=0, so countable additivity fails. That family is not a sigma-algebra either (the set of even numbers is a countable union of singletons but is neither finite nor cofinite).

Unique representation makes this construction well defined

Since μ is defined through index sets, different representations must assign the same value. Overlap alone need not destroy unique representation. For a concrete failure, take B₁={0,1}, B₂={1,2}, B₃={0,1,2}, each with weight 1. Then B₁∪B₂=B₃, but index sets {1,2} and {3} assign totals 2 and 1. That rule is not well defined. Lemma L_rep_unique in S03.1 uses the given atoms' nonemptiness and pairwise disjointness to prove unique representation, which is sufficient for the construction in S09.

• Every family containing ∅ and X is a sigma-algebra → reject — 𝒢={∅,{0},{1},X} contains both, but the complement {1,2,3} of {0} is not in 𝒢 (S14).
• ν is nonnegative with ν(∅)=0, so ν is a measure → reject — {0} and {1,2} are disjoint, but ν({0,1,2})=1≠5/6=ν({0})+ν({1,2}) (S15).
• Since finite additivity gives countable additivity for μ on this finite Σ, every finitely additive set function on any carrier is countably additive → reject — The 0-1 valued λ on the finite/cofinite family of ℕ is finitely additive, but λ(ℕ)=1≠0=Σλ({n}) (error control 2).
• μ is a probability measure on the power set of X, so μ({1}) is defined → reject — μ is defined only on Σ; {1} is not a union of atoms (it contains only part of A_2), so it is not in Σ, and Σ is not the power set.

Result and limitations

Σ={E_I ∣ I⊆{1,2,3}} has exactly 8 sets, contains ∅, is closed under complements (X∖E_I=E_{I'}) and under countable unions (reduced to a finite union of at most 8 distinct sets), so it is a sigma-algebra; μ(E_I)=Σ_{i∈I}m_i is well defined, nonnegative, μ(∅)=0 and countably additive (a disjoint sequence has at most 3 nonempty members), with μ(X)=1, so (X,Σ,μ) is a probability space. 𝒢={∅,{0},{1},X} is not a sigma-algebra and ν is not a measure.

• The finite/cofinite example in error control 2 is argued in prose and not broken into numbered steps; the conclusions of this guide do not depend on it.
• This guide does not prove that every sigma-algebra on a finite set is generated by the atoms of some partition; the Σ here is constructed directly from given atoms.
• Measurable functions, the Lebesgue integral and convergence theorems (the MKO's formal next) are out of scope.

Verification and source binding

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

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

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