@[reducible, inline]

noncomputable abbrev ProjectionTheory.ℝ2 : Type

Shorthand for the Euclidean plane ℝ² with its standard inner product.

structure ProjectionTheory.RSetup : Type

The "real R-SETUP" for the Euclidean version of Theorem 2.3. Bundles a scale R ≥ 1, a finite point set X ⊂ ℝ², a set of directions D ⊂ ℝ that is 1/R-separated, and a uniform projection bound |π_θ(X)| ≤ S for all θ ∈ D. This is the standard hypothesis under which the Fourier-method projection estimates are proved.

• R : ℝ
• hR : 1 ≤ self.R
• X : Finset ℝ2
• D : Finset ℝ
• hD_sep (θ₁ : ℝ) : θ₁ ∈ self.D → ∀ θ₂ ∈ self.D, θ₁ ≠ θ₂ → |θ₁ - θ₂| ≥ 1 / self.R
• S : ℕ
• hS_pos : 0 < self.S
• hS_bound (θ : ℝ) : θ ∈ self.D → (Finset.image (orthProj θ) self.X).card ≤ self.S
• hX_nonempty : self.X.Nonempty
• hD_nonempty : self.D.Nonempty