GridCoverage

Ported from scottnarmstrong/CoarseGraining at c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4. Module imports, support namespace and local option directives adapted for Lean Pool.

Discrete uniform-grid corridor coverage count

Phase comparison (Prop 4.4 of the high-moment paper, Armstrong–Kuusi–Loher, in preparation) is proved with the continuum σ-average replaced by a finite uniform grid gridPhase ℓ N j i = (j i) · ℓ / N for j : Fin d → Fin N. This file records the elementary grid-counting coverage bound that replaces the continuum corridor-coverage estimate e.corridor.coverage:

• card_gridHits_le (1-d heart): for 4 ≤ ℓ and ℓ ≤ N, at most 3N/ℓ of the N grid points c ↦ c·ℓ/N land within (sup-)distance 1 of a fixed real t modulo ℓ. The bound is via an injection of the admissible grid indices into the integer points of an open interval of length 2N/ℓ.
• sum_indicator_gridPhase_corridor_le (d-dim corollary): for a fixed x, the number of grid phases σ_j whose corridor set contains x, summed as indicators over Finset.univ : Finset (Fin d → Fin N), is at most (3d/ℓ)·N^d; i.e. the average of the corridor indicators over the grid is at most 3d/ℓ.

Only 4 ≤ ℓ and ℓ ≤ N are used; the constant 3 is not sharp (any C·N/ℓ is acceptable, absorbed into C_d downstream).

noncomputable def HCPolySupport.gridPhase {d : ℕ} (ℓ : ℝ) (N : ℕ) (j : Fin d → Fin N) : Vec d

The finite uniform phase grid: gridPhase ℓ N j is the phase vector with i-th coordinate (j i)·ℓ/N.

Equations

• HCPolySupport.gridPhase ℓ N j i = ↑↑(j i) * ℓ / ↑N

@[simp]

theorem HCPolySupport.gridPhase_apply {d : ℕ} (ℓ : ℝ) (N : ℕ) (j : Fin d → Fin N) (i : Fin d) : gridPhase ℓ N j i = ↑↑(j i) * ℓ / ↑N

1-d heart

theorem HCPolySupport.card_gridHits_le {ℓ : ℝ} (hℓ : 4 ≤ ℓ) {N : ℕ} (hN : ℓ ≤ ↑N) (t : ℝ) : ↑{c : Fin N | ∃ (n : ℤ), |t - ↑↑c * ℓ / ↑N - ↑n * ℓ| < 1}.card ≤ 3 * ↑N / ℓ

M0 (1-d count). For 4 ≤ ℓ and ℓ ≤ N, at most 3N/ℓ of the grid points c ↦ c·ℓ/N, c : Fin N, lie within sup-distance 1 of t modulo the lattice ℓ·ℤ.

d-dim corollary

theorem HCPolySupport.sum_indicator_gridPhase_corridor_le {d : ℕ} [NeZero d] {ℓ : ℝ} (hℓ : 4 ≤ ℓ) {N : ℕ} (hN : ℓ ≤ ↑N) (x : Vec d) : ∑ j : Fin d → Fin N, (corridorSet ℓ (gridPhase ℓ N j)).indicator (fun (x : Vec d) => 1) x ≤ 3 * ↑d / ℓ * ↑N ^ d

M0 (d-dim coverage). For a fixed x and 4 ≤ ℓ ≤ N, the sum over the finite grid j : Fin d → Fin N of the corridor indicators of the phases gridPhase ℓ N j at x is at most (3d/ℓ)·N^d. Dividing by N^d, the grid average of 𝟙_{corridorSet} at any point is at most 3d/ℓ.