Refined bilinear lattice-cluster bound (Lemma 5.14 of arXiv:2607.10105, eq. (5.58))

Paper: L-5.14 — (5.58) — the refined bilinear lattice bound

This file completes the PAPER_MAP node L-5.14: the bilinear cluster bound (5.58) with the refining factor min (1, (Q/P)^{1/4}), P = |A|·M⁴, Q = |B|·N⁴.

Contents:

• single_y_bound — the pointwise (in y) estimate, paper (5.63)/(5.64);
• bilinear_cluster_S_bound — the Q ≤ P (S-)bound ∑∑ ≲ |A|^{1/4} M⁻³ |B|^{3/4} N⁻¹, paper (5.65)–(5.67);
• bilinear_cluster_bound — the fully refined (5.58), combining the S-bound with bilinear_cluster_bound_weak from Anderson4D.PermSum.Local.

Quarter powers are Real.rpow (· ^ (1/4 : ℝ)); indicator constraints are Finset.filter; constants are explicit in private lemmas and existential in the two public theorems. The dyadic engine of Local.lean is private there, so the small parametric geometric-sum lemmas are (re)proved here in ratio-generic form.

rpow helpers for quarter powers

Dyadic bracketing and per-term bounds (threshold-T versions)

The three cases of the pointwise estimate (5.63)

theorem Anderson4D.single_y_bound (A : Finset (Fin 4 → ℤ)) (M N : ℝ) (hM : 1 ≤ M) (hsep : ∀ x ∈ A, ∀ y ∈ A, x ≠ y → M ≤ znorm (x - y)) (u y : Fin 4 → ℤ) : ∑ x ∈ A with M ≤ znorm (u - x) ∧ max M N ≤ znorm (x - y), (znorm (u - x))⁻¹ ^ 2 * (znorm (x - y))⁻¹ ^ 2 ≤ 524288 * M⁻¹ ^ 4 * (1 + (↑A.card * M ^ 4) ^ (1 / 4) / max (znorm (u - y)) (max M N))

Pointwise (in y) bilinear estimate, paper (5.63). For M-separated A (M ≥ 1), any u, y and any N, ∑_{x ∈ A, |u-x| ≥ M, |x-y| ≥ max(M,N)} |u-x|⁻²|x-y|⁻² ≤ 524288·M⁻⁴·(1 + P^{1/4}/max(|u-y|, M, N)) with P = |A|·M⁴.

Stage 2: summation in y, small-y case (paper (5.66)–(5.67))

theorem Anderson4D.S_bound_smallcases (A B : Finset (Fin 4 → ℤ)) (M N : ℝ) (hM : 1 ≤ M) (hN : 1 ≤ N) (hsepB : ∀ x ∈ B, ∀ y ∈ B, x ≠ y → N ≤ znorm (x - y)) (u : Fin 4 → ℤ) (hQP : ↑B.card * N ^ 4 ≤ ↑A.card * M ^ 4) : ∑ y ∈ B with znorm (u - y) ≤ max M N, 524288 * M⁻¹ ^ 4 * (1 + (↑A.card * M ^ 4) ^ (1 / 4) / max (znorm (u - y)) (max M N)) ≤ 48 * 524288 * (↑A.card ^ (1 / 4) * M⁻¹ ^ 3 * ↑B.card ^ (3 / 4) * N⁻¹)

Stage 2 (paper (5.66)–(5.67)). Summing the pointwise bound (5.63) over the y with max(|u-y|, M, N) = max(M, N), under Q ≤ P, meets the S-target |A|^{1/4}·M⁻³·|B|^{3/4}·N⁻¹.

Stage 3: summation in y, case max = |u-y| (paper (5.65))

theorem Anderson4D.S_bound_largecase (A B : Finset (Fin 4 → ℤ)) (M N : ℝ) (hM : 1 ≤ M) (hN : 1 ≤ N) (hsepB : ∀ x ∈ B, ∀ y ∈ B, x ≠ y → N ≤ znorm (x - y)) (u : Fin 4 → ℤ) (hQP : ↑B.card * N ^ 4 ≤ ↑A.card * M ^ 4) : ∑ y ∈ B with ¬znorm (u - y) ≤ max M N, 524288 * M⁻¹ ^ 4 * (1 + (↑A.card * M ^ 4) ^ (1 / 4) / max (znorm (u - y)) (max M N)) ≤ 257 * 524288 * (↑A.card ^ (1 / 4) * M⁻¹ ^ 3 * ↑B.card ^ (3 / 4) * N⁻¹)

Stage 3 (paper (5.65)). Summing the pointwise bound (5.63) over the y with max(|u-y|, M, N) = |u-y|, under Q ≤ P, meets the S-target.

Stage 4: assembly of the refined (5.58)

theorem Anderson4D.bilinear_cluster_S_bound : ∃ (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 → ℤ), ↑B.card * N ^ 4 ≤ ↑A.card * M ^ 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 ^ (1 / 4) * M⁻¹ ^ 3 * ↑B.card ^ (3 / 4) * N⁻¹

Bilinear cluster S-bound (the Q ≤ P case of (5.58)). For M-separated A, N-separated B, M, N ≥ 1, any u, under Q = |B|N⁴ ≤ P = |A|M⁴: ∑∑ 𝟙·𝟙·|u-x|⁻²|x-y|⁻² ≤ C·|A|^{1/4}·M⁻³·|B|^{3/4}·N⁻¹.

theorem Anderson4D.bilinear_cluster_bound : ∃ (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 * min 1 ((↑B.card * N ^ 4 / (↑A.card * M ^ 4)) ^ (1 / 4))

Refined bilinear cluster bound, paper (5.58) (Lemma 5.14). For M-separated A, N-separated B (M, N ≥ 1) and any u, ∑∑ 𝟙_{|u-x| ≥ M}·𝟙_{|x-y| ≥ max(M,N)}·|u-x|⁻²|x-y|⁻² ≤ C·|A|^{1/2}M⁻²·|B|^{1/2}N⁻²·min(1, (Q/P)^{1/4}), P = |A|M⁴, Q = |B|N⁴ (with Lean's x/0 = 0 convention when A = ∅).