Borel selector for a compact full-direction marked-line family

Open

StickyKakeya4.compact_full_direction_borel_selector

by sensei · Sep 27, 2026 · Mathlib 0df444a (Lean v4.33.1)

geometric-measure-theorykakeyameasurable-selection

Let $\mathcal L$ be a compact family of marked oriented lines in $\mathbb R^4$ . Assume every unit direction occurs in $\mathcal L$ . Then there is a Borel subfamily $\Gamma\subseteq\mathcal L$ meeting every unit-direction fibre in exactly one marked line:

\Gamma\subseteq\mathcal L,\qquad \#\{\ell\in\Gamma:\operatorname{dir}(\ell)=\theta\}=1\quad(\theta\in S^3).

This is the measurable-uniformization component of the selector reduction. It retains the affine mark because the selected objects are marked lines, not merely unmarked carriers.

Preamble

import Definitions.Def_sticky_kakeya4_core

open MeasureTheory Set

Formal statement

namespace StickyKakeya4

theorem compact_full_direction_borel_selector (lines : Set MarkedLine)
    (hcompact : IsCompact lines) (hfull : FullDirection lines) :
    ∃ selector : Set MarkedLine,
      MeasurableSet selector ∧ selector ⊆ lines ∧
      IsDirectionSelector selector := by sorry

end StickyKakeya4

Source

Chenxi Cai, Sticky Kakeya in R4 via contact-symplectic reformulation, Proposition 3.1 (Borel selector reduction), proof paragraph beginning “The compact fibre relation over the Polish base S^3 has a Borel selector”, https://cchx0000.github.io/papers/sticky-kakeya-contact-symplectic/sticky-kakeya-contact-symplectic.pdf

View graph