noncomputable def ProjectionTheory.dyadicExponentRange (R : ℝ) : Finset ℕ

The finite range of dyadic exponents {0, 1, …, ⌊log₂ R⌋} used to index the scales r = 2^k in dyadic decompositions up to a real cutoff R.

@[reducible, inline]

abbrev ProjectionTheory.Point2 : Type

A point in the Euclidean plane ℝ², encoded as Fin 2 → ℝ.

@[reducible, inline]

abbrev ProjectionTheory.Direction : Type

A direction vector in ℝ², encoded as Fin 2 → ℝ.

noncomputable def ProjectionTheory.projDir (θ : Direction) (x : Point2) : ℝ

The projection π_θ(x) = x · θ = ∑_i x_i θ_i of a planar point x onto the direction θ ∈ ℝ².

noncomputable def ProjectionTheory.collisionSet (X : Finset Point2) (D : Finset Direction) : Finset (Point2 × Point2 × Direction)

The set of triples (x₁, x₂, θ) ∈ X × X × D whose projections under θ are within distance 2, i.e. |π_θ(x₁) − π_θ(x₂)| ≤ 2. Its cardinality is the incidence quantity that is bounded both from below and above in the real-version double counting argument.

structure ProjectionTheory.DoubleCountingRealSetup : Type

The data for the SETUP of the real-version double-counting theorem: a scale parameter R ≥ 1, the cardinalities |X| and |D| of a planar point set and a direction set, the maximal projection size S (with 0 < S ≤ |X|), and the multiscale covering numbers N_X(r), N_D(ρ) at radii r, ρ.

• R : ℝ
• hR : 1 ≤ self.R
• cardX : ℕ
• cardD : ℕ
• S : ℕ
• hS_pos : 0 < self.S
• hS_le : self.S ≤ self.cardX
• N_X : ℝ → ℕ
• N_D : ℝ → ℕ
• hN_X_le (r : ℝ) : self.N_X r ≤ self.cardX
• hN_D_le (ρ : ℝ) : self.N_D ρ ≤ self.cardD

noncomputable def ProjectionTheory.dyadicSum (setup : DoubleCountingRealSetup) : ℕ

The dyadic incidence-count sum ∑_{1 ≤ r ≤ R, dyadic} N_X(r) · N_D(1/r) appearing on the right-hand side of the real-version double-counting theorem.

theorem ProjectionTheory.double_counting_real (setup : DoubleCountingRealSetup) (hX_pos : 0 < setup.cardX) (collisionCount : ℝ) (hLower : ∃ c₁ > 0, c₁ * ↑setup.cardD * (↑setup.cardX ^ 2 / ↑setup.S) ≤ collisionCount) (hUpper : ∃ c₂ > 0, collisionCount ≤ c₂ * ↑setup.cardX * ↑(∑ k ∈ dyadicExponentRange setup.R, setup.N_X (2 ^ k) * setup.N_D (2 ^ k)⁻¹)) : ∃ C > 0, ↑setup.cardD ≤ C * (↑setup.S / ↑setup.cardX) * ↑(dyadicSum setup)

Theorem (Double Counting, real version). Under the standard SETUP, an incidence (collision) count I admits the lower bound I ≳ |D| · |X|² / S and the upper bound I ≲ |X| · ∑_r N_X(r) N_D(1/r). Combining these gives |D| ≲ (S/|X|) ∑_{1 ≤ r ≤ R} N_X(r) N_D(1/r).