noncomputable def ProjectionTheory.orthProj (θ : ℝ) (x : EuclideanSpace ℝ (Fin 2)) : ℝ

Orthogonal projection of a point x ∈ ℝ² onto the line through the origin making angle θ with the $x$-axis: $\pi_\theta(x) = x_0 \cos\theta + x_1 \sin\theta$.

def ProjectionTheory.exceptionalSetHD (X : Set (EuclideanSpace ℝ (Fin 2))) (s : ENNReal) : Set ℝ

The Hausdorff-dimension exceptional set: the set of directions θ for which the orthogonal projection orthProj θ '' X of X ⊂ ℝ² has Hausdorff dimension strictly less than s.

theorem ProjectionTheory.orponen_shmerkin_ren_wang (X : Set (EuclideanSpace ℝ (Fin 2))) (s : ENNReal) (hs : s < dimH X) : dimH (exceptionalSetHD X s) ≤ 2 * s - dimH X

Orponen–Shmerkin–Ren–Wang theorem. For X ⊂ ℝ² and s < dimH X, the set of directions whose projection of X has Hausdorff dimension < s is itself small: $$\dim_H\{\theta : \dim_H(\pi_\theta X) < s\} \le 2s - \dim_H X.$$