Absolute lattice-ball counts for the Hepp-tree volume estimate

This file isolates the geometric counting input in paper §5.3, Step 5. Unlike the ambient-box bound used elsewhere to enumerate admissible embeddings, these estimates are uniform in the box cutoff M.

The norm is Anderson4D.znorm, hence the sup norm on ℤ⁴. We enumerate a real-radius ball by filtering a finite coordinate box, then apply the unit-separation packing estimate from PermSum.Local. The resulting absolute constant is 16. A union of k balls and the specialization needed in paper (5.23) are provided at the end.

@[reducible, inline]

abbrev Anderson4D.LatticePoint : Type

Equations

• Anderson4D.LatticePoint = (Fin 4 → ℤ)

A finite set representing a real-radius lattice ball

noncomputable def Anderson4D.latticeBallReal (c : LatticePoint) (R : ℝ) : Finset LatticePoint

The finite set of integer points in the closed znorm-ball of radius R around c. The outer coordinate box is deliberately only an enumeration device; membership is exactly the norm inequality.

Equations

• Anderson4D.latticeBallReal c R = {x ∈ Fintype.piFinset fun (i : Fin 4) => Finset.Icc (c i + ⌊-R⌋) (c i + ⌊R⌋) | Anderson4D.znorm (x - c) ≤ R}

@[simp]

theorem Anderson4D.mem_latticeBallReal {c x : LatticePoint} {R : ℝ} : x ∈ latticeBallReal c R ↔ znorm (x - c) ≤ R

theorem Anderson4D.one_le_znorm_sub_of_ne {x y : LatticePoint} (hxy : x ≠ y) : 1 ≤ znorm (x - y)

Distinct integer lattice points are 1-separated in znorm.

theorem Anderson4D.card_latticeBallReal_le (c : LatticePoint) (R : ℝ) : ↑(latticeBallReal c R).card ≤ 16 * (1 + R) ^ 4

Absolute real-radius lattice-ball count. The constant 16 is independent of the center, radius, and any ambient lattice cutoff.

A directly usable natural-radius version

noncomputable def Anderson4D.latticeBallNat (c : LatticePoint) (R : ℕ) : Finset LatticePoint

Natural-radius spelling of latticeBallReal.

Equations

• Anderson4D.latticeBallNat c R = Anderson4D.latticeBallReal c ↑R

@[simp]

theorem Anderson4D.mem_latticeBallNat {c x : LatticePoint} {R : ℕ} : x ∈ latticeBallNat c R ↔ znorm (x - c) ≤ ↑R

theorem Anderson4D.card_latticeBallNat_le (c : LatticePoint) (R : ℕ) : (latticeBallNat c R).card ≤ 16 * (R + 1) ^ 4

Natural-number cardinality bound for a natural-radius ball.

Unions of balls and the paper (5.23) specialization

noncomputable def Anderson4D.latticeBallUnion (centers : Finset LatticePoint) (R : ℝ) : Finset LatticePoint

Union of equal-radius lattice balls about a finite set of fixed centers.

Equations

• Anderson4D.latticeBallUnion centers R = centers.biUnion fun (c : Anderson4D.LatticePoint) => Anderson4D.latticeBallReal c R

@[simp]

theorem Anderson4D.mem_latticeBallUnion {centers : Finset LatticePoint} {R : ℝ} {x : LatticePoint} : x ∈ latticeBallUnion centers R ↔ ∃ c ∈ centers, znorm (x - c) ≤ R

theorem Anderson4D.card_latticeBallUnion_le (centers : Finset LatticePoint) (R : ℝ) : ↑(latticeBallUnion centers R).card ≤ 16 * ↑centers.card * (1 + R) ^ 4

A union of k fixed balls costs at most k times the absolute single-ball bound.

def Anderson4D.step5LatticeConstant : ℕ

Absolute constant used by the normalized Step-5 lattice count.

Equations

• Anderson4D.step5LatticeConstant = 3888

theorem Anderson4D.card_latticeBallUnion_step5_le (centers : Finset LatticePoint) (Nr Ti Tj : ℝ) (hNr : 1 ≤ Nr) (hTi : 0 ≤ Ti) (hTj : 0 ≤ Tj) (hcenters : ↑centers.card ≤ 3 * (1 + Ti / Nr)) : ↑(latticeBallUnion centers (2 * (Nr + Tj))).card ≤ ↑step5LatticeConstant * Nr ^ 4 * (1 + Ti / Nr) * (1 + Tj / Nr) ^ 4

Paper §5.3 Step 5, equation (5.23), in a form directly consumable when the covering centers form a Finset.

The hypotheses encode:

• Nr ≥ 1;
• nonnegative subtree lengths Ti,Tj;
• at most 3(1 + Ti/Nr) covering centers;
• radius 2(Nr+Tj).

The conclusion has exactly the normalized factors of (5.23), with the absolute explicit constant 3888 = 16 · 3 · 3⁴.

Indexed-center wrappers, convenient when the k centers are supplied as a function rather than as a duplicate-free Finset.

noncomputable def Anderson4D.latticeBallUnionFin {k : ℕ} (center : Fin k → LatticePoint) (R : ℝ) : Finset LatticePoint

Union of the balls centered at an indexed family of k points.

Equations

• Anderson4D.latticeBallUnionFin center R = Anderson4D.latticeBallUnion (Finset.image center Finset.univ) R

@[simp]

theorem Anderson4D.mem_latticeBallUnionFin {k : ℕ} {center : Fin k → LatticePoint} {R : ℝ} {x : LatticePoint} : x ∈ latticeBallUnionFin center R ↔ ∃ (i : Fin k), znorm (x - center i) ≤ R

theorem Anderson4D.card_latticeBallUnionFin_le {k : ℕ} (center : Fin k → LatticePoint) (R : ℝ) : ↑(latticeBallUnionFin center R).card ≤ 16 * ↑k * (1 + R) ^ 4

The direct k-indexed union bound.

theorem Anderson4D.card_latticeBallUnionFin_step5_le {k : ℕ} (center : Fin k → LatticePoint) (Nr Ti Tj : ℝ) (hNr : 1 ≤ Nr) (hTi : 0 ≤ Ti) (hTj : 0 ≤ Tj) (hk : ↑k ≤ 3 * (1 + Ti / Nr)) : ↑(latticeBallUnionFin center (2 * (Nr + Tj))).card ≤ ↑step5LatticeConstant * Nr ^ 4 * (1 + Ti / Nr) * (1 + Tj / Nr) ^ 4

Indexed-center form of (5.23).