HomCGFinalSmoothTest #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The smooth-test approximation of a Hölder field #
What this file supplies #
The second half of the second "absent analytic input": mollification of the
McShane extension of HomCGFinalExtend, preserving the sup bound and the
Hölder bound EXACTLY (no constant is paid), and converging back to the original
field on the set where the data lives.
For a mollifier density ψ (the IsMollifierDensity, i.e. a smooth
compactly supported probability density) and a globally α-Hölder, globally
sup-bounded field G, the coordinatewise convolution convolutionVec ψ G of
HomMollifySwap satisfies
‖(G ⋆ ψ)(x)‖ ≤ B, [G ⋆ ψ]_{C^{0,α}(ℝ^d)} ≤ K, ‖(G ⋆ ψ)(x) - G(x)‖ ≤ K r^{α}
whenever ‖G‖ ≤ B, [G]_{C^{0,α}} ≤ K and supp ψ ⊆ closedBall 0 r. The
first two are the mass-one superposition principle: writing the convolution in
its swapped form ∫ G(x-t) ψ(t) dt, each estimate holds under the integral and
∫ψ = 1 carries it through. All three are constant-free; only the mollifier's
radius enters, and only in the third.
cgSmoothApprox composes this with the McShane extension: for a field φ that
is sup-bounded by K_sup and α-Hölder by K_Höl on A alone, it
produces a sequence of GLOBALLY C^∞ fields obeying the same two bounds
globally and converging to φ pointwise on A. That is exactly the test-class
input the smooth dual needs.
1. The swapped form of the coordinatewise convolution #
(G ⋆ ψ)(x)_i = ∫ G(x - t)_i ψ(t) dt.
2. The sup bound survives #
3. The Hölder bound survives #
[G ⋆ ψ]_{C^{0,α}} ≤ K whenever [G]_{C^{0,α}} ≤ K on all of Vec d.
4. The mollification is smooth #
G ⋆ ψ is globally C^∞.
5. The mollification converges back #
‖G ⋆ ψ - G‖ ≤ K r^{α} when ψ is supported in the closed ball of
radius r.
6. The mollifier radii of mollifyBump #
The normalized bump of radius 1/(k+1) is supported in that closed ball.
The mollifier radii tend to zero at every positive Hölder exponent.
7. The composed smooth approximation #
The smooth approximation of a field that is Hölder on A alone.
McShane extension, then mollification at radius 1/(k+1).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The approximation is globally C^∞.
The approximation obeys the sup bound of the data, everywhere.
The approximation obeys the Hölder bound of the data, everywhere.
The approximation converges to the data on A.