CubeSchauderFreezing #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
Cube Schauder: the freezing step (harmonic approximation with divergence forcing) #
If u solves -Δ u = ∇·G on a window U and V ⊆ U is an interior sub-domain,
then for any constant vector c the same u solves -Δ u = ∇·(G - c) on
V, because a constant field is weakly divergence free. Solving the zero-trace
problem -Δ w = ∇·(G - c) on V and setting h := u - w produces a weakly
harmonic comparison function on V together with the sharp energy bound
∫_V |∇w|² ≤ ∫_V |G - c|² .
Taking c = G(x₀) for a point x₀ of the sub-cube and using the C^{0,1/2}
bound on G gives the freezing gain: the harmonic approximation error is
controlled by the oscillation of the forcing over the sub-cube, hence by
(side)^{1/2} · [G]_{C^{0,1/2}} rather than by ‖G‖.
This is Armstrong--Kuusi ellipticregularity.tex, the display
e.harmapprox.Schauder (~2660) specialized to a = I_d (where the ‖a - I_d‖_{L^∞} leg vanishes identically), in the development's own carriers.
Main results #
integral_vecDot_const_h10_eq_zero— a constant field pairs to zero against the gradient of a zero-trace test function.isDivFormWeakSolutionOn_sub_const— the equation is invariant under subtracting a constant from the forcing.exists_h10_isDivFormWeakSolutionOn_one— the zero-trace solution of-Δ w = ∇·Fon an arbitrary open bounded convex domain.dirichletEnergy_le_of_isDivFormWeakSolutionOn_one— the sharp energy bound∫|∇w|² ≤ ∫|F|²for the zero-trace solution.exists_frozenHarmonicReplacement— the freezing step on an arbitrary open bounded convex domain.exists_frozenHarmonicReplacement_openCubeSet— the freezing step at a triadic sub-cube of a window, with the oscillation bound made explicit:∫_{□} |∇w|² ≤ d · KG² · 3^{Q.scale} · |□|.
References #
- ABK26;
Algsuperdiff/Frozen/External/CubeSchauder.lean. - Armstrong--Kuusi, Elliptic Regularity (
ellipticregularity.tex), Propositionsp.Schauder.Calphaandp.Schauder.C1alpha.
1. The identity background #
The identity coefficient field drops out of the flux pairing.
-Δ u = ∇·g in the development's carrier, unfolded at the identity background.
The identity is the unit diffusivity.
2. A constant field is weakly divergence free #
A constant field pairs to zero against zero-trace gradients. This is the
weak statement ∇ · c = 0 for a constant vector c, and it is the algebraic
heart of the freezing step.
Freezing invariance of the equation. Subtracting a constant from the forcing does not change the divergence-form weak equation.
3. Zero-trace solvability and the sharp energy bound #
The zero-datum comparator exists on any open bounded convex domain. For
F ∈ L²(U) there is w ∈ H¹₀(U) with -Δ w = ∇·F weakly.
The Dirichlet energy of an H¹ function is integrable on its domain.
The squared Euclidean length of an L² field is integrable.
The sharp zero-trace energy bound. A zero-trace weak solution of
-Δ w = ∇·F has Dirichlet energy at most the L² energy of the forcing.
The proof tests the equation with w itself and applies Young's inequality
|ξ·η| ≤ |ξ|²/2 + |η|²/2 pointwise; the balanced split reproduces the sharp
constant 1.
4. The freezing step #
The freezing step (harmonic approximation with divergence forcing).
Let u solve -Δ u = ∇·G weakly on an open bounded convex domain U and let
c be an arbitrary constant vector. Then there is w ∈ H¹₀(U) with
-Δ w = ∇·(G - c)weakly onU,u - wweakly harmonic onU, and∫_U |∇w|² ≤ ∫_U |G - c|².
With c := G(x₀) the right side is the squared L² oscillation of the forcing,
which is the freezing gain of the Schauder argument.
5. The freezing gain on a triadic sub-cube #
The sup-norm diameter of a triadic cube is its side length.
The Euclidean square length is at most d times the squared sup norm.
The pointwise oscillation bound produced by a C^{0,1/2} forcing on a cube.