OneStepSchauderKernelL1 #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Derivative scaling laws for the scaled radial mollifier #
The interior Schauder estimates differentiate the reproducing convolution once (gradient) or twice (Hessian) and move both derivatives onto the kernel. This module supplies the pointwise scaling laws that step rests on:
hasFDerivAt_radialKernelScaled—∇K_ε(z) = ((εᵈ)⁻¹ · ε⁻¹) • ∇K(ε⁻¹ • z);hasFDerivAt_fderiv_radialKernelScaled—D²K_ε(z) = ((εᵈ)⁻¹ · ε⁻¹ · ε⁻¹) • D²K(ε⁻¹ • z);norm_fderiv_fderiv_radialKernelScaled— the second of these read in norm.
Against the ε^d change-of-variables Jacobian of an integration in z, the
(ε^d)⁻¹ of the rescaling cancels, leaving exactly the ε⁻¹ (resp. ε⁻²)
that becomes the 1/r (resp. 1/r²) of the interior estimates.
The derivative of the scaled kernel #
Derivative of the scaled kernel. K_ε(z) = (εᵈ)⁻¹ · radialKernel d (ε⁻¹ • z)
has derivative
((εᵈ)⁻¹ · ε⁻¹) • fderiv radialKernel (ε⁻¹ • z) (const factor times the chain rule for the linear
dilation ε⁻¹ • ·).
Integrability and the L¹ scaling law #
The integrated form of the scaling law is not carried in this module; what is available here is the pointwise identity above.
The second derivative of the scaled kernel #
Second derivative of the scaled kernel. fderiv K_ε = fun w => ((εᵈ)⁻¹·ε⁻¹) • ∇radialKernel(ε⁻¹•w) (from hasFDerivAt_radialKernelScaled), and differentiating that
once more (chain rule for the linear dilation ε⁻¹ • ·) gives D²K_ε(z) = ((εᵈ)⁻¹·ε⁻¹·ε⁻¹) • D²radialKernel (ε⁻¹ • z).
The norm of the scaled kernel's second derivative:
‖D²K_ε(z)‖ = (εᵈ)⁻¹ · ε⁻¹ · ε⁻¹ · ‖D²radialKernel(ε⁻¹•z)‖.
Integrability and the L¹ scaling law #
The integrated form of the scaling law is not carried in this module; what is available here is the pointwise identity above.