@[reducible, inline]

noncomputable abbrev RestrictedProjection.S2 : Set (EuclideanSpace ℝ (Fin 3))

The unit sphere $S^2 \subset \mathbb{R}^3$.

noncomputable def RestrictedProjection.orthogonalProjectionTo (θ : EuclideanSpace ℝ (Fin 3)) : EuclideanSpace ℝ (Fin 3) → EuclideanSpace ℝ (Fin 3)

Orthogonal projection $\pi_\theta : \mathbb{R}^3 \to \mathbb{R}^3$ onto the plane perpendicular to a direction $\theta$, given by $v \mapsto v - \langle v, \theta\rangle\,\theta$.

def RestrictedProjection.IsNonDegenerate (γ : ℝ → EuclideanSpace ℝ (Fin 3)) : Prop

A spherical curve $\gamma : \mathbb{R} \to S^2$ is non-degenerate if it is $C^2$ and, at every parameter $t$, the second derivative $\gamma''(t)$ is not contained in the linear span of $\gamma(t)$ and $\gamma'(t)$; equivalently $\gamma, \gamma', \gamma''$ are pointwise linearly independent.

def RestrictedProjection.projImage (θ : EuclideanSpace ℝ (Fin 3)) (X : Set (EuclideanSpace ℝ (Fin 3))) : Set (EuclideanSpace ℝ (Fin 3))

The image $\pi_\theta(X)$ of $X \subset \mathbb{R}^3$ under orthogonal projection perpendicular to the direction $\theta$.

noncomputable def RestrictedProjection.arcLengthAverage (γ : ℝ → EuclideanSpace ℝ (Fin 3)) (f : EuclideanSpace ℝ (Fin 3) → ℝ) (a b : ℝ) : ℝ

The arc-length average of $f$ along the curve $\gamma$ on $[a,b]$, i.e. $\bigl(\int_a^b \|\gamma'\|\bigr)^{-1} \int_a^b f(\gamma(t))\,\|\gamma'(t)\|\,dt$.

theorem RestrictedProjection.gan_guo_guth_harris_maldague_wang (X : Set (EuclideanSpace ℝ (Fin 3))) (γ : ℝ → EuclideanSpace ℝ (Fin 3)) (δ C : ℝ) (hδ : 0 < δ) (hC : 0 < C) (hX : DeltaRegular.IsDeltaSRegular δ 2 C X) (hγ : IsNonDegenerate γ) (ε : ℝ) (hε : 0 < ε) : ∃ (C_ε : ℝ), 0 < C_ε ∧ ∀ (a b : ℝ), a < b → arcLengthAverage γ (fun (θ : EuclideanSpace ℝ (Fin 3)) => (↑(DeltaRegular.deltaCoveringNumber δ (projImage θ X))).toReal) a b ≥ C_ε * δ ^ (-2 + ε)

Gan–Guo–Guth–Harris–Maldague–Wang theorem. If $X \subset B^3$ is a $(\delta, 2, C)$-set and $\gamma$ is a non-degenerate spherical curve, then for every $\varepsilon > 0$, $\operatorname{Avg}_{\theta \in \gamma} |\pi_\theta(X)|_\delta \ge C_\varepsilon \, \delta^{-2 + \varepsilon}$, i.e. averaging the $\delta$-covering number of the projection along the curve recovers nearly the full upper bound.