Documentation

LeanPool.EscauriazaSereginSverak.Endpoint.VorticityTopTrace

Distributional velocity traces for vorticity #

The terminal velocity trace is expressed by its action on compactly supported smooth spatial tests. This is the trace convention used to identify the terminal value of a continuous vorticity representative.

source
def ESS.HasZeroDistributionalVelocityTrace (u : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3) :
Prop

A velocity has zero weak local trace at time zero if every compactly supported smooth spatial pairing tends to zero from negative times (manuscript lem:vorticity-top-extension).

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    theorem ESS.spatialVorticityTestCurl_contDiff {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : ContDiff ℝ (↑⊤) ψ) :
    ContDiff ℝ (↑⊤) (spatialTestCurl ψ)

    The curl of a smooth vector test is smooth.

    source
    theorem ESS.spatialVorticityTestCurl_hasCompactSupport {ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} (hψ : HasCompactSupport ψ) :
    HasCompactSupport (spatialTestCurl ψ)

    The curl of a compactly supported vector test is compactly supported.