CubeSchauderAeLimit #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: the Lebesgue-point limit of the a.e. identification #
CubeSchauderAeSlopeDefect.abs_slope_sub_le_cutoff_split is the deterministic
inequality behind the almost-everywhere identification Ψ = ∇w. This module
takes the limit and delivers the identification itself.
Fix a base point x ∈ □_m and a scale j small enough that the Euclidean ball
of radius 3^j/2 around x sits inside □_m — the open cube is open, so every
j below a threshold j₀(x) qualifies. Feeding the canonical minimizer of the
window W_j = (x+□_j) ∩ □_m into the slope-defect inequality and dividing by
the cutoff mass gives the one-scale defect bound
|∇ℓ(u,W_j)_i − ∂_i u(x)|
≤ (8(d+1))^d · ( C_ibp(d)·K·√(3^j)
+ ⨍_{B(x,3^j/2)} |∂_i u − ∂_i u(x)| ) ,
where the average is taken over the sup-metric ball, i.e. over the cube of
side 3^j centred at x, and ∂_i u is read through its zero extension off
□_m. Both scale factors cancel exactly: |W_j| ≤ (3^j)^d and the cutoff mass
is at least (3^j)^d/(8(d+1))^d.
Letting j = (m+1) − n run to −∞ kills the first term geometrically and the
second term at every Lebesgue point of the zero extension. Since
CubeSchauderPointwise.tendsto_windowSlope sends ∇ℓ(u,W_j) → Ψ(x), the two
limits identify Ψ(x) with ∇u(x) at almost every x, coordinate by
coordinate.
The Lebesgue points come from the Besicovitch Vitali family of the Lebesgue
measure on Vec d = Fin d → ℝ, whose closed balls are the sup-metric cubes;
the volume identity |B(x,r)| = (2r)^d is the product-measure formula. No
doubling constant and no covering constant enter the statement: the sup-metric
ball is the window's own enclosing cube.
Main results #
exists_zpow_euclideanBall_subset— the interior thresholdj₀(x).gradIndicator— the zero extension of∂_i uoff□_m.abs_windowSlope_sub_grad_le— the one-scale defect bound.ae_campanatoSlopeLimit_eq_grad— the residuehae: at everyK ≥ 0carrying the Campanato datum on all of□_m, the limit slope field agrees with the weak gradient almost everywhere.
References #
- ABK26.
1. The sup-metric ball #
The Euclidean ball sits inside the sup-metric ball of the same radius.
The interior threshold. Around a point of the open cube every sufficiently small Euclidean ball stays inside the cube.
The truncated window sits inside the sup-metric closed ball of radius
3^j/2, i.e. inside the closed cube of side 3^j about the base point.
The sup-metric closed ball has finite volume.
The sup-metric ball's set integral in average form.
∫_{B(x,r)} f = (2r)^d · ⨍_{B(x,r)} f.
2. The zero extension of the weak gradient #
The zero extension of the i-th coordinate of the weak gradient off □_m.
Extending is what makes the Lebesgue differentiation theorem — a statement about
globally integrable functions — available at every interior base point.
Equations
- Algsuperdiff.Section4.Provider.Schauder.gradIndicator m u i = (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)).indicator fun (y : HCPolySupport.Vec d) => u.grad y i
Instances For
The Lebesgue points of the extended gradient. At almost every point of
Vec d the sup-metric averages of |∂_i u − ∂_i u(x)| vanish, simultaneously in
every coordinate. This is the Besicovitch Vitali family of the Lebesgue measure
on Fin d → ℝ, whose closed balls are the sup-metric cubes.
3. The one-scale defect bound #
The one-scale defect bound.
At an interior scale — one whose Euclidean ball of radius 3^j/2 still fits
inside □_m — the coordinate defect between the window slope and the pointwise
gradient value is controlled by the Campanato datum plus one sup-metric
oscillation average. The window's own volume factor cancels against the cutoff
mass floor, leaving the pure d-constant aeLimitConst d.
4. The limit #
The triadic scale sequence 3^{T−n} tends to 0.
The triadic radius sequence tends to 0 from the right.
The a.e. identification Ψ = ∇u.
Off the Campanato datum on all of □_m — the residue hE of
CubeSchauderAssembly — the limit slope field of the Campanato iteration agrees
with the weak gradient of u almost everywhere on the cube. This is the second
named residue hae of zeroDatumCubeSchauder_of_residues, discharged.