def BourgainUniform.meshCube {d : ℕ} (δ : ℝ) (k : Fin d → ℤ) : Set (EuclideanSpace ℝ (Fin d))

The half-open dyadic mesh cube indexed by $k \in \mathbb{Z}^d$ at scale $\delta$: $\{x : k_i \delta \leq x_i < (k_i+1)\delta\ \forall i\}$.

def BourgainUniform.meshCubesIntersecting {d : ℕ} (δ : ℝ) (X : Set (EuclideanSpace ℝ (Fin d))) : Set (Fin d → ℤ)

The set of mesh-cube indices $k \in \mathbb{Z}^d$ such that the cube at scale $\delta$ indexed by $k$ has nonempty intersection with $X$.

noncomputable def BourgainUniform.meshCount {d : ℕ} (δ : ℝ) (X : Set (EuclideanSpace ℝ (Fin d))) : ℕ∞

The mesh-counting function $|X|_\delta$: the (possibly infinite) number of $\delta$-mesh cubes that intersect $X$.

structure BourgainUniform.IsUniform {d : ℕ} (Δ : ℝ) (m : ℕ) (X : Set (EuclideanSpace ℝ (Fin d))) : Prop

IsUniform Δ m X is Bourgain's $(\Delta, m)$-uniformity: $X \subset [0,1]^d$, $\Delta = 1/n$ for some $n \in \mathbb{N}$, and for each $j < m$ the number of $\Delta^{j+1}$-mesh cubes inside any given $\Delta^j$-mesh cube of $X$ is a constant $R_j$ independent of the cube (the "branching factor" at step $j$).

• delta_recip_nat : ∃ (n : ℕ), 0 < n ∧ Δ = 1 / ↑n
• subset_unitCube : X ⊆ {x : EuclideanSpace ℝ (Fin d) | ∀ (i : Fin d), 0 ≤ x.ofLp i ∧ x.ofLp i ≤ 1}
• branching_uniform (j : ℕ) : j < m → ∃ (R : ℕ∞), ∀ k ∈ meshCubesIntersecting (Δ ^ j) X, meshCount (Δ ^ (j + 1)) (meshCube (Δ ^ j) k ∩ X) = R

def BourgainUniform.IsRegularSet {d : ℕ} (δ s : ℝ) (C : NNReal) (X : Set (EuclideanSpace ℝ (Fin d))) : Prop

IsRegularSet δ s C X says that $X$ is a $(\delta, s, C)$-regular set: for every scale $\rho \in [\delta, 1]$ and every $\rho$-mesh cube $Q$, $|X \cap Q|_\delta \leq C \rho^s |X|_\delta$, the discrete analogue of Frostman regularity with exponent $s$.