Sup-norm shells for the critical four-dimensional lattice convolution

This file supplies the discrete counting engine for the sharp logarithmic Green-square convolution. Frequencies are grouped by their exact integral sup radius. A shell has cubic cardinality, so its fourth-order mass is harmonic and its eighth-order tail is summable with fourth-order decay.

def Anderson4D.z4SupRadius (k : Z4) : ℕ

Integral sup radius of a four-dimensional lattice frequency.

Equations

• Anderson4D.z4SupRadius k = Finset.univ.sup fun (i : Fin Anderson4D.dim) => (k i).natAbs

theorem Anderson4D.z4SupRadius_eq_z4FrequencyNorm (k : Z4) : ↑(z4SupRadius k) = z4FrequencyNorm k

theorem Anderson4D.mem_z4Cube_iff_z4SupRadius_le (n : ℕ) (k : Z4) : k ∈ z4Cube n ↔ z4SupRadius k ≤ n

noncomputable def Anderson4D.z4SupShell : ℕ → Finset Z4

Exact integral sup-radius shell.

Equations

• Anderson4D.z4SupShell 0 = Anderson4D.z4Cube 0
• Anderson4D.z4SupShell n.succ = Anderson4D.z4Cube (n + 1) \ Anderson4D.z4Cube n

@[simp]

theorem Anderson4D.mem_z4SupShell (n : ℕ) (k : Z4) : k ∈ z4SupShell n ↔ z4SupRadius k = n

theorem Anderson4D.card_z4Cube (n : ℕ) : (z4Cube n).card = (2 * n + 1) ^ 4

theorem Anderson4D.z4Cube_mono {m n : ℕ} (hmn : m ≤ n) : z4Cube m ⊆ z4Cube n

theorem Anderson4D.card_z4SupShell (n : ℕ) : (z4SupShell n).card = if n = 0 then 1 else (2 * n + 1) ^ 4 - (2 * n - 1) ^ 4

theorem Anderson4D.card_z4SupShell_le (n : ℕ) : (z4SupShell n).card ≤ 80 * (n + 1) ^ 3

Cubic shell count, with a generous explicit constant.

theorem Anderson4D.l2LatticeRadialWeight_eq_z4SupRadius (q : ℕ) (k : Z4) : l2LatticeRadialWeight q k = ((1 + ↑(z4SupRadius k)) ^ q)⁻¹

theorem Anderson4D.sum_z4Cube_l2LatticeRadialWeight_four_le (N : ℕ) : ∑ k ∈ z4Cube N, l2LatticeRadialWeight 4 k ≤ 80 * ∑ n ∈ Finset.range (N + 1), (↑(n + 1))⁻¹

Fourth-order mass in a finite cube is bounded by the corresponding harmonic shell sum.

theorem Anderson4D.sum_z4Cube_l2LatticeRadialWeight_four_le_log (N : ℕ) : ∑ k ∈ z4Cube N, l2LatticeRadialWeight 4 k ≤ 80 * (1 + Real.log (↑N + 1))

Logarithmic form of the finite fourth-order shell bound.

def Anderson4D.z4SupRadiusFiberEquiv (n : ℕ) : { k : Z4 // z4SupRadius k = n } ≃ ↥(z4SupShell n)

The fibre of the integral sup radius is the corresponding finite shell.

Equations

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

theorem Anderson4D.tsum_z4SupRadius_fiber_eq_sum_shell (f : Z4 → ℝ) (n : ℕ) : ∑' (k : { k : Z4 // z4SupRadius k = n }), f ↑k = ∑ k ∈ z4SupShell n, f k

def Anderson4D.z4SupRadiusPreimageEquiv (n : ℕ) : ↑(z4SupRadius ⁻¹' {n}) ≃ { k : Z4 // z4SupRadius k = n }

Equations

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

theorem Anderson4D.tsum_z4SupRadius_preimage_eq_sum_shell (f : Z4 → ℝ) (n : ℕ) : ∑' (k : ↑(z4SupRadius ⁻¹' {n})), f ↑k = ∑ k ∈ z4SupShell n, f k

theorem Anderson4D.tsum_eq_tsum_z4SupShell (f : Z4 → ℝ) (hf : Summable f) : ∑' (k : Z4), f k = ∑' (n : ℕ), ∑ k ∈ z4SupShell n, f k

Regroup a summable nonnegative lattice series by its exact sup radius.

theorem Anderson4D.l2LatticeRadialWeight_eight_le_five (k : Z4) : l2LatticeRadialWeight 8 k ≤ l2LatticeRadialWeight 5 k

theorem Anderson4D.summable_l2LatticeRadialWeight_eight : Summable (l2LatticeRadialWeight 8)

theorem Anderson4D.sum_z4SupShell_l2LatticeRadialWeight_eight_le (n : ℕ) : ∑ k ∈ z4SupShell n, l2LatticeRadialWeight 8 k ≤ 80 * (↑(n + 1))⁻¹ ^ 5

One eighth-order shell has fifth-order residual decay after its cubic cardinality is paid.

theorem Anderson4D.inv_pow_five_eq_rpow_neg_five {x : ℝ} : x⁻¹ ^ 5 = x ^ (-5)

theorem Anderson4D.tsum_inv_nat_add_pow_five_le (N : ℕ) (hN : 0 < N) : ∑' (j : ℕ), (↑(j + N + 1))⁻¹ ^ 5 ≤ 4⁻¹ * (↑N)⁻¹ ^ 4

Explicit integral-test tail for the fifth-order scalar series.