noncomputable def BourgainProjection.deltaCoveringNumberR (δ : ℝ) (X : Set ℝ) : ℕ∞

One-dimensional $\delta$-covering number of $X \subseteq \mathbb{R}$.

def BourgainProjection.IsDeltaSRegular1D (δ s C : ℝ) (D : Set ℝ) : Prop

IsDeltaSRegular1D δ s C D says that $D \subseteq [0,1]$ is a $(\delta, s, C)$-set on the line: for every interval $B(x, r)$ with $\delta \leq r \leq 1$, $|D \cap B(x,r)|_\delta \leq C r^s |D|_\delta$.

noncomputable def BourgainProjection.directionVector (θ : ℝ) : EuclideanSpace ℝ (Fin 2)

The unit direction vector $(\cos\theta, \sin\theta) \in \mathbb{R}^2$ associated to the angle $\theta$.

noncomputable def BourgainProjection.orthProjLine (θ : ℝ) : EuclideanSpace ℝ (Fin 2) →L[ℝ] ℝ

Orthogonal projection onto the line through the origin in direction $\theta$, viewed as a continuous linear map $\mathbb{R}^2 \to \mathbb{R}$.

theorem BourgainProjection.bourgain_projection_restated (t : ℝ) (ht0 : 0 < t) (ht2 : t < 2) (s : ℝ) (hs0 : 0 < s) (hs1 : s ≤ 1) : ∃ (ε : ℝ) (η : ℝ), 0 < ε ∧ 0 < η ∧ ∀ (δ : ℝ), 0 < δ → δ < 1 → ∀ (X : Set (EuclideanSpace ℝ (Fin 2))), DeltaRegular.IsDeltaSRegular δ t (δ ^ (-η)) X → ↑(DeltaRegular.deltaCoveringNumber δ X) = ENNReal.ofReal (δ ^ (-t)) → ∀ (D : Set ℝ), IsDeltaSRegular1D δ s (δ ^ (-η)) D → ∃ θ ∈ D, ∀ X' ⊆ X, ↑(DeltaRegular.deltaCoveringNumber δ X') ≥ ENNReal.ofReal (δ ^ η) * ↑(DeltaRegular.deltaCoveringNumber δ X) → ↑(deltaCoveringNumberR δ (⇑(orthProjLine θ) '' X')) ≥ ENNReal.ofReal (δ ^ (-t / 2 - ε))

Bourgain's projection theorem, restated ($\delta$-discretized form): for any $t \in (0,2)$ and $s \in (0,1]$ there exist $\varepsilon, \eta > 0$ such that for every $\delta \in (0,1)$, every $(\delta, t, \delta^{-\eta})$-regular set $X \subset \mathbb{R}^2$ with covering number $|X|_\delta = \delta^{-t}$, and every $(\delta, s, \delta^{-\eta})$-regular set $D \subseteq [0,1]$ of directions, there exists a direction $\theta \in D$ such that for every robust subset $X' \subseteq X$ with $|X'|_\delta \geq \delta^\eta |X|_\delta$, $|\pi_\theta(X')|_\delta \geq \delta^{-t/2 - \varepsilon}$.