@[reducible, inline]

abbrev ContinuumBeck.E2 : Type

Shorthand for the Euclidean plane ℝ².

def ContinuumBeck.IsInRhoOneRectangle (center dir : E2) (ρ : ℝ) (x : E2) : Prop

Predicate that x lies in the ρ × 1 rectangle centered at center, oriented along the unit vector dir: the projection of x − center onto dir has absolute value at most ρ/2, and the projection onto the perpendicular direction has absolute value at most 1/2.

def ContinuumBeck.RhoOneRectangle (center dir : E2) (ρ : ℝ) : Set E2

The ρ × 1 rectangle in ℝ² centered at center, oriented along dir.

def ContinuumBeck.RectangleCondition (δ η C : ℝ) (E : Set E2) : Prop

The thin-rectangle hypothesis appearing in the Continuum Beck theorem: for every ρ × 1 rectangle R (any orientation), |E ∩ R|_δ ≤ C ρ^η |E|_δ.

def ContinuumBeck.directionsFromSet (x : E2) (E : Set E2) : Set E2

The set of unit-vector directions (y − x)/‖y − x‖ for y ∈ E \ {x}. This encodes the directions of lines through x that pass through another point of E, as used in Beck's theorem.

theorem ContinuumBeck.continuum_beck_theorem (δ u C η : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) (hu : 0 < u) (hC : 0 < C) (hη : 0 < η) (E : Set E2) (hE : DeltaRegular.IsDeltaSRegular δ u C E) (hRect : RectangleCondition δ η C E) (ε : ℝ) (hε : 0 < ε) : ∃ (c : ℝ), 0 < c ∧ ∃ E' ⊆ E, ↑(DeltaRegular.deltaCoveringNumber δ E') ≥ ENNReal.ofReal (1 / 2) * ↑(DeltaRegular.deltaCoveringNumber δ E) ∧ ∀ x ∈ E', ↑(DeltaRegular.deltaCoveringNumber δ (directionsFromSet x E)) ≥ ENNReal.ofReal (c * δ ^ ε * min (δ ^ (-u)) (δ ^ (-1)))

Continuum Beck theorem (Orponen–Shmerkin–Wang, 2023). If E ⊆ ℝ² is a (δ, u, C)-set satisfying the thin-rectangle condition (i.e. |E ∩ R|_δ ≤ C ρ^η |E|_δ for every ρ × 1 rectangle R), then for most x ∈ E the set of directions Lₓ,E = directionsFromSet x E satisfies |Lₓ,E|_δ ≳ δ^ε · min(δ^{-u}, δ^{-1}). The "most" is formalized as a subset E' ⊆ E containing at least half of the δ-mass of E.