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

Projection of $v \in \mathbb{R}^2$ onto the line with affine parameter $\theta$: $\pi_\theta(v) = v_0 + \theta v_1$.

noncomputable def BourgainProjection.coveringNumber1 (S : Set ℝ) : ℕ∞

The $1$-scale covering number of a subset $S \subseteq \mathbb{R}$.

theorem BourgainProjection.bourgain_projection (t s : ℝ) (ht : 0 < t) (ht2 : t < 2) (hs : 0 < s) (hs1 : s ≤ 1) : ∃ ε > 0, ∃ η > 0, ∀ (R : ℝ), 1 ≤ R → ∀ (X : Finset (EuclideanSpace ℝ (Fin 2))) (D : Finset ℝ), ↑X.card = R ^ t → ↑D.card = R ^ s → (∀ (x : EuclideanSpace ℝ (Fin 2)), ∀ r ≤ R, ↑{p ∈ X | dist p x ≤ r}.card ≤ R ^ η * (r / R) ^ t * ↑X.card) → (∀ (θ₀ ρ : ℝ), ρ ≤ 1 → ↑{d ∈ D | |d - θ₀| ≤ ρ}.card ≤ R ^ η * ρ ^ s * ↑D.card) → ∃ θ ∈ D, ∀ Y ⊆ X, ↑Y.card ≥ R ^ (-1 * η) * ↑X.card → ↑(coveringNumber1 (projLine θ '' ↑Y)) ≥ ENNReal.ofReal (R ^ (t / 2 + ε))

Bourgain's projection theorem (real case): for any $t \in (0,2)$ and $s \in (0,1]$ there exist $\varepsilon, \eta > 0$ such that for every $R \geq 1$ and every pair $(X, D)$ with $|X| = R^t$, $|D| = R^s$, both Frostman-regular with exponents $t$ and $s$ up to an $R^\eta$ loss, there exists a direction $\theta \in D$ for which every robust subset $Y \subseteq X$ (i.e.\ $|Y| \geq R^{-\eta} |X|$) satisfies $|\pi_\theta(Y)|_1 \geq R^{t/2 + \varepsilon}$.