A product distribution on the integer lattice

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

Komlos.cubeP d N is the product of d copies of the probability weight gridF N ^ 2. Correlations of its square root factor over the coordinates. Combining this factorisation with Komlos.sum_gridF_sub_sq_le and Weierstrass' product inequality gives

shiftDist (cubeP d N) h ^ 2 ≤ (∑ k, (h k / N) ^ 2) / 12.

noncomputable def Komlos.cubeF (d N : ℕ) (g : Fin d → ℤ) : ℝ

The d-dimensional product weight on the integer grid.

Equations

• Komlos.cubeF d N g = ∏ k : Fin d, Komlos.gridF N (g k)

theorem Komlos.support_cubeF_sub_subset {d N : ℕ} {a : Fin d → ℤ} {K : Finset ℤ} (hK : ∀ (k : Fin d), (Function.support fun (j : ℤ) => gridF N (j - a k)) ⊆ ↑K) : (Function.support fun (g : Fin d → ℤ) => cubeF d N (g - a)) ⊆ ↑(Fintype.piFinset fun (x : Fin d) => K)

theorem Komlos.support_cubeF_subset {d N : ℕ} {K : Finset ℤ} (hK : Function.support (gridF N) ⊆ ↑K) : Function.support (cubeF d N) ⊆ ↑(Fintype.piFinset fun (x : Fin d) => K)

noncomputable def Komlos.cubeP (d N : ℕ) : (Fin d → ℤ) →₀ ℝ

The probability weight cubeF d N g ^ 2 on the integer lattice, normalised for N > 0.

Equations

• Komlos.cubeP d N = Finsupp.onFinset (Fintype.piFinset fun (x : Fin d) => Finset.Icc (-↑(Komlos.gridM N)) ↑(Komlos.gridM N)) (fun (g : Fin d → ℤ) => Komlos.cubeF d N g ^ 2) ⋯

@[simp]

theorem Komlos.cubeP_apply (d N : ℕ) (g : Fin d → ℤ) : (cubeP d N) g = cubeF d N g ^ 2

theorem Komlos.support_cubeP_subset {d N : ℕ} {K : Finset ℤ} (hK : Function.support (gridF N) ⊆ ↑K) : (cubeP d N).support ⊆ Fintype.piFinset fun (x : Fin d) => K

theorem Komlos.sum_cubeF_sub_mul_cubeF_sub (d N : ℕ) (K : Finset ℤ) (a b : Fin d → ℤ) : ∑ g ∈ Fintype.piFinset fun (x : Fin d) => K, cubeF d N (g - a) * cubeF d N (g - b) = ∏ k : Fin d, ∑ j ∈ K, gridF N (j - a k) * gridF N (j - b k)

The correlation of two translates of cubeF is the product of their coordinate correlations.

theorem Komlos.sum_cubeF_sub_sq {d N : ℕ} (hN : 0 < N) (a : Fin d → ℤ) {K : Finset ℤ} (hK : ∀ (k : Fin d), (Function.support fun (j : ℤ) => gridF N (j - a k)) ⊆ ↑K) : ∑ g ∈ Fintype.piFinset fun (x : Fin d) => K, cubeF d N (g - a) ^ 2 = 1

theorem Komlos.cubeP_isDist {d N : ℕ} (hN : 0 < N) : IsDist (cubeP d N)

noncomputable def Komlos.shiftBox {d : ℕ} (N : ℕ) (h : Fin d → ℤ) : Finset ℤ

A Finset containing the supports of gridF N and of its translates by every h k.

Equations

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

theorem Komlos.support_gridF_subset_shiftBox {d : ℕ} (N : ℕ) (h : Fin d → ℤ) : Function.support (gridF N) ⊆ ↑(shiftBox N h)

theorem Komlos.support_gridF_sub_subset_shiftBox {d : ℕ} (N : ℕ) (h : Fin d → ℤ) (k : Fin d) : (Function.support fun (j : ℤ) => gridF N (j - h k)) ⊆ ↑(shiftBox N h)

theorem Komlos.shiftDist_cubeP_sq_le {d N : ℕ} (hN : 0 < N) (h : Fin d → ℤ) : shiftDist (cubeP d N) h ^ 2 ≤ (∑ k : Fin d, (↑(h k) / ↑N) ^ 2) / 12

The squared shift distance of cubeP is at most (∑ k, (h k / N) ^ 2) / 12.