LocalizedSkewDivergence #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The weak divergence of a C¹ antisymmetric coefficient field #
A C¹ antisymmetric matrix field k acts on a divergence-form equation as a
divergence-free drift: the flux k grad u pairs against a zero-trace test
exactly as the drift u (div k) does, because the only two terms produced by
one integration by parts are the drift and a contraction of k with the
Hessian of the test, and the second vanishes by antisymmetry.
The consequence used by the localized decay estimates is the quadratic identity
∫ u ⟨k ∇u, ∇w⟩ = (1 / 2) ∫ u ^ 2 ⟨div k, ∇w⟩ ,
valid for a zero-trace u and a smooth compactly supported multiplier w.
It is what replaces the crude size bound for the smooth part of the skew
coefficient: the left side carries a gradient of the solution and would only
admit a bound by ‖k‖, while the right side carries no gradient at all and is
bounded by ‖div k‖.
The identity is obtained without any chain rule for u ^ 2, by pairing the
transfer identity twice, once with the test w u and once with the factor
w u. Only the divergence-form layer is used, so this module depends on no
model-specific construction.
Divergence convention #
skewFieldDiv k contracts the first index,
(div k)_j (x) = ∑_i ∂_i k_{i j}(x) ,
the contraction that turns a ∇u into ∇ · (a ∇u) in the divergence-form
equation. With this convention the quadratic identity carries a plus sign;
with the opposite (row) contraction both sides change sign.
Main results #
The divergence of a matrix field #
The divergence of a matrix field, contracting the first index.
Instances For
Each coordinate of the divergence of a C¹ matrix field is continuous.
L² membership on a bounded domain #
A C¹ function on a bounded measurable domain, packaged with its
classical gradient.
Equations
- One or more equations did not get rendered due to their size.
Instances For
From smooth tests to zero-trace tests #
The transfer identity against smooth tests #
L² control of the two flux fields #
Each coordinate of the flux of a continuous matrix field against an L²
vector field is square integrable on a bounded domain.
The drift pairing of a C¹ matrix field against an L² vector field is
square integrable on a bounded domain.
The transfer identity #
The antisymmetry transfer against zero-trace tests. For a C¹ matrix
field that is antisymmetric at every point, the flux k grad v pairs against a
zero-trace test exactly as the drift -(test) (div k) · grad v does. One
integration by parts produces the drift together with a contraction of k
against the Hessian of a smooth test, and the second term vanishes because an
antisymmetric array pairs to zero against a symmetric one.
The quadratic identity #
The antisymmetric flux as a drift. For a zero-trace z and a smooth
compactly supported multiplier w, the drift pairing w z ⟨div k, grad z⟩ is
the negative of the flux cross term z ⟨k grad z, grad w⟩.
Integration by parts for the antisymmetric flux against a smooth
multiplier. For a zero-trace z and a smooth compactly supported w, the
cross term z ⟨k grad z, grad w⟩ carries no gradient of z at all: it equals
half of the drift term z ^ 2 ⟨div k, grad w⟩. This is what lets the smooth
part of an antisymmetric coefficient be paid for by ‖div k‖ rather than by
‖k‖.
The drift pairing in terms of the multiplier gradient alone.