Curl Cutoff

Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.

noncomputable def CIV.gradVec (χ : CKN.Foundation.Parabolic.Vec3 → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The gradient of a scalar χ on Vec3, as the vector of its partials.

Equations

• CIV.gradVec χ x i = (fderiv ℝ χ x) (CKN.basisVec i)

def CIV.cross3 (a b : CKN.Foundation.Parabolic.Vec3) : CKN.Foundation.Parabolic.Vec3

The cross product on Vec3.

Equations

• CIV.cross3 a b = ![a 1 * b 2 - a 2 * b 1, a 2 * b 0 - a 0 * b 2, a 0 * b 1 - a 1 * b 0]

theorem CIV.curlVec_smul {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} (hχ : DifferentiableAt ℝ χ x) (hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) : curlVec (fun (y : CKN.Foundation.Parabolic.Vec3) => χ y • v y) x = χ x • curlVec v x + cross3 (gradVec χ x) (v x)

theorem CIV.div_smul {χ : CKN.Foundation.Parabolic.Vec3 → ℝ} {v : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {x : CKN.Foundation.Parabolic.Vec3} (hχ : DifferentiableAt ℝ χ x) (hv : ∀ (i : Fin 3), DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y i) x) : ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (χ y • v y) j) x) (CKN.basisVec j) = χ x * ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => v y j) x) (CKN.basisVec j) + ∑ j : Fin 3, gradVec χ x j * v x j

theorem CIV.sum_sq_cross3_le (a b : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, cross3 a b i ^ 2 ≤ (∑ i : Fin 3, a i ^ 2) * ∑ i : Fin 3, b i ^ 2

theorem CIV.sum_sq_add_le_two_mul (a b : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (a i + b i) ^ 2 ≤ 2 * ∑ i : Fin 3, a i ^ 2 + 2 * ∑ i : Fin 3, b i ^ 2

theorem CIV.sum_sq_smul (c : ℝ) (a : CKN.Foundation.Parabolic.Vec3) : ∑ i : Fin 3, (c • a) i ^ 2 = c ^ 2 * ∑ i : Fin 3, a i ^ 2