LocalizedErrorScaling #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The localized error read at a datum that is not normalized #
The localized error E(y+□_n) is a supremum over the normalized forcing class
[g]_{W^{1/2,∞}(y+□_n)} ≤ 1, so on its own it says nothing about a solution
whose datum is not normalized. The localized Dirichlet problem is homogeneous of
degree one in the pair (solution, datum), so the bound transfers to an arbitrary
datum of finite Hölder seminorm at the cost of the factor
3^{n/2} [g]_{C^{0,1/2}(y+□_n)}. This is the companion, for the essential
supremum, of localizedRegularity_apply_general.
The degenerate branch [g] = 0 is not a limiting case of the scaling: the datum
is then constant on the cube, both solutions vanish almost everywhere by the
uniqueness of the localized problem, and the essential supremum of their
difference vanishes outright.
Main results #
eLpNorm_top_sub_le_localizedError— the homogeneous form.eLpNorm_top_sub_le_of_mem_goodCubeEvent— its reading on the good cube event, where the localized error is at mostε.
References #
- ABK26, the localized error of Section 5.1 and the triangle inequality closing the injection estimate.
1. The degenerate branch #
A datum of vanishing Hölder seminorm forces the solution to vanish. On the cube the datum is then constant, a constant datum pairs to zero against every zero-trace gradient, and the almost-everywhere uniqueness of the localized problem identifies the solution with zero.
2. The homogeneous form #
The localized error bounds every pair of solutions, normalized or not.
For a datum g of finite 1/2-Hölder seminorm on y + □_n, a rough-field
solution u and a comparator solution v with that datum,
σ_n 3^{-n} ‖u - v‖_{L^∞(y+□_n)}
≤ E(y+□_n) · 3^{n/2} [g]_{C^{0,1/2}(y+□_n)} .
The reading on the good cube event.