Borel selector reduction
OpenStickyKakeya4.borel_selector_reductionEvery compact Sticky Kakeya datum contains a Borel subset selecting exactly one marked line in every unit direction. Its unmarked carrier still has packing dimension , and its unit front is contained in the original front.
The output is measurable, not asserted compact; all downstream selector statements therefore use a Borel hypothesis.
import Definitions.Def_sticky_kakeya4_core open MeasureTheory Set
namespace StickyKakeya4
theorem borel_selector_reduction (lines : Set MarkedLine)
(hsticky : IsStickyDatum lines) :
∃ selector : Set MarkedLine,
MeasurableSet selector ∧
selector ⊆ lines ∧
IsDirectionSelector selector ∧
packingDim (lineCarrier selector) = 3 ∧
unitFront selector ⊆ unitFront lines := by sorry
end StickyKakeya4Read-back
What the Lean code literally says, in plain math · gpt-5
For every set of marked lines , where and , assume that is compact; every satisfies and (with no condition on ); every unit vector is the direction of at least one member of ; and the custom packing dimension of the unmarked carrier equals . Here, for a set in a pseudometric space, this custom packing dimension is the infimum over such that there are arbitrary sets indexed by with and custom upper Minkowski dimension at most for every ; the custom upper Minkowski dimension of is the infimum over finite for which there exists a finite , possibly , such that, for all sufficiently small positive , , where is the real value of , exponentiation is extended-nonnegative-real exponentiation, and is the infimum of the extended-nonnegative-real cardinalities of finite, possibly empty, sets of centers whose open radius- balls cover . Then there exists a measurable set of marked lines such that ; for every unit vector , there exists exactly one marked line satisfying both and ; the same custom packing dimension of the unmarked carrier equals ; and