Spatial Gradient Sq ENorm

Supporting estimates for the Navier–Stokes development.

theorem CKN.ofReal_spatialGradientSq_le_nine_mul (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) : ENNReal.ofReal (spatialGradientSq u Du z) ≤ 9 * ‖Du z‖ₑ ^ 2

The extended-real form of the inequality |∇u|² ≤ 9 ‖Du‖²: for any velocity field u and its spatial gradient Du, the ENNReal-valued ofReal of the squared spatial gradient density is bounded by 9 times the ENNReal-valued norm of Du raised to power (2 : ℝ).