Documentation

LeanPool.CIVAxisymmetric.Statements.IsClassicalSolutionOn

Is Classical Solution On #

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

source
def CIV.IsClassicalSolutionOn (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (S : Set CKN.Foundation.Parabolic.ParabolicPoint) :
Prop

A classical solution of the forced Navier–Stokes equations eq:nse:forced on an open space-time set: smooth fields satisfying the momentum and divergence equations pointwise.

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