CubeSchauderAeIbp #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: the integration-by-parts step of the a.e. identification #
For the smooth cutoff η = campanatoCutoff z j supported inside □_m, the weak
gradient identity of u ∈ H¹(□_m) and the same identity for the smooth affine
competitor ℓ = (c,g) combine into
∫_{□_m} (∂_i u − g_i)·η = −∫_{□_m} (u − ℓ)·∂_i η ,
and the right-hand side is bounded by ‖∂_i η‖_∞ · ∫_{W_j} |u − ℓ|, because
∂_i η vanishes off the Euclidean ball of radius 3^j/2, which sits inside the
window W_j = (z+□_j) ∩ □_m. The L¹ ≤ L² comparison of
CubeSchauderAeCutoff then converts the last integral into the window's own
L² distance to ℓ:
|∫_{□_m} (∂_i u − g_i)·η| ≤ C(d)·3^{-j} · ‖u − ℓ‖_{L²(W_j)} · |W_j| .
At the affine minimizer of W_j the middle factor is the unnormalized excess,
so the Campanato datum E(u, W_j) ≤ K√(3^j) turns the bound into
C(d)·K·√(3^j)·|W_j|.
References #
- ABK26.
1. The affine competitor is smooth #
2. Continuity and compact support of the cutoff derivative #
3. The integration-by-parts identity #
The cutoff pairing identity.
The weak gradient identity of u, minus the classical one for the smooth affine
competitor ℓ = (c,g). No hypothesis beyond the support condition on the
cutoff.
4. The bound #
The cutoff pairing bound.
|∫_{□_m} (∂_i u − g_i) η| ≤ C(d)·3^{-j}·‖u − ℓ‖_{L²(W_j)}·|W_j|, for every
affine competitor ℓ = (c,g).