LocalizationOverlapCount

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Provider: the bounded-overlap count for the meso windows

Source displays in ABK26:

• e.nablaw.oscillations (label; display) is stated at a mesh point z in 3^n Zd cap cu_K and involves the outer window z + cu_{m-h}, of side 3^{m-h}, which is much larger than the mesh spacing 3^n;
• e.lower.bound.oscillations (label; display) averages the resulting quantity over the whole mesh z in 3^n Zd cap cu_K.

Because the window scale m - h exceeds the mesh scale n, the windows z + cu_{m-h} attached to distinct mesh points overlap. The tiling identity cubeAverage_originCube_eq_mesoGridAverage of LocalizationGrid is a partition statement about the scale-n tiles z + cu_n and says nothing about the windows. This module supplies the missing combinatorial input: the exact multiplicity of the overlapping window family.

What is proved

Write N = m - h - n for the gap, so the window at the site z is z + cu_{n+N} = openCubeAtScale z (n + N), and let I be any finite family of scale-n triadic cubes, each contributing the window based at its own site z = triadicCubeShift R.

• card_filter_mem_openCubeAtScale_le -- the overlap count. For every point x, the number of members of I whose window contains x is at most (3^N)^d. The proof is one-dimensional and exact: a window contains x iff the cube's i-th index lies in an open real interval of length exactly 3^N, and such an interval contains at most 3^N integers.
• sum_indicator_openCubeAtScale_le -- the same statement as a pointwise bound on the sum of the window indicators, which is the form the integral transfer consumes. Since it is stated at an arbitrary finite family of scale-n cubes, it applies verbatim to the meso grid and to the interior meso grid of LocalizationGrid, whose members all have scale n by construction.

Divergences from the printed statement

• The count below is proved for any finite family of cubes of a common scale, so it covers mesoCubeGrid, interiorMesoCubeGrid and any subfamily of either.
• The count is not clipped to cu_K. The bound (3^N)^d is the full lattice multiplicity; restricting the family to cu_K can only decrease it. It is also the exact multiplicity, since (3^N)^d scale-n cubes can have windows sharing a common point, so the volume-normalized transfer constant produced from it (module LocalizationOverlapTransfer) cannot be improved by sharpening the count. That sharpness is a remark about the lattice, not a theorem of this module.
• Nothing here is an average. This module is pure counting; the passage from the count to a normalized average, including the interior-grid deficit, is the separate module LocalizationOverlapTransfer.

The one-dimensional interval of admissible indices

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.overlapWindowArg {d : ℕ} (x : HCPolySupport.Vec d) (n : ℤ) (N : ℕ) (i : Fin d) : ℝ

The right endpoint of the open interval of admissible i-th indices: a cube of scale n and i-th index k has its window z + cu_{n+N} containing x in the i-th coordinate exactly when k lies in (overlapWindowArg x n N i - 3^N, overlapWindowArg x n N i).

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.overlapWindowArg x n N i = x i / 3 ^ n + 3 ^ N / 2

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.overlapIndexBox {d : ℕ} (x : HCPolySupport.Vec d) (n : ℤ) (N : ℕ) (i : Fin d) : Finset ℤ

The integer box containing every admissible i-th index.

Equations

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

The overlap count

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.card_filter_mem_openCubeAtScale_le {d : ℕ} (x : HCPolySupport.Vec d) (n : ℤ) (N : ℕ) {I : Finset (HCPolySupport.TriadicCube d)} (hI : ∀ R ∈ I, R.scale = n) : {R ∈ I | x ∈ HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N)}.card ≤ (3 ^ N) ^ d

The bounded-overlap count for the meso windows.

For a finite family I of triadic cubes all of scale n, and for the windows z + cu_{n+N} based at the sites z = triadicCubeShift R, every point of space lies in at most (3^N)^d of the windows. This is the multiplicity that the manuscript's passage from e.nablaw.in.L.eight to e.lower.bound.oscillations needs and does not state.

: the caller supplies hI, the common-scale property of the family; it is discharged for the development's grids by scale_eq_of_mem_mesoCubeGrid.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sum_indicator_openCubeAtScale_le {d : ℕ} (x : HCPolySupport.Vec d) (n : ℤ) (N : ℕ) {I : Finset (HCPolySupport.TriadicCube d)} (hI : ∀ R ∈ I, R.scale = n) : ∑ R ∈ I, (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N)).indicator (fun (x : HCPolySupport.Vec d) => 1) x ≤ (3 ^ N) ^ d

The overlap count in indicator form. This is the shape the integral transfer consumes: the sum of the window indicators is bounded by the pure multiplicity (3^N)^d, uniformly in the point.

: the caller supplies hI, as in card_filter_mem_openCubeAtScale_le.