OneStepSchauderInteriorHess #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The interior Hessian estimate and the gradient-Lipschitz estimate #
The analytic apex of the interior half of the Schauder gradient-Hölder estimate. For u
harmonic on ball x R and 0 < r < R,
‖D²u(p)‖ ≤ C(d) · r⁻¹ · r⁻¹ · √(msd_{B(x,r)}(u, c)) for every p ∈ B(x, r/2),
for every constant c (the deviation is measured against an arbitrary
constant, which is what later lets the estimate be taken to the infimum over
affine competitors). The convex mean-value inequality on B(x, r/2) then gives
the gradient-Lipschitz form
‖∇u(y) − ∇u(z)‖ ≤ C(d) · r⁻¹ · r⁻¹ · √(msd_{B(x,r)}(u, c)) · ‖y − z‖ .
The route: differentiate the reproducing convolution twice, bound the kernel
Hessian by its sup (ε^{d+2})⁻¹ · B, integrate |u−c|, upgrade ∫|·| to
√(vol · ∫(·)²) by Cauchy–Schwarz, and convert the Haar ball volume by
Measure.addHaar_ball. The inner-ball version re-centres at p ∈ B(x, r/2)
with radii r/4 < r/2 and pays 2^d for enlarging the averaging ball.
Instance caches for the Euclidean and Hessian carriers #
The base carrier EuclideanSpace ℝ (Fin d), the gradient carrier
EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ and the Hessian carrier
EuclideanSpace ℝ (Fin d) →L[ℝ] EuclideanSpace ℝ (Fin d) →L[ℝ] ℝ are searched
hundreds of times while elaborating this file (measured: 82 MeasureSpace,
75 Module, 63 NormedSpace closed top-level searches on the base carrier
alone). Caching the recurring classes once at module level — outside the
section, so that every declaration sees them — turns each search into a single
step. Every cache below is literally the instance Lean would otherwise
rediscover, so no definitional content changes.
A sup bound for the unit-kernel Hessian #
Sup bound for the second derivative of a compactly supported C³ function. Stated for an
abstract f so that the compact support of the real-valued norm function z ↦ ‖D²f z‖ is routed
through the tsupport-subset chain: the tower-valued HasCompactSupport.fderiv blows up whnf on
the iterated continuous-linear-map type (the same pitfall documented at
KernelHessL1.integrable_norm_fderivSq_of).
The Hessian of the unit radial kernel is bounded: it is continuous with compact support.
The core L¹ Hessian bound #
Core L¹ interior Hessian bound. For a globally-C² function w harmonic on ball x₀ ρ
with 2ε ≤ ρ, the second derivative at the centre is bounded by (ε^{d+2})⁻¹·B times the L¹ norm
of w on ball x₀ (2ε), where B bounds the unit-kernel Hessian.
Proof: differentiate the native reproducing convolution twice (as in
norm_fderiv_fderiv_le_of_harmonic_bound), then bound the kernel factor pointwise by its sup
‖D²K_ε(t)‖ ≤ (ε^d)⁻¹·ε⁻¹·ε⁻¹·B = (ε^{d+2})⁻¹·B and integrate |w| (as in
norm_fderiv_le_L1_of_harmonic) — the L¹-on-the-data / sup-on-the-kernel split, which is what
makes the subsequent Cauchy–Schwarz upgrade to an L² deviation possible.
Ball-volume and coefficient algebra #
The centre L² Hessian estimate #
Interior Hessian estimate, L²-deviation shape (native), at the centre.
For u harmonic (mathlib sense) on B(x, R) and any inner radius 0 < r < R,
the Hessian at the centre is bounded by C·r⁻² times the square root of the
mean-square deviation of u on B(x, r) (measured on the corresponding
CoarseGraining Euclidean ball — the §4.3 excess), for any constant c.
This is the exact second-order analogue of interiorGradientEstimateL2; the explicit constant is
B·ω·2^{d+2}, with B the sup of the unit-kernel Hessian and ω = vol(B(0,1)).
The uniform inner-ball L² Hessian estimate #
Interior Hessian estimate, L²-deviation shape (native), uniformly on the half-radius ball.
For u harmonic on B(x, R) and 0 < r < R, the Hessian is bounded by C·r⁻²·√msd at every
point of B(x, r/2), with the mean-square deviation still measured on the fixed outer ball
B(x, r).
Proof: apply the centre estimate interiorSecondDerivEstimateL2 re-centred at y with radii
r/4 < r/2 (legitimate since B(y, r/2) ⊆ B(x, R)), then enlarge the averaging ball from
B(y, r/4) to B(x, r): the integral only grows (the integrand is nonnegative) while the
normalizing volume shrinks by 4^{-d}, so msd_{B(y,r/4)} ≤ 4^d · msd_{B(x,r)} and the square root
costs a factor 2^d. The explicit constant is 16·C·2^d with C the centre constant.
The gradient-Lipschitz consequence #
Interior gradient-Lipschitz estimate from the L² deviation (native). For u harmonic on
B(x, R) and 0 < r < R, the gradient of u is Lipschitz on the half-radius ball B(x, r/2) with
constant C·r⁻²·√( msd_{B(x,r)}(u, c) ):
‖∇u(y) − ∇u(z)‖ ≤ C·r⁻¹·r⁻¹·√( msd_{B(x,r)}(u, c) ) · ‖y − z‖ for y, z ∈ B(x, r/2).
This is the convex mean-value inequality Convex.norm_image_sub_le_of_norm_fderiv_le applied to the
C¹ map fderiv ℝ u on the convex set B(x, r/2), with the derivative bound supplied by
interiorSecondDerivEstimateL2_ball. Differentiability of fderiv ℝ u on the ball comes from the
C² regularity contained in HarmonicAt.