Scaling Quantity Nonneg

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

theorem CKN.alpha_nonneg (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ alpha u z r

The velocity energy quantity α is nonnegative.

theorem CKN.beta_nonneg (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ beta u Du z r

The gradient quantity β is nonnegative.

theorem CKN.gamma_nonneg (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ gamma u z r

The velocity cubic quantity γ is nonnegative.

theorem CKN.delta_nonneg (p : Foundation.Parabolic.ParabolicPoint → ℝ) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ delta p z r

The pressure quantity δ is nonnegative.

theorem CKN.lambda_nonneg (q : ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) {r : ℝ} (hr : 0 ≤ r) : 0 ≤ lambda q f z r

The force quantity λ is nonnegative.