Documentation

LeanPool.Superdiffusion.Algsuperdiff.StochasticProcess.Common.DivergenceForm.Decay.LocalizedSkewDivergence

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.

Equations
Instances For
    theorem DivergenceFormProcess.Decay.continuous_skewFieldDiv_apply {d : ℕ} {k : HCPolySupport.Vec d → HCPolySupport.Mat d} (hk : ∀ (p q : Fin d), ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => k x p q) (j : Fin d) :

    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 #

      theorem DivergenceFormProcess.Decay.memScalarL2_matVecMul_coord {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hUm : MeasurableSet U) (hUb : HCPolySupport.IsBoundedDomain U) {k : HCPolySupport.Vec d → HCPolySupport.Mat d} (hk : ∀ (p q : Fin d), ContDiff ℝ 1 fun (x : HCPolySupport.Vec d) => k x p q) {G : HCPolySupport.Vec d → HCPolySupport.Vec d} (hG : ∀ (j : Fin d), HCPolySupport.MemScalarL2 U fun (x : HCPolySupport.Vec d) => G x j) (i : Fin d) :

      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.