def FurstenbergSets.IsDeltaSC (E : Finset (EuclideanSpace ℝ (Fin 2))) (δ s C : ℝ) : Prop

A planar finset $E$ is a $(\delta, s, C)$-set in the unit ball: every point has norm $\le 1$, distinct points are $\ge \delta$ apart, and for every ball $B(x, r)$ with $r \ge \delta$, $|E \cap B(x,r)| \le C r^s |E|$.

def FurstenbergSets.IsDeltaSC_S1 (D : Finset ℝ) (δ s C : ℝ) : Prop

A finset of angles $D \subset [0, 2\pi)$ is a $(\delta, s, C)$-set on $S^1$: distinct angles are $\delta$-separated (mod $2\pi$), and for every arc of length $r \ge \delta$, $|D \cap B(\theta_0, r)| \le C r^s |D|$.

structure FurstenbergSets.FurstenbergConfig : Type

Configuration data for the Furstenberg $\delta$-tube incidence proposition: a scale $\delta$, exponents $t$ (for $E$) and $s$ (for the direction sets), a $(\delta, t, C)$-set $E \subset \mathbb{R}^2$, and for each $x \in E$ a $(\delta, s, C)$-set of tube directions $\mathbb{T}_x \subset S^1$, together with a total-tube count totalTubes bounding $|\mathbb{T}_x|$ uniformly.

• δ : ℝ
• t : ℝ
• s : ℝ
• C : ℝ
• E : Finset (EuclideanSpace ℝ (Fin 2))
• tubeDirections : EuclideanSpace ℝ (Fin 2) → Finset ℝ
• totalTubes : ℕ
• hδ_pos : 0 < self.δ
• hδ_le : self.δ ≤ 1
• hs_pos : 0 < self.s
• ht_pos : 0 < self.t
• hC : 1 ≤ self.C
• hE_spacing : IsDeltaSC self.E self.δ self.t self.C
• hDir_spacing (x : EuclideanSpace ℝ (Fin 2)) : x ∈ self.E → IsDeltaSC_S1 (self.tubeDirections x) self.δ self.s self.C
• hTotalTubes_lower (x : EuclideanSpace ℝ (Fin 2)) : x ∈ self.E → (self.tubeDirections x).card ≤ self.totalTubes