def UniformSet.IsSubAdditive {d : ℕ} (μ : Finset (Fin d → ℕ) → ℝ) : Prop

A real-valued set function μ is sub-additive if μ(A ∪ B) ≤ μ(A) + μ(B) for all finite sets A, B. This is the hypothesis used in the Uniformization Lemma (e.g. μ(B) = |B|_δ).

def UniformSet.IsMonotoneSetFn {d : ℕ} (μ : Finset (Fin d → ℕ) → ℝ) : Prop

A real-valued set function μ is monotone if A ⊆ B implies μ A ≤ μ B.

def UniformSet.IsUniformFrom (N m d k : ℕ) (X : Finset (Fin d → ℕ)) : Prop

IsUniformFrom N m d k X is the "partial" uniformity property used in the inductive proof of the Uniformization Lemma: the set X is required to be (Δ, m)-uniform only at scales j ∈ {k, k+1, …, m-1}. Taking k = 0 recovers the full IsUniform predicate; k = m is automatic.

theorem UniformSet.isUniform_iff_uniformFrom_zero (N m d : ℕ) (X : Finset (Fin d → ℕ)) : IsUniform N m d X ↔ IsUniformFrom N m d 0 X

Full (Δ, m)-uniformity is the same as IsUniformFrom starting at scale 0.

theorem UniformSet.isUniformFrom_m (N m d : ℕ) (X : Finset (Fin d → ℕ)) : IsUniformFrom N m d m X

Every set is vacuously IsUniformFrom at the top scale k = m, since there are no indices j satisfying m ≤ j < m. This is the base case for the inductive proof of the Uniformization Lemma.

theorem UniformSet.dyadic_range_card_bound (N m d : ℕ) (hN : N ≥ 2) (hd : d ≥ 1) (k : ℕ) (hk : k < m) (X : Finset (Fin d → ℕ)) (hX : X.Nonempty) : ↑(Finset.image (fun (p : Fin d → ℕ) => subcubeCovering N m k d X (cubeOf N m k p)) X).card ≤ 2 * ↑d * Real.log ↑N

Pigeon-hole bound: at any fixed scale k, the number of distinct branching values R_j taken by the sub-cube counts across the cubes of X is at most 2 d log(N). This is the loss factor that appears at each scale in the Uniformization Lemma.

theorem UniformSet.one_step_uniformization (N m d : ℕ) (hN : N ≥ 2) (hd : d ≥ 1) (k : ℕ) (hk : k < m) (X : Finset (Fin d → ℕ)) (hX : X.Nonempty) (hXunif : IsUniformFrom N m d (k + 1) X) (μ : Finset (Fin d → ℕ) → ℝ) (hμ_sub : IsSubAdditive μ) (hμ_mono : IsMonotoneSetFn μ) (hμ_nonneg : ∀ (S : Finset (Fin d → ℕ)), 0 ≤ μ S) : ∃ Y ⊆ X, Y.Nonempty ∧ IsUniformFrom N m d k Y ∧ μ Y ≥ (2 * ↑d * Real.log ↑N)⁻¹ * μ X

One inductive step of the Uniformization Lemma. If X is already uniform at every scale j ≥ k + 1, then by pigeon-holing the branching factor at scale k we can pass to a subset Y ⊆ X which is uniform from scale k onward, while losing only a factor of (2 d log N)⁻¹ in the sub-additive measure μ.

theorem UniformSet.uniformization_lemma (N m d : ℕ) (hN : N ≥ 2) (hd : d ≥ 1) (hm : m ≥ 1) (X : Finset (Fin d → ℕ)) (hX : X.Nonempty) (μ : Finset (Fin d → ℕ) → ℝ) (hμ_sub : IsSubAdditive μ) (hμ_mono : IsMonotoneSetFn μ) (hμ_empty : μ ∅ = 0) (hμ_nonneg : ∀ (S : Finset (Fin d → ℕ)), 0 ≤ μ S) : ∃ Y ⊆ X, Y.Nonempty ∧ IsUniform N m d Y ∧ μ Y ≥ (2 * ↑d * Real.log ↑N)⁻¹ ^ m * μ X

Uniformization Lemma (Bourgain). Let δ = Δ^m = N^{-m}, let X ⊂ {0, …, N^m - 1}^d, and let μ be any non-negative, monotone, sub-additive set function with μ ∅ = 0. Then there is a subset Y ⊆ X that is (Δ, m)-uniform and satisfies $$\mu(Y) \ge \big[2 d \ln(1/\Delta)\big]^{-m} \, \mu(X) = \delta^{-\sigma}\, \mu(X), \qquad \sigma = \frac{\ln(2 \ln(1/\Delta))}{\ln(1/\Delta)}.$$ The proof iterates one_step_uniformization for m scales, losing the factor (2 d log N)⁻¹ at each one.