LatticeHolder #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
A Hölder seminorm bound on the whole cube from lattice oscillation decay #
This file composes the two halves of the passage from a scale-by-scale oscillation estimate on a cube to a Hölder seminorm on the same cube:
- the off-grid transfer, which moves the centre from the lattice to an arbitrary
point of the cube at the price
clipScaleStepConstant d αand the loss of one triadic scale; - the clipped Campanato telescope and its convex chaining, which turn oscillation decay at every centre into a two-point Hölder bound for the canonical representative.
Because the windows are clipped to the cube, the conclusion holds up to the boundary: no interior sub-cube is involved and no boundary term is created.
Every constant is written out. The composed price is
clipOffGridHolderConstant d α N = N ^ (1 - α) · clipLocalHolderConstant d α · (clipScaleStepConstant d α) ^ 2,
with N the number of chaining steps, and the conclusion is the bound
clipOffGridHolderConstant d α N · K on the C^{0,α} seminorm of the
representative on the whole cube, where K is the constant of the lattice
family.
The concrete instance is the cube y + □_m against a lattice family on its own
clipped windows. One triadic scale is spent — the enclosing lattice window of
an off-lattice centre is one scale up — so the Campanato decay reaches half-side
3 ^ (m-1) / 2, the telescope's top radius is 3 ^ (m-2) / 2, and the chain
length is N = 18, both scale constraints being exact equalities.
Main definitions #
clipOffGridHolderConstant d α N— the composed explicit constant.
Main results #
holderSeminormBoundOn_cube_of_grid— the wrapper on an arbitrary cube, withRandNfree.holderSeminormBoundOn_cubeSetAt_of_grid— the concrete two-point instance ony + □_m, atN = 18.continuousOn_campanatoRepresentative_of_grid,campanatoRepresentative_ae_eq_of_grid— the representative produced is continuous on the cube and agrees withfalmost everywhere on it.cubeSetAt_eq_ball— the dictionary between the cube of the underlying scale range and the supremum ball.
1. The composed constant #
The composed explicit constant of the passage from a lattice oscillation
family on the clipped windows of a cube to a Hölder seminorm on that cube: the
chaining price N ^ (1 - α), the two-point bound, and the two triadic steps —
one for the passage from the discrete scales to all radii, one for the off-grid
transfer.
Equations
- One or more equations did not get rendered due to their size.
Instances For
2. The wrapper #
The Campanato decay at every centre of the cube, from lattice decay.
The Hölder seminorm bound on the whole cube, from lattice decay. The
lattice family is available at the admissible centres from index j₀ on; the
off-grid transfer then supplies every centre of the cube from index j₀ + 1 on,
and the telescope of top radius R — constrained by
3 R ≤ triadicRadius Rtop (j₀ + 1) — is chained across the cube in N steps,
where N is constrained by 2 Rm ≤ N R.
The representative produced by the wrapper is continuous on the cube.
The representative produced by the wrapper is a representative of f.
3. The cube of the underlying scale range #
The cube y + □_n is the supremum ball of radius 3 ^ n / 2 at y.
4. The concrete instance #
The concrete instance on y + □_m. The lattice family lives on the
windows clipped to y + □_m itself, so no scale is spent on fitting a lattice
window inside the cube; the single triadic scale spent is the one the off-grid
transfer costs. Both scale constraints are exact equalities:
3 R = 3 ^ (m-1) / 2 is the top radius of the transferred Campanato family, and
18 R = 3 ^ m is the diameter of the cube.
The concrete instance at the concrete family of lattice centres. The approximation hypothesis is discharged by rounding toward the centre of the cube, so the only remaining inputs are the oscillation estimate at the lattice centres and square integrability on the cube.