The sharp critical Green-square convolution

This file turns the shell-counting engine into the four-dimensional logarithmic convolution estimate. The proof splits the lattice into the two endpoint regions and the residual region where both endpoints are large.

def Anderson4D.natAddIciEquiv (N : ℕ) : ℕ ≃ ↑(Set.Ici N)

Translation identifies ℕ with the natural-number tail above N.

Equations

• Anderson4D.natAddIciEquiv N = { toFun := fun (j : ℕ) => ⟨j + N, ⋯⟩, invFun := fun (n : ↑(Set.Ici N)) => ↑n - N, left_inv := ⋯, right_inv := ⋯ }

noncomputable def Anderson4D.z4EighthRadialTail (N : ℕ) (k : Z4) : ℝ

Eighth-order radial mass outside the integral sup-radius N.

Equations

• Anderson4D.z4EighthRadialTail N k = if N ≤ Anderson4D.z4SupRadius k then Anderson4D.l2LatticeRadialWeight 8 k else 0

theorem Anderson4D.summable_z4EighthRadialTail (N : ℕ) : Summable (z4EighthRadialTail N)

theorem Anderson4D.summable_scalar_fifth_shell_major : Summable fun (n : ℕ) => 80 * (↑(n + 1))⁻¹ ^ 5

theorem Anderson4D.tsum_z4EighthRadialTail_le (N : ℕ) (hN : 0 < N) : ∑' (k : Z4), z4EighthRadialTail N k ≤ 20 * (↑N)⁻¹ ^ 4

noncomputable def Anderson4D.z4FourthCubeMass (R : ℕ) (k : Z4) : ℝ

Fourth-order radial mass truncated to a finite sup-norm cube.

Equations

• Anderson4D.z4FourthCubeMass R k = if k ∈ Anderson4D.z4Cube R then Anderson4D.l2LatticeRadialWeight 4 k else 0

theorem Anderson4D.summable_z4FourthCubeMass (R : ℕ) : Summable (z4FourthCubeMass R)

theorem Anderson4D.tsum_z4FourthCubeMass (R : ℕ) : ∑' (k : Z4), z4FourthCubeMass R k = ∑ k ∈ z4Cube R, l2LatticeRadialWeight 4 k

theorem Anderson4D.z4SupRadius_triangle (α γ : Z4) : z4SupRadius γ ≤ z4SupRadius α + z4SupRadius (γ - α)

Integral sup radius obeys the triangle inequality under the convolution decomposition γ = α + (γ - α).

theorem Anderson4D.inv_pow_four_le_sixteen_inv_pow_four {B G : ℝ} (hB : 0 < B) (hG : 0 < G) (hGB : G ≤ 2 * B) : (B ^ 4)⁻¹ ≤ 16 * (G ^ 4)⁻¹

theorem Anderson4D.inv_pow_four_mul_le_inv_pow_eight {A B : ℝ} (hA : 0 < A) (hAB : A ≤ B) : (A ^ 4)⁻¹ * (B ^ 4)⁻¹ ≤ (A ^ 8)⁻¹

theorem Anderson4D.l2LatticeRadialWeight_four_near_le (α γ : Z4) (hnear : 2 * z4SupRadius α ≤ z4SupRadius γ) : l2LatticeRadialWeight 4 (γ - α) ≤ 16 * l2LatticeRadialWeight 4 γ

theorem Anderson4D.l2LatticeRadialWeight_four_mul_le_eight_of_radius_le (k l : Z4) (hkl : z4SupRadius k ≤ z4SupRadius l) : l2LatticeRadialWeight 4 k * l2LatticeRadialWeight 4 l ≤ l2LatticeRadialWeight 8 k

theorem Anderson4D.z4FourthCubeMass_nonneg (R : ℕ) (k : Z4) : 0 ≤ z4FourthCubeMass R k

theorem Anderson4D.z4EighthRadialTail_nonneg (N : ℕ) (k : Z4) : 0 ≤ z4EighthRadialTail N k

noncomputable def Anderson4D.criticalRadialConvolutionMajor (γ α : Z4) : ℝ

A single summable majorant simultaneously covering the two endpoint regions and the residual region of the critical convolution.

Equations

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

theorem Anderson4D.summable_criticalRadialConvolutionMajor (γ : Z4) : Summable (criticalRadialConvolutionMajor γ)

theorem Anderson4D.l2LatticeRadialConvolution_term_le_criticalMajor (γ α : Z4) : l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α) ≤ criticalRadialConvolutionMajor γ α

noncomputable def Anderson4D.z4SupCriticalWeight (γ : Z4) : ℝ

The sup-radius form of the critical weight.

Equations

• Anderson4D.z4SupCriticalWeight γ = Anderson4D.l2LatticeRadialWeight 4 γ * (1 + Real.log ↑(Anderson4D.z4SupRadius γ + 1))

theorem Anderson4D.z4SupCriticalWeight_nonneg (γ : Z4) : 0 ≤ z4SupCriticalWeight γ

theorem Anderson4D.tsum_criticalRadialConvolutionMajor_le (γ : Z4) : ∑' (α : Z4), criticalRadialConvolutionMajor γ α ≤ 3200 * z4SupCriticalWeight γ

theorem Anderson4D.tsum_l2LatticeRadialConvolution_le_critical (γ : Z4) : ∑' (α : Z4), l2LatticeRadialWeight 4 α * l2LatticeRadialWeight 4 (γ - α) ≤ 3200 * z4SupCriticalWeight γ

theorem Anderson4D.z4FrequencyNorm_le_norm_z4EuclideanFrequency (k : Z4) : z4FrequencyNorm k ≤ ‖z4EuclideanFrequency k‖

theorem Anderson4D.designJapaneseBracket_sq (k : Z4) : designJapaneseBracket k ^ 2 = 1 + ‖z4EuclideanFrequency k‖ ^ 2

theorem Anderson4D.norm_z4EuclideanFrequency_le_designJapaneseBracket (k : Z4) : ‖z4EuclideanFrequency k‖ ≤ designJapaneseBracket k

theorem Anderson4D.designJapaneseBracket_le_two_mul_supBracket (k : Z4) : designJapaneseBracket k ≤ 2 * ↑(z4SupRadius k + 1)

theorem Anderson4D.supBracket_le_two_mul_designJapaneseBracket (k : Z4) : ↑(z4SupRadius k + 1) ≤ 2 * designJapaneseBracket k

theorem Anderson4D.z4SupCriticalWeight_le_designCriticalHSWeight (γ : Z4) : z4SupCriticalWeight γ ≤ 32 * designCriticalHSWeight γ

theorem Anderson4D.tsum_greenL2SquaredConvolutionSummand_le_critical (γ : Z4) : ∑' (α : Z4), greenL2SquaredConvolutionSummand γ α ≤ 1638400 * designCriticalHSWeight γ

theorem Anderson4D.exists_positive_criticalGreenSquaredConvolutionEstimate : ∃ (C : ℝ), 0 < C ∧ CriticalGreenSquaredConvolutionEstimate C

The scalar critical estimate required by the conditioned Hilbert--Schmidt theorem is unconditional.