noncomputable def ProjectionTheory.DeltaTube.richness (T : DeltaTube) (E : Finset (EuclideanSpace ℝ (Fin 2))) : ℕ

The richness of a δ-tube T with respect to a point set E is the number of points of E contained in T.

def ProjectionTheory.DeltaTube.EssentiallyDistinct (T₁ T₂ : DeltaTube) (δ : ℝ) : Prop

Two δ-tubes are essentially distinct at scale δ if either their midpoints are more than δ apart, or their directions differ by more than δ.

def ProjectionTheory.IsWellSpaced (E : Finset (EuclideanSpace ℝ (Fin 2))) (C₀ : ℝ) : Prop

A finite point set E ⊆ ℝ² is well-spaced with constant C₀ if every ball of radius |E|^(-1/2) contains at most C₀ points of E, i.e. $|E \cap B_{|E|^{-1/2}}| \lesssim 1$.

theorem ProjectionTheory.gsw_basic_fourier_bound : ∃ C₀ > 0, ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → ∀ R > 0, R ≤ ↑E.card → ∀ (𝒯 : Finset DeltaTube), (∀ T ∈ 𝒯, T.width = δ) → (∀ T ∈ 𝒯, ↑(T.richness E) ≥ R) → (∀ T₁ ∈ 𝒯, ∀ T₂ ∈ 𝒯, T₁ ≠ T₂ → T₁.EssentiallyDistinct T₂ δ) → ↑𝒯.card ≤ C₀ * δ⁻¹ * ↑E.card / R ^ 2

GSW Fourier bound (first ingredient). There is a universal constant C₀ > 0 such that for any δ-separated set E of points in the unit ball and any collection 𝒯 of essentially distinct δ-tubes of width δ, each of which is R-rich for E, one has $|\mathcal T| \le C_0 \, \delta^{-1} |E| / R^2$.

theorem ProjectionTheory.gsw_two_ends_bound : ∃ C₁ > 0, ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → ∀ R > 0, R ≤ ↑E.card → ∀ (Rtilde : ℝ), δ ≤ Rtilde → Rtilde ≤ 1 → ∀ (𝒯_sub : Finset DeltaTube), (∀ T ∈ 𝒯_sub, T.width = δ) → (∀ T ∈ 𝒯_sub, ↑(T.richness E) ≥ R) → (∃ E_sub ⊆ E, ↑E_sub.card ≤ Rtilde ∧ ∃ (witnesses : DeltaTube → Finset (EuclideanSpace ℝ (Fin 2) × EuclideanSpace ℝ (Fin 2))), (∀ T ∈ 𝒯_sub, witnesses T ⊆ E_sub ×ˢ E_sub) ∧ (∀ T ∈ 𝒯_sub, (witnesses T).card ≥ ⌈R ^ 2 / 4⌉₊) ∧ ∀ T₁ ∈ 𝒯_sub, ∀ T₂ ∈ 𝒯_sub, T₁ ≠ T₂ → Disjoint (witnesses T₁) (witnesses T₂)) → ↑𝒯_sub.card ≤ C₁ * Rtilde ^ 2 / R ^ 2

GSW two-ends bound (second ingredient). There exists C₁ > 0 such that whenever a collection 𝒯_sub of R-rich δ-tubes admits, for some scale Rtilde, a subset E_sub ⊆ E of size ≤ Rtilde and pairwise-disjoint witness pairs (one large pair set of size ≥ R²/4 per tube), the number of tubes satisfies $|\mathcal T| \le C_1 \, \widetilde R^2 / R^2$.

This is a combinatorial double-counting on point pairs inside E_sub × E_sub.

theorem ProjectionTheory.gsw_geometric_partition (CF CT : ℝ) : CF > 0 → CT > 0 → ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → ∀ R > 0, R ≤ ↑E.card → ∀ (𝒯 : Finset DeltaTube), (∀ T ∈ 𝒯, T.width = δ) → (∀ T ∈ 𝒯, ↑(T.richness E) ≥ R) → (∀ T₁ ∈ 𝒯, ∀ T₂ ∈ 𝒯, T₁ ≠ T₂ → T₁.EssentiallyDistinct T₂ δ) → ∃ (K : ℕ), ↑K ≤ 1 + Real.log (1 / δ) / Real.log 2 ∧ ∃ (Rtilde : Fin K → ℝ) (n_rho : Fin K → ℝ) (per_rho : Fin K → ℝ), (∀ (k : Fin K), Rtilde k > 0) ∧ (∀ (k : Fin K), 0 ≤ n_rho k) ∧ (∀ (k : Fin K), 0 ≤ per_rho k) ∧ (∀ (k : Fin K), n_rho k ≤ CF * ↑E.card ^ 2 / (R * Rtilde k ^ 2)) ∧ (∀ (k : Fin K), per_rho k ≤ CT * Rtilde k ^ 2 / R ^ 2) ∧ ↑𝒯.card ≤ ∑ k : Fin K, n_rho k * per_rho k

Dyadic geometric partition for GSW. Given the Fourier and two-ends constants CF, CT > 0, the set of R-rich essentially distinct δ-tubes can be partitioned into K ≲ 1 + log(1/δ) dyadic scales Rtilde k, each carrying counts n_rho k, per_rho k bounded respectively by the Fourier and two-ends estimates, with total $|\mathcal T| \le \sum_k n_\rho(k)\, \text{per}_\rho(k)$.

theorem ProjectionTheory.gsw_fat_tube_decomposition : ∃ (C₀ : ℝ) (C₁ : ℝ), C₀ > 0 ∧ C₁ > 0 ∧ ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → ∀ R > 0, R ≤ ↑E.card → ∀ (𝒯 : Finset DeltaTube), (∀ T ∈ 𝒯, T.width = δ) → (∀ T ∈ 𝒯, ↑(T.richness E) ≥ R) → (∀ T₁ ∈ 𝒯, ∀ T₂ ∈ 𝒯, T₁ ≠ T₂ → T₁.EssentiallyDistinct T₂ δ) → ∃ (K : ℕ), ↑K ≤ 1 + Real.log (1 / δ) / Real.log 2 ∧ ∃ (Rtilde : Fin K → ℝ) (fourier : Fin K → ℝ) (twoends : Fin K → ℝ), (∀ (k : Fin K), Rtilde k > 0) ∧ (∀ (k : Fin K), fourier k ≤ C₀ * ↑E.card ^ 2 / (R * Rtilde k ^ 2)) ∧ (∀ (k : Fin K), twoends k ≤ C₁ * Rtilde k ^ 2 / R ^ 2) ∧ (∀ (k : Fin K), 0 ≤ fourier k) ∧ (∀ (k : Fin K), 0 ≤ twoends k) ∧ ↑𝒯.card ≤ ∑ k : Fin K, fourier k * twoends k

Fat-tube decomposition. Combining gsw_basic_fourier_bound, gsw_two_ends_bound, and gsw_geometric_partition, the count of R-rich essentially distinct δ-tubes splits into at most K ≲ 1 + log(1/δ) dyadic pieces, each bounded by the product $\bigl(C_0 |E|^2 / (R\,\widetilde R^2)\bigr) \cdot \bigl(C_1 \widetilde R^2 / R^2\bigr)$.

theorem ProjectionTheory.gsw_dyadic_combination : ∃ C₂ > 0, ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → ∀ R > 0, R ≤ ↑E.card → ∀ (𝒯 : Finset DeltaTube), (∀ T ∈ 𝒯, T.width = δ) → (∀ T ∈ 𝒯, ↑(T.richness E) ≥ R) → (∀ T₁ ∈ 𝒯, ∀ T₂ ∈ 𝒯, T₁ ≠ T₂ → T₁.EssentiallyDistinct T₂ δ) → ↑𝒯.card ≤ C₂ * (1 + Real.log (1 / δ) / Real.log 2) * ↑E.card ^ 2 / R ^ 3

Dyadic combination giving the GSW bound (up to a log). Summing the dyadic pieces of gsw_fat_tube_decomposition yields $|\mathcal T| \le C_2 \bigl(1 + \log_2(1/\delta)\bigr) |E|^2 / R^3$.

theorem ProjectionTheory.log_dominated_by_rpow (ε : ℝ) (hε : 0 < ε) (δ : ℝ) (hδ : 0 < δ) (hδ1 : δ ≤ 1) : 1 + Real.log (1 / δ) / Real.log 2 ≤ (1 + 1 / (ε * Real.log 2)) * δ ^ (-ε)

For any ε > 0, the logarithmic factor 1 + log(1/δ)/log 2 is dominated by (1 + 1/(ε log 2)) · δ^(-ε). Used to convert the log factor in gsw_dyadic_combination into the arbitrarily small loss δ^(-ε) appearing in gsw_theorem.

theorem ProjectionTheory.gsw_theorem (ε : ℝ) (hε : 0 < ε) : ∃ (C_ws : ℝ) (C_conc : ℝ), C_ws > 0 ∧ C_conc > 0 ∧ ∀ (δ : ℝ), 0 < δ → δ ≤ 1 → ∀ (E : Finset (EuclideanSpace ℝ (Fin 2))), 0 < E.card → (∀ x ∈ E, ‖x‖ ≤ 1) → (∀ x ∈ E, ∀ y ∈ E, x ≠ y → δ ≤ dist x y) → IsWellSpaced E C_ws → ∀ R > δ ^ (-ε) * δ * ↑E.card, ∀ (𝒯 : Finset DeltaTube), (∀ T ∈ 𝒯, T.width = δ) → (∀ T ∈ 𝒯, ↑(T.richness E) ≥ R) → (∀ T₁ ∈ 𝒯, ∀ T₂ ∈ 𝒯, T₁ ≠ T₂ → T₁.EssentiallyDistinct T₂ δ) → ↑𝒯.card ≤ C_conc * δ ^ (-ε) * ↑E.card ^ 2 / R ^ 3

Theorem (GSW). Let E ⊂ ℝ² be a set of N δ-balls in B₁ which is well-spaced (every ball of radius N^(-1/2) meets E in ≲ 1 points). Let 𝒯_R(E) be a family of essentially distinct δ-tubes with |T ∩ E|_δ ≥ R, and assume R > δ^(-ε) · δ · |E|_δ. Then $|\mathcal T_R(E)| \lessapprox N^2 / R^3$, formalised here as $|\mathcal T| \le C_\varepsilon \, \delta^{-\varepsilon} |E|^2 / R^3$.