Documentation

LeanPool.Komlos.Grid

Normalised weights on a one-dimensional grid #

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

For N > 0, the integers in [-6 * N, 6 * N] index the points of N⁻¹ • ℤ in [-6, 6]. gridF N is the tent of half-width gridM N = 6 * N, divided by its L² norm. Its square has total mass 1. The L² distance between gridF N and its translate by an integer m is at most |m| / (N * √12).

source
def Komlos.gridM (N : ℕ) :
ℕ

The integer half-width 6 * N corresponding to [-6, 6] at grid spacing 1 / N.

Equations
Instances For
    source
    noncomputable def Komlos.gridZ (N : ℕ) :
    ℝ

    The normalising constant ∑ j, tent (gridM N) j ^ 2.

    Equations
    Instances For
      source
      noncomputable def Komlos.gridF (N : ℕ) (j : ℤ) :
      ℝ

      The normalised one-dimensional weight.

      Equations
      Instances For
        source
        theorem Komlos.cast_gridM (N : ℕ) :
        ↑(gridM N) = 6 * ↑N
        source
        theorem Komlos.gridZ_eq (N : ℕ) :
        gridZ N = 144 * ↑N ^ 3 + 2 * ↑N
        source
        theorem Komlos.gridZ_pos {N : ℕ} (hN : 0 < N) :
        0 < gridZ N
        source
        theorem Komlos.gridF_nonneg (N : ℕ) (j : ℤ) :
        0 ≤ gridF N j
        source
        theorem Komlos.support_gridF_subset (N : ℕ) :
        Function.support (gridF N) ⊆ ↑(Finset.Icc (-↑(gridM N)) ↑(gridM N))
        source
        theorem Komlos.finsum_gridF_sq {N : ℕ} (hN : 0 < N) :
        ∑ᶠ (j : ℤ), gridF N j ^ 2 = 1
        source
        theorem Komlos.sum_gridF_sub_sq {N : ℕ} (hN : 0 < N) (m : ℤ) {K : Finset ℤ} (hK : (Function.support fun (j : ℤ) => gridF N (j - m)) ⊆ ↑K) :
        ∑ j ∈ K, gridF N (j - m) ^ 2 = 1

        gridF N ^ 2 has total mass 1, computed on any Finset containing the support of the translate gridF N (· - m).

        source
        theorem Komlos.sum_gridF_sq {N : ℕ} (hN : 0 < N) {K : Finset ℤ} (hK : Function.support (gridF N) ⊆ ↑K) :
        ∑ j ∈ K, gridF N j ^ 2 = 1
        source
        theorem Komlos.sum_gridF_sub_sq_le {N : ℕ} (hN : 0 < N) (m : ℤ) (K : Finset ℤ) :
        ∑ j ∈ K, (gridF N j - gridF N (j - m)) ^ 2 ≤ ↑m ^ 2 / (12 * ↑N ^ 2)

        The squared L² distance between gridF N and its translate by m is at most m ^ 2 / (12 * N ^ 2).