CubeSchauderAeSlopeDefect #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: the slope-defect inequality of the a.e. identification #
The master inequality of the a.e. identification Ψ = ∇w. Fix a base point
z ∈ □_m and a scale j small enough that the Euclidean ball of radius 3^j/2
around z sits inside □_m, and let η = campanatoCutoff z j. For an
arbitrary affine competitor ℓ = (c,g) and an arbitrary reference vector v,
|g_i − v_i| · ∫_{□_m} η
≤ |∫_{□_m} (∂_i u − g_i) η| + ∫_{□_m} |∂_i u − v_i| η
≤ C(d)·3^{-j}·‖u − ℓ‖_{L²(W_j)}·|W_j| + ∫_{W_j} |∂_i u − v_i| ,
with W_j = (z+□_j) ∩ □_m. Both right-hand terms are localized: the first is
C(d)·K·√(3^j)·|W_j| at the affine minimizer under the Campanato datum, and the
second is |W_j| times the oscillation average of ∂_i u around v on the
window. The left factor is bounded below by
(3^j/(8(d+1)))^d = |euclideanBall z (3^j/8)|'s own lower bound, because η = 1
there.
Taking v = ∇u(z) at a Lebesgue point of ∇u and letting j → −∞ therefore
forces g_i → (∇u)_i(z), i.e. Ψ(z) = ∇u(z). That last limit is not taken
here: this module supplies the deterministic inequality only, and the Lebesgue
differentiation step remains the open residue.
References #
- ABK26.
1. The cutoff has a definite mass #
The cutoff's mass. ∫_{□_m} η ≥ (3^j/(8(d+1)))^d, because η = 1 on
the Euclidean ball of radius 3^j/8 and that ball sits inside □_m.
2. Integrability of the two cutoff pairings #
3. The slope-defect inequality #
The slope-defect inequality.
For any affine competitor ℓ = (c,g) and any reference vector v, the defect
|g_i − v_i|, weighted by the cutoff's mass, is controlled by the cutoff
pairing bound plus the oscillation of ∂_i u around v_i on the window. Both
right-hand terms are localized to W_j = (z+□_j) ∩ □_m.