While this submission is a draft, it cannot be used by other submissions.

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.

Read the Lean proof on GitLab

Description

Since š“›Ļ‰š“›_ω has rank one and š“›Ļ‰e0=±e0š“›_ω eā‚€ = ±eā‚€, ā€–š“›Ļ‰(n)x‖=āˆ£Ļ†Ļ‰(x)āˆ£ā€–š“›^{(n)}_ω x‖ = |φ_ω(x)| for n≄1n ≄ 1, so Ī»1=0λ₁ = 0, Ī»2=āˆ’āˆžĪ»ā‚‚ = -āˆž, and the slow space is kerφωker φ_ω. By density of Z√2ā„¤āˆš2 in the circle the sign patterns (si(ω))i(sįµ¢(ω))įµ¢ separate points, and kernels of distinct functionals φω≠±φω′φ_ω ≠ ±φ_{ω'} are at distance at least 11 in š’¢Xš’¢X. A measurable choice of slow spaces would therefore make every subset of [0,1/2)[0, 1/2) measurable, but the Borel σσ-algebra of the circle has only š” š”  members.