Before any region can have a probability, someone has to say which regions are allowed to have a size at all. This is the answer everyone uses.
Here is the problem, and it genuinely shocked mathematics when it surfaced: not every collection of points can be assigned a size. Insist that every set has a volume and you get contradictions -- most famously, a solid ball that can be cut into five pieces and reassembled into two balls the same size as the original.
The repair is to be selective. Fix a family of well-behaved sets -- start from simple ones like intervals, close under countable combinations -- and only ever measure those. That family is the Borel sets.
The restriction sounds drastic and costs nothing. Every region you could describe, draw, or physically distinguish is Borel. The pathologies need the axiom of choice and cannot be exhibited, only proved to exist. Probability theory lives happily inside the fence.
Every measure in the corpus is a Borel measure -- on the state space, on the unitary group -- and every outcome region whose volume becomes a Born weight is a Borel set. This is not decoration: the programme's central claim is a statement about the measures of regions, and it would be meaningless for regions without measures.
One detail the constructions lean on: the boundaries between outcome regions are null sets. A state sitting exactly on a boundary is ambiguous about which outcome it belongs to -- and the ambiguity has probability zero, so no prediction ever depends on resolving it.
The sigma-algebra generated by the open sets of a topological space. The corpus's measures are Borel probability measures on the projective space and on the unitary group; the outcome regions are Borel with Fubini-Study-null boundaries, and the null- boundary fact is used, not just noted.
Emile Borel (1871-1956) was born at Saint-Affrique in the Aveyron, a pastor's son, and topped the entrance examinations for BOTH the Ecole Normale Superieure and the Ecole Polytechnique -- choosing the Normale, to the Polytechnique's lasting chagrin. He taught at Lille and then in Paris, at the Normale and the Sorbonne, founding measure theory around 1898.
His second life was public: Radical-Socialist deputy in the Chamber, Minister of the Navy in 1925, and at seventy, Resistance activity that earned him a spell in Vichy detention and, after the war, the Resistance Medal. The infinite monkey theorem is his image, from a 1913 paper. Few mathematicians have run a ministry; fewer still after founding a field.
Source links are pinned to a commit, so they do not drift. The anchors above are checked mechanically against the Lean tree on every build. The mathematics is not, and cannot be: that is a human responsibility and it rests with the author.
Part of Constraint-Surface Dynamics · Formalised in csd-lean4.
Google Analytics counts visits to this page, which stores cookies in your browser. They record how the page was reached, not who you are, and nothing is passed on. Blocking cookies for this site breaks nothing here. Details.