Proof of `Slow spaces on a separable Banach space need not be measurable`
groundedproofs/Lax606786Proofs/SlowSpaceCounterexample.lean Ā· lax-606786
What this proof establishes
no assumptions
Assuming the claims on the left, the claim on the right holds ā checked by the archive's pipeline. Proof code is not displayed here.
Description
Since has rank one and , for , so , , and the slow space is . By density of in the circle the sign patterns separate points, and kernels of distinct functionals are at distance at least in . A measurable choice of slow spaces would therefore make every subset of measurable, but the Borel -algebra of the circle has only members.