LatticeCount

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The triadic lattice annulus is finite, with an explicit count

ABK26, §4.1, l.good.scales.ratio.lambda, the per-annulus atom tail: the union-bound penalty C(n−k+1)³ of the lattice maximum

max_{z ∈ 3^{k−2}ℤ^d ∩ (□_n ∖ □_{n−1})} ( … )_+

This module proves it.

What is proved

• abs_le_of_mem_latticeCubeSet — a lattice point of spacing 3^j inside □_outer has integer coordinates bounded by 3^{outer−j} (crude by a factor 2, which costs nothing downstream).
• latticeAnnulusFinset — the Finset of those index vectors, with card_latticeAnnulusFinset_le giving # ≤ 3^{d(outer−j+1)}.
• log_card_latticeAnnulusFinset_le — the form the union bound consumes, and annulusPenalty / log_card_le_annulusPenalty_rpow_sub_one — the admissible penalty c of isBigOWith_fmax, which at σ = 1/3 is a cubic in outer − j, the manuscript's C(n−k+1)³.

Scope

Provider material: proved local helpers. Pure geometry and counting; no probability, no model, no standing assumption.

References

• ABK26, l.good.scales.ratio.lambda.

1. The coordinate bound

theorem Algsuperdiff.Section4.Provider.Proportion.abs_le_of_mem_latticeCubeSet {d : ℕ} {j outer : ℤ} (hj : j ≤ outer) {v : Fin d → ℤ} (hv : v ∈ Support.latticeCubeSet d j outer) (i : Fin d) : |v i| ≤ 3 ^ (outer - j).toNat

A triadic lattice point of spacing 3^j inside □_outer has bounded index. The sharp bound is (3^{outer−j} − 1)/2; the crude 3^{outer−j} used here avoids an integer division and costs only a bounded factor in the logarithm.

2. The enclosing box and its cardinality

def Algsuperdiff.Section4.Provider.Proportion.boxIndexFinset (d : ℕ) (B : ℤ) : Finset (Fin d → ℤ)

The Finset of integer index vectors with all coordinates in [-B, B].

Equations

• Algsuperdiff.Section4.Provider.Proportion.boxIndexFinset d B = Fintype.piFinset fun (x : Fin d) => Finset.Icc (-B) B

theorem Algsuperdiff.Section4.Provider.Proportion.mem_boxIndexFinset_iff {d : ℕ} {B : ℤ} {v : Fin d → ℤ} : v ∈ boxIndexFinset d B ↔ ∀ (i : Fin d), |v i| ≤ B

theorem Algsuperdiff.Section4.Provider.Proportion.card_boxIndexFinset (d : ℕ) (B : ℤ) : (boxIndexFinset d B).card = (2 * B + 1).toNat ^ d

3. The annulus Finset

noncomputable def Algsuperdiff.Section4.Provider.Proportion.latticeAnnulusFinset (d : ℕ) (j outer inner : ℤ) : Finset (Fin d → ℤ)

The lattice annulus as a Finset. The proved set Support.latticeAnnulusSet cut out of the enclosing index box.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.Proportion.mem_latticeAnnulusFinset_iff {d : ℕ} {j outer inner : ℤ} (hj : j ≤ outer) {v : Fin d → ℤ} : v ∈ latticeAnnulusFinset d j outer inner ↔ v ∈ Support.latticeAnnulusSet d j outer inner

theorem Algsuperdiff.Section4.Provider.Proportion.card_latticeAnnulusFinset_le (d : ℕ) {j outer inner : ℤ} : (latticeAnnulusFinset d j outer inner).card ≤ 3 ^ (d * ((outer - j).toNat + 1))

The count. #(3^j ℤ^d ∩ (□_outer ∖ □_inner)) ≤ 3^{d(outer−j+1)}.

4. The union-bound penalty

theorem Algsuperdiff.Section4.Provider.Proportion.log_card_latticeAnnulusFinset_le (d : ℕ) {j outer inner : ℤ} : Real.log ↑(latticeAnnulusFinset d j outer inner).card ≤ ↑d * (↑(outer - j).toNat + 1) * Real.log 3

The logarithm of the count, in the form the union bound consumes.

noncomputable def Algsuperdiff.Section4.Provider.Proportion.annulusPenalty (d : ℕ) (sigma : ℝ) (p : ℕ) : ℝ

The annular counting penalty in the proportion tail estimate.

Equations

• Algsuperdiff.Section4.Provider.Proportion.annulusPenalty d sigma p = (1 + ↑d * (↑p + 1) * Real.log 3) ^ sigma⁻¹

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenalty_base_nonneg (d p : ℕ) : 0 ≤ 1 + ↑d * (↑p + 1) * Real.log 3

theorem Algsuperdiff.Section4.Provider.Proportion.one_le_annulusPenalty (d : ℕ) {sigma : ℝ} (hsigma : 0 < sigma) (p : ℕ) : 1 ≤ annulusPenalty d sigma p

theorem Algsuperdiff.Section4.Provider.Proportion.annulusPenalty_rpow (d : ℕ) {sigma : ℝ} (hsigma : 0 < sigma) (p : ℕ) : annulusPenalty d sigma p ^ sigma = 1 + ↑d * (↑p + 1) * Real.log 3

The penalty raised back to the power σ returns its base.

theorem Algsuperdiff.Section4.Provider.Proportion.log_card_le_annulusPenalty_rpow_sub_one (d : ℕ) {sigma : ℝ} (hsigma : 0 < sigma) (j outer inner : ℤ) : Real.log ↑(latticeAnnulusFinset d j outer inner).card ≤ annulusPenalty d sigma (outer - j).toNat ^ sigma - 1

The defining property of the penalty: it clears the isBigOWith_fmax interface log(#S) ≤ c^σ − 1 at the lattice annulus.