ShellPerturbation #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The stream increment k_m - k_n as a perturbation on y + □_n #
Section 5.1 compares the localized Dirichlet problems for a_n and for a_m,
m ≥ n, by treating k_m - k_n as a perturbation of the coefficient field on
the cube y + □_n. The whole size input for that comparison is the large-scale
event 𝒥(y + □_n, θ) of Translation.lean, which caps the tail sum
Σ_{k ≥ n} 3^{(2-γ) n} ‖∇ j_k‖_{W^{1,∞}(y+□_n)} ≤ θ .
Because the weight is fixed at the cube scale n, a bound on the whole tail is
in particular a bound on the block k ∈ (n, m], uniformly in m. Unfolding
the volume-normalized gauge ‖∇ j‖_{W^{1,∞}(y+□_n)} = max(‖∇²j‖_{L^∞(y+□_n)}, 3^{-n} ‖∇ j‖_{L^∞(y+□_n)}) therefore gives, with no constant at all,
Σ_{k ∈ (n,m]} ‖∇² j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-2) n} ,
Σ_{k ∈ (n,m]} ‖∇ j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-1) n} ,
which are the two displayed bounds of the perturbation step. The 1/2-Hölder
bound follows by the mean value inequality on the convex cube together with the
interpolation [F]_{1/2} ≤ (2 ‖F‖_∞ ‖∇F‖_∞)^{1/2} of HolderCalculus.lean.
The two metrics, and where the dimensional constants come from #
The shell gauges of Section4/Support/ShellNorms.lean are built from the exact
Euclidean-induced sizes matrixDerivativeNorm and matrixSecondDerivativeNorm
of the stored derivatives, whereas supNormOn and holderSeminormOn use the
ambient norm of the derivative carriers Vec d →L[ℝ] Mat d and
Vec d →L[ℝ] (Vec d →L[ℝ] Mat d), whose source is Vec d in the supremum
norm and whose target Mat d carries the entrywise supremum norm. Converting
one into the other costs √d per differentiation, since ‖v‖_∞ ≤ |v|_2 ≤ √d ‖v‖_∞ and the entrywise supremum norm of a matrix is at most its Euclidean
operator norm. That is the entire source of the constants below: the exact
Euclidean statements carry the constant 1, the ambient statements carry √d
for the gradient, d for the Hessian and √2 · d for the Hölder seminorm.
References #
- ABK26, the large-scale good event of Section 5.1 and the perturbation step of the injection estimate.
1. The Euclidean gauges versus the ambient norms #
The entrywise supremum norm of a matrix is at most its Euclidean operator norm.
The gradient conversion: the ambient norm of a stored first derivative is
at most √d times its exact Euclidean induced norm.
The packaged gradient conversion, with the same constant d as the Hessian
conversion below.
The Hessian conversion: the ambient norm of a stored second derivative is
at most d times its exact twice-induced Euclidean norm.
2. The mean value step on a convex set #
The mean value inequality as a Lipschitz (exponent-one Hölder) bound.
On a convex set a uniform bound on the Fréchet derivative is exactly the
two-point bound HolderSeminormBoundOn U 1 L F. The dimensional cost of
converting the derivative bound into the ambient operator norm ‖F' x‖ is
carried by the caller; for the shell carriers it is the factor d of
norm_le_dim_mul_matrixSecondDerivativeNorm.
3. The shell gauges on the translated cube #
The exact Euclidean size of ∇ j at a point of y + □_n is controlled by
the L^∞(y + □_n) gauge of the translated shell.
The exact Euclidean size of ∇² j at a point of y + □_n is controlled by
the L^∞(y + □_n) gauge of the translated shell.
Triangle inequality for the exact Euclidean gradient size over a finite sum of shell fields.
Triangle inequality for the exact Euclidean Hessian size over a finite sum of shell fields.
4. Reading the large-scale event on a block of shells #
The weight 3^{(2-γ) n} of largeScaleEventBase does not run with the
summation index, so a bound on the whole tail k ≥ n restricts to a bound on
any finite block of shells, with no loss and in particular uniformly in the
upper endpoint.
The block form of the large-scale event on y + □_n. On
𝒥(y + □_n, θ) the volume-normalized gauges of any finite block of shells
k ≥ n sum to at most θ 3^{(γ-2) n}.
The Hessian leg of the block bound: Σ ‖∇² j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-2) n}.
The gradient leg of the block bound: Σ ‖∇ j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-1) n}.
The extra factor 3^n is the volume normalization |□_n|^{-1/d} = 3^{-n} that
the gauge divides out of the first-derivative leg.
The increment shell field carries the derivative of k_m - k_n. Its
values are k_m x - k_n x, and the stored first derivative is the genuine
Fréchet derivative of that map, so the bounds below are bounds on
∇(k_m - k_n).
The gradient bound, in the exact Euclidean induced norm and with the
constant 1: ‖Σ_{k ∈ (n,m]} ∇ j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-1) n}, uniformly in
m. The block is empty for m ≤ n, and for n ≤ m the field it sums to is
∇(k_m - k_n) by hasFDerivAt_cutoff_sub.
The Hessian bound, in the exact twice-induced Euclidean norm and with
the constant 1: ‖Σ_{k ∈ (n,m]} ∇² j_k‖_{L^∞(y+□_n)} ≤ θ 3^{(γ-2) n},
uniformly in m. The block is empty for m ≤ n, and for n ≤ m the field it
sums to is ∇²(k_m - k_n).
The gradient bound in the ambient gauge of HolderGauge.lean, with the
dimensional cost √d of the change of metric.
The mean value step on the cube: Σ_{k ∈ (n,m]} ∇ j_k, which is
∇(k_m - k_n) for n ≤ m, is Lipschitz on y + □_n with constant
d · θ · 3^{(γ-2) n}.
The 1/2-Hölder bound of the perturbation step:
[Σ_{k ∈ (n,m]} ∇ j_k]_{C^{0,1/2}(y+□_n)} ≤ √2 · d · θ · 3^{(γ - 3/2) n},
uniformly in m; for n ≤ m the field is ∇(k_m - k_n). The exponent is the
printed one; the constant is the interpolation constant √2 times the
dimensional cost d of the change of metric.