Bilinear lattice-cluster bound (Lemma 5.14 of arXiv:2607.10105)

This file formalizes the PAPER_MAP node L-5.14 of the Deng–Shen four-dimensional Anderson model paper (Y. Deng, H. Shen, The four-dimensional Anderson model: a case study for critical SPDEs, arXiv:2607.10105). It provides:

• card_shell_le — the separated-points-in-a-ball packing/shell count, paper (5.61);
• sum_inv_sq_le — the single-variable dyadic sum estimate, paper (5.60)/(5.62);
• bilinear_cluster_bound_weak — the trivial-direction component of (5.58), obtained by iterating (5.60). The refined factor is proved in LocalRefined.lean.

Design notes (project DESIGN §5.4)

• The ambient norm on ℤ⁴ is fixed to the sup norm on Fin 4 → ℝ (mathlib's default Pi norm) applied to the real coercion of an integer vector; this is packaged as Anderson4D.znorm. All constants below are norm-choice dependent and are absorbed into the named line-constants; the paper's ≳/≲ become explicit constants introduced existentially (single-use line constants) or the concrete value 16 in card_shell_le.
• Powers. Half-powers |A|^{1/2} are written with Real.sqrt. (The refined bound's quarter power (Q/P)^{1/4} would be Real.rpow, · ^ (1/4 : ℝ); it is not present in the delivered _weak form.)
• Indicators. The membership constraints 𝟙_{|u-x| ≳ M} etc. are represented as Finset.filter on the summation domain (equivalently, sub-sums), not as if … then 1.
• The recurring dyadic-decomposition engine is factored into the reusable private lemmas sum_geom_incr_le, sum_geom_decr_le, dyadic_min_geom_sum.

def Anderson4D.znorm (x : Fin 4 → ℤ) : ℝ

Sup-norm of an integer 4-vector x : Fin 4 → ℤ, defined via the real coercion (fun i => (x i : ℝ)) and mathlib's default Pi (sup) norm on Fin 4 → ℝ. See paper §5.4; all constants below are relative to this choice.

Equations

• Anderson4D.znorm x = ‖fun (i : Fin 4) => ↑(x i)‖

theorem Anderson4D.znorm_nonneg (x : Fin 4 → ℤ) : 0 ≤ znorm x

theorem Anderson4D.znorm_coord_le (x : Fin 4 → ℤ) (i : Fin 4) : |↑(x i)| ≤ znorm x

Each coordinate is controlled by the sup norm.

theorem Anderson4D.znorm_sub_coord (x y : Fin 4 → ℤ) (i : Fin 4) : |↑(x i) - ↑(y i)| ≤ znorm (x - y)

Coordinatewise bound for a difference.

theorem Anderson4D.znorm_lt_iff (v : Fin 4 → ℤ) (M : ℝ) (hM : 0 < M) : znorm v < M ↔ ∀ (i : Fin 4), |↑(v i)| < M

The sup norm is < M iff every coordinate is.

theorem Anderson4D.znorm_neg (x : Fin 4 → ℤ) : znorm (-x) = znorm x

Reflection symmetry of znorm.

theorem Anderson4D.znorm_sub_comm (x y : Fin 4 → ℤ) : znorm (x - y) = znorm (y - x)

theorem Anderson4D.card_ball_center_le (u : Fin 4 → ℤ) (A : Finset (Fin 4 → ℤ)) (M : ℝ) (hM : 1 ≤ M) (hsep : ∀ x ∈ A, ∀ y ∈ A, x ≠ y → M ≤ znorm (x - y)) (X : ℝ) : ↑{x ∈ A | znorm (u - x) ≤ X}.card ≤ 16 * min (↑A.card) ((X / M + 1) ^ 4)

Shell / packing count, paper (5.61), centered form. A set A whose distinct points are M-separated (M ≤ znorm (x - y)) meets the ball {x : znorm (u - x) ≤ X} in at most 16 · min(|A|, (X/M + 1)⁴) points.

Proof: the rounding map x ↦ (fun i => ⌊(xᵢ - uᵢ)/M⌋) is injective on an M-separated set (two points in a common M-grid cell have sup-distance < M) and lands in a box of at most (2X/M + 2)⁴ = 16 (X/M + 1)⁴ cells; combined with the trivial bound ≤ |A|.

theorem Anderson4D.card_shell_le (A : Finset (Fin 4 → ℤ)) (M : ℝ) (hM : 1 ≤ M) (hsep : ∀ x ∈ A, ∀ y ∈ A, x ≠ y → M ≤ znorm (x - y)) (X : ℝ) : ↑{x ∈ A | znorm x ≤ X}.card ≤ 16 * min (↑A.card) ((X / M + 1) ^ 4)

Shell / packing count, paper (5.61) (centered at the origin). Special case of card_ball_center_le with u = 0.

Dyadic-decomposition engine for paper (5.62)

theorem Anderson4D.sum_inv_sq_le : ∃ (C : ℝ), 0 < C ∧ ∀ (A : Finset (Fin 4 → ℤ)) (M : ℝ), 1 ≤ M → (∀ x ∈ A, ∀ y ∈ A, x ≠ y → M ≤ znorm (x - y)) → ∀ (u : Fin 4 → ℤ), ∑ x ∈ A with M ≤ znorm (u - x), (znorm (u - x))⁻¹ ^ 2 ≤ C * √↑A.card * M⁻¹ ^ 2

Single-variable dyadic sum estimate, paper (5.60)/(5.62). For an M-separated set A and any center u, ∑_{x ∈ A, |u-x| ≥ M} |u-x|^{-2} ≲ |A|^{1/2} M^{-2}. The constant is the single-use existential line-constant C = 256·(8/3); |A|^{1/2} is Real.sqrt (A.card).

Bilinear cluster bound (paper (5.58))

theorem Anderson4D.bilinear_cluster_bound_weak : ∃ (C : ℝ), 0 < C ∧ ∀ (A B : Finset (Fin 4 → ℤ)) (M N : ℝ), 1 ≤ M → 1 ≤ N → (∀ x ∈ A, ∀ y ∈ A, x ≠ y → M ≤ znorm (x - y)) → (∀ x ∈ B, ∀ y ∈ B, x ≠ y → N ≤ znorm (x - y)) → ∀ (u : Fin 4 → ℤ), ∑ x ∈ A with M ≤ znorm (u - x), ∑ y ∈ B with max M N ≤ znorm (x - y), (znorm (u - x))⁻¹ ^ 2 * (znorm (x - y))⁻¹ ^ 2 ≤ C * √↑A.card * M⁻¹ ^ 2 * √↑B.card * N⁻¹ ^ 2

Bilinear cluster bound (5.58) — trivial-direction ("weak") form. The bound ∑∑ 𝟙·𝟙·|u-x|^{-2}|x-y|^{-2} ≲ |A|^{1/2}M^{-2}|B|^{1/2}N^{-2} without the refining factor min(1,(Q/P)^{1/4}). Obtained by iterating (5.60) (sum_inv_sq_le): sum in y, then in x. Indicators are represented as Finset.filter; half-powers via Real.sqrt.

Together with the S-bound in LocalRefined.lean, the elementary min-combination gives the complete factor min(1,(Q/P)^{1/4}) in (5.58).