Documentation

LeanPool.CIVAxisymmetric.Statements.IsDistributionalDriftDiffusion

Is Distributional Drift Diffusion #

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

def CIV.IsDistributionalDriftDiffusion (m d : ℕ) (I : Set ℝ) (B : CKN.Vec m × ℝ → CKN.Vec m) (divB q : CKN.Vec m × ℝ → ℝ) :

∂_τ q + B·∇q = Δ_X q on Vec m × I in the sense of distributions, with B·∇q = div(Bq) - (div B) q (footnote to eq:aniso:comparison:equation), the divergence div B of the drift being carried as data (design note N5).

Equations
  • One or more equations did not get rendered due to their size.
Instances For