IterationStep #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
One step of the perturbation iteration on y + □_n #
Section 5.1 compares the solution of the rough-field Dirichlet problem at scale
m with the one at scale n ≤ m by treating k_m - k_n as a perturbation and
iterating. One step of that iteration takes an H¹ function w on y + □_n
with a continuous representative and produces
- the solution
hof the Laplace problem-Δ h = -∇·(w ∇·(k_m - k_n))ony + □_nwith zero boundary values, together with the sup and Hölder bounds its gradient inherits from the boundary Schauder estimate for the Poisson equation in a cube; and - the next iterate
w', the solution of the rough-field problem at scalenwith forcing field∇h.
Both halves are assembled here. The Laplace half is the cube Schauder estimate
Algsuperdiff.Frozen.External.cube_schauder at s = 1/2, unit coefficient and
zero boundary datum, transported from the origin cube to y + □_n; the size of
its right-hand side is the Hölder Leibniz rule of HolderCalculus; the
antisymmetry of the perturbation rewrites the forcing field through
SkewTransfer; and the next iterate exists by DirichletSolvability.
Main results #
exists_isDirichletSolutionAt_laplacian— the Laplace problem ony + □_nwith a1/2-Hölder forcing field, with‖∇h‖_{L^∞} ≤ C 3^{n/2} [G]and[∇h]_{C^{0,1/2}} ≤ C [G].holderSeminormBoundOn_neg_smul— the Leibniz rule in the form the forcing field of the iteration needs.exists_iterationStep— one step of the iteration.contDiff_one_shellIncrement_entry,matTranspose_shellIncrement— the shell incrementk_m - k_nsatisfies the two hypotheses of the step.holderSeminormOn_le_of_mem_goodCubeEvent— on the good cube event the next iterate obeysσ_n 3^{-n/2} [w'] ≤ 2 C_reg 3^{n/2} [∇h].exists_iterationStep_of_mem_goodCubeEvent— the two combined.
References #
- ABK26, the iteration scheme of the proof of Proposition 5.1.
The C^{0,α} bound transports from the origin cube to y + □_n.
A C^{0,α} bound depends on the field only through its values on the set.
The Laplace problem in the cube y + □_n with a 1/2-Hölder forcing
field.
For every G with [G]_{C^{0,1/2}(y+□_n)} ≤ K there is a zero-boundary weak
solution h of -Δ h = ∇·G on y + □_n whose gradient obeys
‖∇h‖_{L^∞(y+□_n)} ≤ C 3^{n/2} K , [∇h]_{C^{0,1/2}(y+□_n)} ≤ C K ,
with C = C(d) independent of the scale, the centre and the forcing field.
This is the boundary Schauder estimate for the Poisson equation in a cube at
s = 1/2, unit coefficient and zero boundary datum, read on y + □_n through
the translation bridge of Translation.lean. The two displayed powers of the
scale are exactly what the frozen estimate produces: its left-hand gauge is
3^{-n/2} ‖∇h‖_{L^∞} + [∇h]_{C^{0,1/2}} and its right-hand side at zero datum
is C 3^{-n/2} · 3^{n/2} K = C K.
3. The size of the forcing field of the iteration #
The Hölder Leibniz rule in the form the iteration needs. The forcing
field of the Laplace step is -w ∇·(k_m - k_n), a scalar field times a vector
field.
4. One step of the iteration #
One step of the perturbation iteration.
Given a skew, entrywise C¹ matrix field k and an H¹ function w on
y + □_n with a continuous representative wRep obeying
[wRep] ≤ Kw and ‖wRep‖_{L^∞} ≤ Sw, and given the two sizes
[∇·k] ≤ Kk, ‖∇·k‖_{L^∞} ≤ Sk of the divergence of the perturbation, the
step produces
h, the zero-boundary solution of-Δ h = -∇·(w ∇·k)ony + □_n, stated in the equivalent antisymmetric form-∇·(k ∇w)that the antisymmetry transfer supplies, with‖∇h‖_{L^∞(y+□_n)} ≤ C 3^{n/2} ([wRep] ‖∇·k‖_∞ + ‖wRep‖_∞ [∇·k]) , [∇h]_{C^{0,1/2}(y+□_n)} ≤ C ([wRep] ‖∇·k‖_∞ + ‖wRep‖_∞ [∇·k]);w', the next iterate: the solution of the rough-field problem at scalenwith forcing field∇h.
C = C(d) is the constant of the cube Schauder estimate; it does not depend on
the scale, the centre, the sample, the perturbation or w.
5. The perturbation of the iteration is the shell increment #
Every entry of the shell increment k_q - k_p is C¹, the first hypothesis
of the iteration step.
The shell increment k_q - k_p is pointwise antisymmetric, the second
hypothesis of the iteration step.
6. The good cube event bounds the next iterate #
On the good cube event the localized regularity is at most 2 C_reg, and
this bounds the next iterate.
σ_n 3^{-n/2} [w']_{C^{0,1/2}(y+□_n)}
≤ 2 C_reg 3^{n/2} [∇h]_{C^{0,1/2}(y+□_n)} .
On the good cube event the next iterate has a continuous representative.
The infimum defining the localized regularity is ⊤ when none exists.
One step of the iteration on the good cube event. The step produces the
Laplace solution h, the next iterate w', a continuous representative of w',
and the estimate of the proof of Proposition 5.1 relating the two.