SeriesIdentification #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The iteration series converges in H¹₀ and sums to the solution for the perturbed field #
Section 5.1 computes the solution of -∇·a_m∇u = ∇·g on y + □_n by an
iteration that starts from the solution w_0 for the background field a_n and
whose increments solve
-∇·a_n ∇w_{j+1} = ∇·( (a_m - a_n) ∇w_j ) in y + □_n , w_{j+1} = 0 on the boundary.
The manuscript asserts u_m = Σ_j w_j "provided that we can establish the
convergence of the series" and does not establish it: the contraction it proves
is in C^{0,1/2}, which by itself does not identify a limit as a weak solution.
This module supplies the missing step in the norm in which the weak formulation
is continuous.
The telescoped identity. Write kap := a_m - a_n and S_J := Σ_{j ≤ J} w_j.
Adding the weak equations of w_0, …, w_J gives
∫ a_n ∇S_J · ∇φ = -∫ g · ∇φ - ∫ (kap ∇S_{J-1}) · ∇φ ,
and adding ∫ (kap ∇S_J)·∇φ to both sides collapses the sum to its last term:
∫ a_m ∇S_J · ∇φ = -∫ (g - kap ∇w_J) · ∇φ .
So S_J solves the problem for a_m with the original datum g up to the
single remainder -kap ∇w_J, and the difference u - S_J of any solution u
for a_m at datum g and the partial sum solves the problem for a_m at datum
kap ∇w_J.
The remainder vanishes. The energy estimate applied to that difference gives
lam_m ‖∇(u - S_J)‖_{L²} ≤ d ‖kap ∇w_J‖_{L²} ≤ d² (Lam_n + Lam_m) ‖∇w_J‖_{L²} ,
so the remainder is measured in L² (equivalently, the forcing functional it
carries has H⁻¹ size at most d times that L² norm), and it tends to zero
as soon as the iterates' energies do. The per-step constant is bad — it depends
on the molecular diffusivity through lam_m and on the scale through the volume
of the cube — but it does not depend on the step index, so a geometric decay of
the data of the steps is enough. That decay is exactly what the C^{0,1/2}
contraction supplies through the supremum bound on the data of the iteration.
References #
- ABK26, the iteration scheme of the proof of the
L^∞injection estimate.
1. Finite sums of Sobolev witnesses #
The gradient of a finite sum is the sum of the gradients.
The partial sum Σ_{j ≤ J} w_j of the iteration.
Equations
- Algsuperdiff.Section5.Support.iterationPartialSum w J = ∑ j ∈ Finset.range (J + 1), w j
Instances For
2. From the Laplace step to the perturbation datum #
The two halves of one iteration step compose. If h solves the
Laplace problem with datum -k ∇v and the next iterate solves the background
problem with datum ∇h, then the next iterate solves the background problem
with datum k ∇v directly. This is the step that removes the auxiliary
Laplace solution from the recursion.
3. The telescoped weak formulation #
The partial sum solves the background problem with the accumulated forcing.
The telescoped weak formulation. Against the perturbed field the whole accumulated forcing collapses to the original datum minus the action of the perturbation on the gradient of the last iterate.
The remainder problem. Any solution for the perturbed field at the original datum differs from the partial sum by the solution at the single remainder datum.
4. The remainder vanishes #
The quantitative remainder bound. The distance from the partial sum to any solution for the perturbed field is controlled, in the energy norm, by the energy of the last iterate.
The partial sums converge to the solution in the energy norm.
The value of the difference is controlled by its energy: a solution and a partial sum both vanish on the boundary, so their difference is a zero-trace function and the Poincaré inequality applies.
The partial sums converge to the solution in value as well.
5. Geometric decay of the energies of the iterates #
One step of the iteration, in the energy norm: the energy of an iterate is controlled by the supremum size of its datum on the cube.
The energies of the iterates tend to zero when the data of the steps decay geometrically in the supremum norm on the cube.
6. The cutoff coefficient fields of the model #
The coefficient field at scale m is the field at scale n perturbed by
the difference of the two cutoff shell sums; no order relation between the
scales is used.
Every solution for the coefficient field at scale m is the limit of the
partial sums of the iteration, in gradient and in value. The limit is the
same for every solution, so any two solutions of that Dirichlet problem agree
almost everywhere on the cube, in value and in gradient.