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

Orthogonal projection of a point $x \in \mathbb{R}^2$ onto the line through the origin making angle $\theta$ with the $x$-axis: $\pi_\theta(x) = x_0 \cos\theta + x_1 \sin\theta$.

noncomputable def BourgainProjection.coveringNum (δ : NNReal) {α : Type u_1} [PseudoEMetricSpace α] (A : Set α) : ℝ

The $\delta$-covering number $|A|_\delta$ of a set $A$ in a pseudo-extended metric space, returned as a real number (via the external covering number from Mathlib).

noncomputable def BourgainProjection.avgFamilyCovering (f : ℝ → EuclideanSpace ℝ (Fin 2) → ℝ) (δ : NNReal) (X : Set (EuclideanSpace ℝ (Fin 2))) (a b : ℝ) : ℝ

The average $\delta$-covering number of a one-parameter family of projections $f_t : \mathbb{R}^2 \to \mathbb{R}$ applied to $X$, averaged over the parameter $t \in [a,b]$: $\frac{1}{b-a} \int_a^b |f_t(X)|_\delta \, dt$.

noncomputable def BourgainProjection.avgProjectionCovering (δ : NNReal) (X : Set (EuclideanSpace ℝ (Fin 2))) : ℝ

The average $\delta$-covering number of the orthogonal projections of $X \subset \mathbb{R}^2$ over angles $\theta \in [0, \pi]$.

theorem BourgainProjection.projection_averaging_estimate : ∃ C > 0, ∀ X ⊆ Metric.closedBall 0 1, ∀ (δ : NNReal), 0 < ↑δ → avgProjectionCovering δ X ≥ C * coveringNum δ X ^ (1 / 2)

Projection averaging estimate: there is a universal constant $C > 0$ such that for any $X \subset \overline{B}(0,1) \subset \mathbb{R}^2$ and any $\delta > 0$, the average $\delta$-covering number of the orthogonal projections of $X$ over $\theta \in [0,\pi]$ is at least $C \cdot |X|_\delta^{1/2}$.

theorem BourgainProjection.avg_projection_covering_bound (f : ℝ → EuclideanSpace ℝ (Fin 2) → ℝ) (X : ℕ → Set (EuclideanSpace ℝ (Fin 2))) (δ : NNReal) (hδ : 0 < ↑δ) (C₁ : ℝ) (hC₁ : C₁ > 0) (hdecomp : ∀ (j : ℕ), coveringNum δ (X (j + 1)) ≥ C₁ * (↑δ)⁻¹ * avgFamilyCovering f δ (X j) 0 1) (C₂ : ℝ) (hC₂ : C₂ > 0) (havgest : ∀ (j : ℕ), avgFamilyCovering f δ (X j) 0 1 ≥ C₂ * coveringNum δ (X j) ^ (1 / 2)) : ∃ C > 0, ∀ (j : ℕ), coveringNum δ (X (j + 1)) ≥ C * (↑δ)⁻¹ * coveringNum δ (X j) ^ (1 / 2)

Iterative scale growth: if at every scale $j$ the covering number of $X_{j+1}$ dominates $C_1 \delta^{-1}$ times the average family covering of $X_j$, and the average family covering of $X_j$ is at least $C_2 |X_j|_\delta^{1/2}$, then $|X_{j+1}|_\delta \geq (C_1 C_2)\, \delta^{-1}\, |X_j|_\delta^{1/2}$ for every $j$.