A distribution with small shift distance

Adapted for Lean Pool by changing module paths and selecting explicit imports.

Lemma 1.5 of Karingula–Lovett: for each grid N⁻¹ • ℤ ^ d, there is a finitely supported probability distribution in [-6, 6] ^ d with mean zero and shift distance at most 1 / 3 under every grid translation of Euclidean norm at most 1.

The distribution is the image of cubeP d N under coordinatewise division by N.

noncomputable def Komlos.gridEmb (d N : ℕ) : (Fin d → ℤ) →+ Fin d → ℝ

The scaling g ↦ g / N from the integer lattice to the grid N⁻¹ • ℤ ^ d.

Equations

• Komlos.gridEmb d N = { toFun := fun (g : Fin d → ℤ) (k : Fin d) => ↑(g k) / ↑N, map_zero' := ⋯, map_add' := ⋯ }

@[simp]

theorem Komlos.gridEmb_apply (d N : ℕ) (g : Fin d → ℤ) (k : Fin d) : (gridEmb d N) g k = ↑(g k) / ↑N

theorem Komlos.gridEmb_injective {d N : ℕ} (hN : 0 < N) : Function.Injective ⇑(gridEmb d N)

@[simp]

theorem Komlos.gridF_neg (N : ℕ) (j : ℤ) : gridF N (-j) = gridF N j

@[simp]

theorem Komlos.cubeF_neg (d N : ℕ) (g : Fin d → ℤ) : cubeF d N (-g) = cubeF d N g

theorem Komlos.cubeP_neg (d N : ℕ) (g : Fin d → ℤ) : (cubeP d N) (-g) = (cubeP d N) g

theorem Komlos.sum_smul_eq_zero_of_neg {E : Type u_1} {F : Type u_2} [AddCommGroup E] [AddCommGroup F] [Module ℝ F] (f : E →+ F) {P : E →₀ ℝ} (hP : ∀ (x : E), P (-x) = P x) : (P.sum fun (x : E) (r : ℝ) => r • f x) = 0

A symmetric distribution has mean zero after pushing forward along any additive map.

theorem Komlos.exists_nearInvariant {d N : ℕ} (hN : 0 < N) : ∃ (P : (Fin d → ℝ) →₀ ℝ), IsDist P ∧ mean P = 0 ∧ (∀ x ∈ P.support, ‖x‖ ≤ 6) ∧ ∀ (g : Fin d → ℤ), ∑ k : Fin d, (↑(g k) / ↑N) ^ 2 ≤ 1 → shiftDist P ((gridEmb d N) g) ≤ 3⁻¹

Lemma 1.5: a probability distribution in [-6, 6] ^ d with mean zero and shift distance at most 1 / 3 for every grid vector of Euclidean norm at most 1.