@[reducible, inline]

abbrev TwoEnds.Point : Type

A point in the Euclidean plane ℝ², modelled as EuclideanSpace ℝ (Fin 2).

def TwoEnds.deltaTube (c v : Point) (δ : ℝ) : Set Point

The δ-tube around the unit-length segment {c + t v : |t| ≤ 1/2}: the set of points within Euclidean distance δ of some point on that segment.

def TwoEnds.IsDeltaTube (T : Set Point) (δ : ℝ) : Prop

IsDeltaTube T δ says that T is a δ-tube, i.e. it is of the form deltaTube c v δ for some centre c and unit-length direction v.

structure TwoEnds.WellSpaced (E : Finset Point) (N : ℕ) (C : ℝ) : Prop

A finite set E ⊂ B(0,1) of N points is "well-spaced" (with constant C) in the sense of Sharp Projection Theorems III: it lies in the unit ball, has cardinality comparable to N, and every ball of radius N^{-1/2} contains at most C points of E.

• subset_unitBall (x : Point) : x ∈ E → ‖x‖ ≤ 1
• card_lower : ↑N ≤ C * ↑E.card
• card_upper : ↑E.card ≤ C * ↑N
• spacing (x : Point) : ↑{y ∈ E | ‖y - x‖ ≤ ↑N ^ (-1 / 2)}.card ≤ C

theorem TwoEnds.pair_determines_tube_geometric (δ : ℝ) (hδ : 0 < δ) (tubes : Finset (Set Point)) (h_tubes : ∀ T ∈ tubes, IsDeltaTube T δ) (x₁ x₂ : Point) (hsep : ‖x₁ - x₂‖ ≥ δ) (hx₁ : ∀ T ∈ tubes, x₁ ∈ T) (hx₂ : ∀ T ∈ tubes, x₂ ∈ T) : ↑tubes.card ≤ 1

Geometric incidence fact: a pair of points x₁, x₂ separated by at least δ can lie in at most one δ-tube. (Two distinct δ-tubes through the same δ-separated pair would force their directions to coincide.)

structure TwoEnds.TubeFamily (E : Finset Point) (Tρ : Set Point) (ρ δ : ℝ) (R : ℕ) (C : ℝ) : Type

A family of δ-tubes 𝕋 contained in a fixed ρ-tube Tρ, each of which contains many points of E and additionally satisfies the two-ends condition: for each T ∈ 𝕋 one can split its ≳ R points of E ∩ T into two clusters H₁ T, H₂ T, both of cardinality at least C⁻¹ R, separated by Euclidean distance at least δ. This is exactly the hypothesis of the two-ends lemma.

• hTρ_tube : IsDeltaTube Tρ ρ
• hδ_le_ρ : δ ≤ ρ
• tubes : Finset (Set Point)
• is_tube (T : Set Point) : T ∈ self.tubes → IsDeltaTube T δ
• subset_Tρ (T : Set Point) : T ∈ self.tubes → T ⊆ Tρ
• H₁ : Set Point → Finset Point
• H₂ : Set Point → Finset Point
• H₁_sub (T : Set Point) : T ∈ self.tubes → self.H₁ T ⊆ {x ∈ E | x ∈ Tρ}
• H₂_sub (T : Set Point) : T ∈ self.tubes → self.H₂ T ⊆ {x ∈ E | x ∈ Tρ}
• H₁_in_tube (T : Set Point) : T ∈ self.tubes → ∀ x ∈ self.H₁ T, x ∈ T
• H₂_in_tube (T : Set Point) : T ∈ self.tubes → ∀ x ∈ self.H₂ T, x ∈ T
• separation (T : Set Point) : T ∈ self.tubes → ∀ x ∈ self.H₁ T, ∀ y ∈ self.H₂ T, ‖x - y‖ ≥ δ
• H₁_card (T : Set Point) : T ∈ self.tubes → C⁻¹ * ↑R ≤ ↑(self.H₁ T).card
• H₂_card (T : Set Point) : T ∈ self.tubes → C⁻¹ * ↑R ≤ ↑(self.H₂ T).card

theorem TwoEnds.pair_determines_tube_from_geometry (δ : ℝ) (hδ : 0 < δ) (tubes : Finset (Set Point)) (is_tube : ∀ T ∈ tubes, IsDeltaTube T δ) (H₁ H₂ : Set Point → Finset Point) (H₁_in_tube : ∀ T ∈ tubes, ∀ x ∈ H₁ T, x ∈ T) (H₂_in_tube : ∀ T ∈ tubes, ∀ x ∈ H₂ T, x ∈ T) (separation : ∀ T ∈ tubes, ∀ x ∈ H₁ T, ∀ y ∈ H₂ T, ‖x - y‖ ≥ δ) (x₁ x₂ : Point) : ↑{T ∈ tubes | x₁ ∈ H₁ T ∧ x₂ ∈ H₂ T}.card ≤ 1

Combinatorial consequence of pair_determines_tube_geometric: a fixed ordered pair (x₁, x₂) can play the role of (H₁, H₂) representatives for at most one tube in the family. This is the pointwise upper bound on the double-counting sum used in the proof of the two-ends lemma.

theorem TwoEnds.two_ends_lemma (E : Finset Point) (C ρ δ : ℝ) (R R_tilde : ℕ) (Tρ : Set Point) (hC : C ≥ 1) (hδ : 0 < δ) (hR : 0 < R) (hTρ_upper : ↑{x ∈ E | x ∈ Tρ}.card ≤ C * ↑R_tilde) (𝕋 : TubeFamily E Tρ ρ δ R C) : ↑𝕋.tubes.card ≤ C ^ 4 * ↑R_tilde ^ 2 / ↑R ^ 2

Lemma (two ends). Let E be a well-spaced set in B¹ ⊂ ℝ² with |E| ∼ N and |E ∩ B(x, N^{-1/2})| ≲ 1, let δ ≤ ρ ≤ N^{-1/2}, and let Tρ be a ρ-tube with |Tρ ∩ E|_ρ ∼ R̃. If every δ-tube T ∈ 𝕋_R(E, Tρ) obeys the two-ends condition, then $$\big|\mathbb{T}_R(E, T_\rho)\big| \;\lesssim\; \frac{\tilde R^{\,2}}{R^{\,2}}.$$ The proof double-counts triples (T, x, y) with x ∈ H₁ T, y ∈ H₂ T, using pair_determines_tube_from_geometry for the upper bound.