Documentation

LeanPool.CaffarelliKohnNirenberg.Statements.IsForcedLerayHopfSolution

Is Forced Leray Hopf Solution #

Supporting estimates for the Navier–Stokes development.

source
def CKN.IsForcedLerayHopfSolution (T : ℝ) (a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) (f u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) :
Prop

The finite-time forced Leray--Hopf conditions from def:forced-leray-hopf. The shared time representative satisfies the energy class, weak continuity, and initial trace clauses of def:leray-hopf, together with the forced momentum and work inequalities.

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