Carrier-free analytic core of paper §5.4.3, (5.90)--(5.92).

structure Anderson4D.XYCluster : Type

• points : Finset (Fin 4 → ℤ)
• X : ℝ
• N : ℝ
• X_nonneg : 0 ≤ self.X
• one_le_N : 1 ≤ self.N
• separated (x : Fin 4 → ℤ) : x ∈ self.points → ∀ y ∈ self.points, x ≠ y → self.N ≤ znorm (x - y)

def Anderson4D.XYCluster.Y (c : XYCluster) : ℝ

Equations

• c.Y = ↑c.points.card

def Anderson4D.XYCluster.P (c : XYCluster) : ℝ

Equations

• c.P = c.Y * c.N ^ 4

noncomputable def Anderson4D.XYCluster.lambda (c : XYCluster) (R : ℝ) (skipped : Bool) (u x : Fin 4 → ℤ) : ℝ

Equations

• c.lambda R skipped u x = if skipped = true then R⁻¹ ^ 2 else if c.N ≤ Anderson4D.znorm (u - x) then (Anderson4D.znorm (u - x))⁻¹ ^ 2 else 0

noncomputable def Anderson4D.XYCluster.singleInner (c : XYCluster) (R : ℝ) (skipped : Bool) (u : Fin 4 → ℤ) : ℝ

Equations

• c.singleInner R skipped u = c.X * ∑ x ∈ c.points, c.lambda R skipped u x

noncomputable def Anderson4D.XYCluster.pairInner (a b : XYCluster) (R : ℝ) (skipA skipB : Bool) (u : Fin 4 → ℤ) : ℝ

Equations

• a.pairInner b R skipA skipB u = a.X * b.X * ∑ x ∈ a.points, a.lambda R skipA u x * ∑ y ∈ b.points, b.lambda R skipB x y

theorem Anderson4D.XYCluster.singleInner_le_5_92 (c : XYCluster) (R : ℝ) (skipped : Bool) (u : Fin 4 → ℤ) : c.singleInner R skipped u ≤ c.X * c.Y * if skipped = true then R⁻¹ ^ 2 else c.N⁻¹ ^ 2

Paper (5.92), in the stronger form X_j Y_j · (N_j⁻² or R⁻²).

theorem Anderson4D.XYCluster.pairInner_le_5_90 (a b : XYCluster) (R : ℝ) (skipA skipB : Bool) (u : Fin 4 → ℤ) : a.pairInner b R skipA skipB u ≤ (a.X * a.Y * if skipA = true then R⁻¹ ^ 2 else a.N⁻¹ ^ 2) * (b.X * b.Y * if skipB = true then R⁻¹ ^ 2 else b.N⁻¹ ^ 2)

Paper (5.90), with the printed square-root factors multiplied out.

theorem Anderson4D.XYCluster.pairInner_le_5_91_unskipped : ∃ (C : ℝ), 0 < C ∧ ∀ (a b : XYCluster) (u : Fin 4 → ℤ), a.X * b.X * ∑ x ∈ a.points with a.N ≤ znorm (u - x), ∑ y ∈ b.points with max a.N b.N ≤ znorm (x - y), (znorm (u - x))⁻¹ ^ 2 * (znorm (x - y))⁻¹ ^ 2 ≤ C * a.X * √a.Y * a.N⁻¹ ^ 2 * b.X * √b.Y * b.N⁻¹ ^ 2 * min 1 ((b.P / a.P) ^ (1 / 8))

Unskipped (5.91); Lemma 5.14's 1/4 gain implies the required 1/8.

theorem Anderson4D.XYCluster.innerPi_parity_assembly {ι : Type u_1} [DecidableEq ι] (blocks skipped : Finset ι) (_hsub : skipped ⊆ blocks) (_h20 : skipped.card ≤ 20) (term base gain : ι → ℝ) (hlocal0 : ∀ i ∈ blocks, 0 ≤ term i) (hlocal : ∀ i ∈ blocks, term i ≤ base i * if i ∈ skipped then 1 else gain i) : ∏ i ∈ blocks, term i ≤ (∏ i ∈ blocks, base i) * ∏ i ∈ blocks, if i ∈ skipped then 1 else gain i

One-parity product assembly with at most twenty discarded (5.87) gains.