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/Statements.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

Horan's example (Horan 2020). Distinct kernels VωV_ω are at distance at least 11 in 𝒢X𝒢X, and Vω=Vω′V_ω = V_{ω'} only for ω′=±ωω' = ±ω, so a measurable WW would make every set S=−SS = -S measurable. The product σσ-algebra is generated by countably many cylinders and so has at most 𝔠𝔠 members, while the symmetric sets number 2𝔠2^𝔠.