Fubini-Study measure

The space of quantum states allows exactly one way of measuring size that respects its symmetry, and that one measure is what turns regions of the space into Born-rule probabilities.

proved in corpus · proved here, no imported axiomsLean fsMeasure_unique
Portrait photograph of Guido Fubini
Guido Fubini, one of the two names on the measure.public domain, via Wikimedia Commons

In plain terms

In quantum mechanics the complete description of a system at one moment is called its state, and the collection of all possible states forms a curved space, rather as every place on Earth is a point on a globe. CSD says the probability of an outcome is the fraction of that space occupied by the states that lead to it, so you need a way of saying how big a region is before a fraction means anything. That way is called a measure, a rule that assigns a size to every region. If you chose the rule carelessly you could make any region as large or as small as you liked, which would amount to writing the answer into the question.

Symmetry is what rescues the idea. The space of states has a family of rearrangements, the unitary transformations, which are the quantum counterpart of rigid motions, and they carry any state to any other state while preserving the overlap between every pair of states. The overlap is the number that fixes how likely one state is to be found when the other was prepared. A measure is called invariant when these rearrangements leave the size of every region unchanged, so no direction in the space is secretly favoured, and that's the natural sense in which a measure can be fair.

The Fubini-Study measure is the fair one, and it's the only one. Once you give the whole space size one, exactly one invariant measure exists on the space of states, and that uniqueness is a theorem rather than a convention. Nobody chose the sizes it reports, as the geometry of the space fixes them on its own.

In CSD

CSD doesn't assume the Born rule. It calculates the probability of each outcome as a ratio of volumes, the size of the region of states that leads to the outcome divided by the size of the whole space, and a ratio of volumes means nothing until the measure is fixed. This is the measure, and the whole point of the derivation is that the geometry forces it rather than the theorist picking it.

The geometry forces it because any state can be carried to any other by a unitary transformation, so the space of states is as symmetric as a space can be. A space with that much symmetry admits exactly one invariant probability measure, by the same argument that gives a unique fair measure on the surface of a sphere, so the measure falls out of the geometry instead of going in as an assumption.

This answers the oldest objection to arguments from typicality, which is that they presuppose the very measure they claim to justify. Here the measure comes from symmetry with a uniqueness proof behind it. Helland reaches the same conclusion from the theory of group representations and CSD reaches it from geometry, and two independent routes to the same answer are worth more than either alone.

Mathematically

CP^(N-1) is the compact homogeneous space U(N)/(U(1) x U(N-1)), and the Fubini-Study measure is the unique U(N)-invariant Borel probability measure on it. As standard mathematics it's equivalently the normalised Riemannian volume of the Fubini-Study metric, or the top power of the Kahler form over n factorial, and all three readings are corpus theorems identifying the same measure. The top power of the Fubini-Study form is (4 pi)^n times the measure (fsVolume_eq_smul_fsMeasure), the Riemannian volume of the Fubini-Study metric is that top power over n factorial (riemannianVolume_fsMetric), so the measure is the normalised Riemannian volume (riemannianVolume_fsMetric_eq_smul_fsMeasure). The invariance characterisation is the one that carries the weight in the Born derivation, and the other two are corpus results rather than background. See the Kahler form entry.

The proof is Haar uniqueness carried downstairs. The unitary group is compact, so it has a unique invariant probability measure, and the state space is a quotient of the group, so pushing the measure forward along the orbit map carries the uniqueness with it. It's proved at general N with no imported axioms.

The construction takes a reference point, but that's bookkeeping rather than freedom, as fsMeasure_basepoint_independent shows that every choice gives the same measure. So defaultFsMeasure is the measure and not one member of a family.

The name

Guido Fubini (1879-1943) was born in Venice and trained at the Scuola Normale Superiore in Pisa. He held chairs at Catania, Genoa and, from 1908, the Politecnico di Torino. Most people meet him through his theorem on exchanging the order of integration, and the metric that bears his name came out of his work on projective differential geometry. Italy's racial laws stripped him of his post in 1938, so he emigrated the following year and taught at Princeton and NYU until his death.

Eduard Study (1862-1930) was German. He trained at Jena, Strasbourg, Leipzig and Munich, and held the chair at Bonn from 1904. He worked on invariant theory and complex geometry, and he had a reputation for abrasive independence that kept him at arm's length from the Gottingen establishment. The two men found the metric independently, within about a year of each other around 1904 to 1905, and neither knew of the other's work, which is why it carries both names.

Related entries

Module
CsdLean4/Mathlib/LinearAlgebra/Projectivization/FubiniStudyUnique.lean
Paper
TN1, the Fubini-Study measure as a U(N)-equivariant pushforward
Paper
Paper B, the symmetry argument that fixes the measure
On the site
Paper B derives the Born rule from this measure
New to this?
explainquantum is a beginners' course in quantum mechanics, which starts from scratch and needs no maths
Background
Bengtsson and Zyczkowski, Geometry of Quantum States, 2nd ed., CUP 2020
Referenced
Helland 2024, APL Quantum, Wikipedia

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.

Privacy policy