noncomputable def Marstrand.directionVector (θ : ℝ) : EuclideanSpace ℝ (Fin 2)

The unit direction vector $(\cos\theta, \sin\theta) \in \mathbb{R}^2$ associated to the angle $\theta$.

noncomputable def Marstrand.orthProjLine (θ : ℝ) : EuclideanSpace ℝ (Fin 2) →L[ℝ] ℝ

Orthogonal projection $\pi_\theta : \mathbb{R}^2 \to \mathbb{R}$ onto the line through the origin in direction $\theta$, expressed as the continuous linear functional $x \mapsto \langle x, (\cos\theta, \sin\theta) \rangle$.

theorem Marstrand.marstrand_projection (X : Set (EuclideanSpace ℝ (Fin 2))) (hX : IsCompact X) : ∀ᵐ (θ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ico 0 Real.pi), dimH (⇑(orthProjLine θ) '' X) = min (dimH X) 1

Marstrand's projection theorem (1954). If $X \subseteq \mathbb{R}^2$ is compact, then for almost every angle $\theta \in [0, \pi)$ the Hausdorff dimension of the orthogonal projection $\pi_\theta(X)$ onto the line in direction $\theta$ equals $\min(\dim_H X, 1)$.