Compactness Gradient Fiber

Supporting estimates for the Navier–Stokes development.

@[reducible, inline]

abbrev CKN.Leray.CompactnessGradientFiber : Type

The nine spatial derivative coordinates with their Euclidean Hilbert norm.

Equations

• CKN.Leray.CompactnessGradientFiber = PiLp 2 fun (x : Fin 3) => CKN.Foundation.Parabolic.L2Vec3

def CKN.Leray.toCompactnessGradientFiber (A : Fin 3 → Foundation.Parabolic.Vec3) : CompactnessGradientFiber

The matrix field in its Euclidean Hilbert carrier.

Equations

• CKN.Leray.toCompactnessGradientFiber A = WithLp.toLp 2 fun (i : Fin 3) => WithLp.toLp 2 (A i)

theorem CKN.Leray.norm_toCompactnessGradientFiber_sq (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : ‖toCompactnessGradientFiber (Du z)‖ ^ 2 = spatialGradientSq u Du z

The norm in the gradient carrier has the exact spatial energy density.