LatticeCover #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The scale-k lattice tiling of cu_m, and the shell gauge it dominates #
ABK26, Section 4.1, the two Step-2 budget displays. Both perform the same
unremarked move: a shell norm read on the annulus cube z + cu_n (with z a
scale-n lattice point) is replaced by the maximum of the W^{2,infinity}
shell gauge over the scale-k lattice cubes of cu_m -- the very family the
good event Support.eventG1's second condition, and the frozen clause-(i)
fourth term, are written with.
Support.GaugeBridge's scope note records that this "lattice-max enlargement"
is NOT proved there (only the same-centre cube-scale comparison is).
Recorded here, because it fixes the route taken below: the naive reading --
first enlarge z + cu_n to z + cu_k at the same centre by
Support.shellW1InfGradNorm_le_zpow_mul_of_le, then look for a scale-k
lattice cube of cu_m containing the enlarged cube -- does NOT close. For
k > n and z at the outer edge of the annulus the enlarged cube leaves
cu_m: z = 3^n v with |z_i| <= (3^m - 3^n)/2 only gives
|z_i| + 3^k/2 <= 3^m/2 + (3^k - 3^n)/2, which exceeds 3^m/2 as soon as
k > n.
This module proves the move by the other route, which needs no enlargement:
- the annulus cube stays inside the observation cube --
translate_openCubeSet_originCube_subset:z + cu_nis contained incu_m(openly) for every scale-nlattice pointzofcu_m; and - the scale-
klattice cubes tilecu_min CoarseGraining's half-open realizationcubeSet--exists_mem_latticeCubeSet_sub_mem_cubeSet.
Only the half-open tiling is exact, so a point of z + cu_n may land on a
tile face, which the open-cube sup gauges of the shell layer do not see.
The gap is closed by continuity: the frozen ShellField carries continuous
first and second derivatives, so the sup over an open triadic cube already
bounds the value at every point of its half-open closure
(..._le_localCubeSecondDerivNorm_cubeSet and its two siblings).
Main results #
exists_mem_latticeCubeSet_sub_mem_cubeSet-- the tiling.translate_openCubeSet_originCube_subset-- the containment.shellW2InfLatticeMaxOf-- the lattice maximum ofDisplaySlots, read at an abstract shell field.shellW1InfGradNorm_translate_le_shellW2InfLatticeMaxOf-- the enlargement at theW^{1,infinity}gauge, at the honest factormax 1 3^{k-n}.localCubeControl_translate_le_shellW2InfLatticeMaxOf-- the same at theL^infinityvalue gauge, at the factor3^{2k}.localCubeControl_le_of_forallandlocalCubeControl_sum_le-- the two missing pieces of the provedCutoff.localCubeControlA (its minimality characterization and its layer-sum triangle inequality), re-proved here because the in-repo versions areprivate/ absent. They are what makes the value leg available at all.
References #
- ABK26,
p.mathcalE.annular.decompStep 2. - ABK26,
d.good.event.for.lambda, (the3^k Z^d ∩ cu_mfamily).
Part A -- the half-open tiling of cu_m by scale-k lattice cubes #
The scale-k lattice cubes tile cu_m.
Every point of the open cube cu_m lies in the half-open realization
cubeSet of exactly one scale-k lattice cube 3^k w + cu_k with
w ∈ 3^k Z^d ∩ cu_m -- the index family of the good event's second condition
and of the frozen clause-(i) fourth term. The index is the coordinatewise
rounding w_i = floor(x_i 3^{-k} + 1/2), and it stays inside the balanced box
because 3^{m-k} is odd.
Part B -- the open-cube sup gauges see the half-open closure #
The second-derivative gauge of a shell dominates the exact induced norm at every point of the half-open triadic cube, not only the open one: the frozen shell carrier stores a continuous second derivative.
The first-derivative gauge, at every point of the half-open cube.
The value gauge, at every point of the half-open cube.
A nonnegative pointwise bound controls the value gauge.
The layer-sum triangle inequality at the value gauge, the L^infinity
analogue of Support.shellW1InfGradNorm_translate_sum_le.
Part C -- the annulus cube stays inside the observation cube #
z + cu_n is contained in cu_m for every scale-n lattice point z
of cu_m and every n <= m. The containment is in the open cube on both
sides: z is a lattice point, so |z_i| <= (3^m - 3^n)/2 exactly.
Part D -- the lattice-max enlargement at the two shell gauges #
DisplaySlots.shellW2InfLatticeMax, read at an abstract shell field: the
maximum of the W^{2,infinity} gauge over 3^k Z^d ∩ cu_m.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The enlargement at the second-derivative leg.
The enlargement at the first-derivative leg.
The enlargement at the value leg.
The lattice-max enlargement of the W^{1,infinity} shell gauge: the gauge
of a shell on the annulus cube z + cu_n is at most max(1, 3^{k-n}) times
the maximum of its W^{2,infinity} gauge over the scale-k lattice cubes of
cu_m, for every k <= m.