Documentation

LeanPool.CIVAxisymmetric.Statements.IsAdmissibleDrift

Is Admissible Drift #

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

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

The drift class eq:aniso:comparison:drift: B measurable with measurable divergence div B, and for every compact J ⊆ I one constant Λ such that for a.e. τ ∈ J the slice B(·, τ) is bounded and Lipschitz with constant Λ, and divB(·, τ) is bounded by Λ and is the weak divergence of B(·, τ).

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