Sup-norm to Euclidean-norm bridge on the four-dimensional lattice

The discrete Hepp-tree estimates use znorm, mathlib's sup norm on Fin 4 → ℝ, while the paper's unqualified lattice norm may be read as the Euclidean norm. This file makes the finite-dimensional equivalence explicit. In particular, the Euclidean fourth-order bracket is bounded by the sup-norm bracket used in Proposition 5.6, and conversely with the sharp dimension-four loss 16.

def Anderson4D.zEuclideanNormSq (x : LatticePoint) : ℝ

Squared Euclidean norm of an integer four-vector.

Equations

• Anderson4D.zEuclideanNormSq x = ∑ i : Fin 4, ↑(x i) ^ 2

theorem Anderson4D.zEuclideanNormSq_nonneg (x : LatticePoint) : 0 ≤ zEuclideanNormSq x

theorem Anderson4D.znorm_sq_le_zEuclideanNormSq (x : LatticePoint) : znorm x ^ 2 ≤ zEuclideanNormSq x

The sup norm squared is no larger than the Euclidean norm squared.

theorem Anderson4D.zEuclideanNormSq_le_four_mul_znorm_sq (x : LatticePoint) : zEuclideanNormSq x ≤ 4 * znorm x ^ 2

In four dimensions the Euclidean norm squared is at most four times the sup norm squared.

noncomputable def Anderson4D.zEuclideanNorm (x : LatticePoint) : ℝ

Euclidean norm of an integer four-vector.

Equations

• Anderson4D.zEuclideanNorm x = √(Anderson4D.zEuclideanNormSq x)

theorem Anderson4D.znorm_le_zEuclideanNorm (x : LatticePoint) : znorm x ≤ zEuclideanNorm x

theorem Anderson4D.zEuclideanNorm_le_two_mul_znorm (x : LatticePoint) : zEuclideanNorm x ≤ 2 * znorm x

noncomputable def Anderson4D.latticeEuclideanBracketInvFourth (x₀ x₁ : LatticePoint) : ℝ

Euclidean reading of the fourth-order bracket in paper (5.14).

Equations

• Anderson4D.latticeEuclideanBracketInvFourth x₀ x₁ = ((1 + Anderson4D.zEuclideanNormSq (x₀ - x₁)) ^ 2)⁻¹

theorem Anderson4D.latticeEuclideanBracketInvFourth_nonneg (x₀ x₁ : LatticePoint) : 0 ≤ latticeEuclideanBracketInvFourth x₀ x₁

theorem Anderson4D.latticeEuclideanBracketInvFourth_le_latticeBracketInvFourth (x₀ x₁ : LatticePoint) : latticeEuclideanBracketInvFourth x₀ x₁ ≤ latticeBracketInvFourth x₀ x₁

The Euclidean bracket is pointwise no larger than the sup-norm bracket already controlled by Proposition 5.6.

theorem Anderson4D.latticeBracketInvFourth_le_sixteen_mul_euclidean (x₀ x₁ : LatticePoint) : latticeBracketInvFourth x₀ x₁ ≤ 16 * latticeEuclideanBracketInvFourth x₀ x₁

Reverse bracket comparison. The factor is 2⁴ = 16, exactly the dimension-four norm-equivalence loss.