SkewTransfer #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The antisymmetry transfer for a variable skew field #
ABK26's iteration scheme for the injection estimate of Section 5.1 solves, at each step,
-Δ h_j = -∇ · ( w_j ∇ · (k_m - k_n) ) in □_n , h_j = 0 on ∂□_n ,
and then rewrites the right side, "using that k_m - k_n is anti-symmetric", as
∇ · ( w ∇ · k ) = ∇w · (∇ · k) = ∇ · ( k ∇w ) .
The manuscript states the display and does not prove it. This module supplies the argument, as an identity of the two weak forcings and then as an equivalence of the two Dirichlet problems.
The divergence convention #
matFieldDiv k contracts the first index,
(∇ · k)_j = ∑_i ∂_i k_{i j} ,
which is the convention under which the printed display is literally true: it is
the same contraction that turns a ∇u into ∇ · a ∇u in the divergence-form
equation. With the opposite (row) contraction both sides of the display change
sign, so the convention is not cosmetic; it is the one fixed for the maps
Vec d → Mat d of this file.
The mathematics #
Write the difference of the two forcings against a test function φ and expand
the product rule inside one integration by parts:
∑_{i,j} ∂_i ( k_{i j} · w · ∂_j φ )
= ∑_{i,j} (∂_i k_{i j}) w ∂_j φ + ∑_{i,j} k_{i j} (∂_i w) ∂_j φ
+ ∑_{i,j} k_{i j} w ∂_i ∂_j φ .
The left side integrates to zero (a compactly supported field), the last sum
vanishes pointwise because a skew array pairs to zero against the symmetric
Hessian of a smooth test function, and the first two sums are, after renaming the
summation indices and using skewness once, exactly the two forcings. Only the
first derivative of k is used, so C¹ with continuous derivative is enough;
the shell increments carry C² data.
The single integration by parts is carried out against the test function
x ↦ ∂_j φ (x) · k_{i j}(x), which is C¹ and compactly supported in the cube
but not smooth. It is admissible because a smooth compactly supported factor
times an H¹ factor lies in H¹₀, and an H¹ function integrates by parts
against every H¹₀ function. The passage from smooth test functions to H¹₀
test functions is the H¹₀ approximating sequence, exactly as in the constant
skew shift and in the constant-forcing invariance.
Main definitions #
matFieldDiv k— the divergence(∇ · k)_j = ∑_i ∂_i k_{i j}of a matrix field.
References #
- ABK26, the proof of the injection estimate of Section 5.1 (the antisymmetry step of the iteration scheme).
Algsuperdiff.Section3.Cutoff.Limit(cutoff_skew),Algsuperdiff.Section3.Cutoff.Finite(finiteShellIncrement_skew) — the skewness of the cutoff and of its finite increments.Algsuperdiff.Section3.Provider.Stream.ShellSum(shellIncrement,shellIncrement_apply_eq_cutoff_sub) — the increment as a shell field with honest first and second derivatives.Algsuperdiff.Section4.Provider.ExcessDecay.AntisymmetricShift— the constant skew matrix case, where no derivative of the field appears.
1. Shared divergence convention #
The generic divergence and analytic support are imported from FieldDivergenceTest.
2. Two elementary reductions #
3. L² membership on a bounded domain #
4. From smooth tests to zero-trace tests #
5. The identity against smooth tests #
6. Integral identities for the forcing fields #
7. The antisymmetry transfer #
The antisymmetry transfer.
For a C¹ matrix field k that is skew at every point, and for w ∈ H¹(U) on a
bounded convex open set U, the two weak forcings w (∇ · k) and k ∇w pair
identically against the gradient of every zero-trace test function:
∫_U (w (∇ · k)) · ∇φ = ∫_U (k ∇w) · ∇φ , φ ∈ H¹₀(U) .
Equivalently ∇ · (w (∇ · k)) = ∇ · (k ∇w) in the sense of distributions. Both
extra terms of the expansion
∑_{i,j} ∂_i (k_{i j} ∂_j w) = ∑_{i,j} (∂_i k_{i j}) ∂_j w + ∑_{i,j} k_{i j} ∂_i ∂_j w
vanish because a skew array pairs to zero against a symmetric one: here the
symmetric array is the second derivative of the smooth test function, which is
where the single integration by parts of the proof places both derivatives.
The antisymmetry transfer on the weak equation. The divergence-form weak
equation with forcing -w (∇ · k) and the one with forcing -k ∇w have exactly
the same solutions when k is C¹ and skew.
The antisymmetry transfer on the localized Dirichlet problem. The boundary
clause of IsDirichletSolutionAt does not see the forcing field, so the transfer
moves the whole predicate.
8. The shell increment of the coefficient cutoff #
Every entry of a shell field is C¹; the carrier stores continuous first and
second derivatives, so the field is in fact C².