UTensor Norm Factor

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.pressureUTensorNorm_eq_mul (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) (y : Foundation.Parabolic.Vec3) : pressureUTensorNorm u c s y = Foundation.Parabolic.vec3EuclideanNorm (u (y, s)) * Foundation.Parabolic.vec3EuclideanNorm (u (y, s) - c s)

The Frobenius norm of the velocity tensor u_i (u_j - c_j) factors as |u| · |u - c|.