Partial Calculus

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

theorem CIV.spatialPartial_add_of_differentiableAt {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) (hh : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, z.2)) z.1) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w + h w) i z = CKN.spatialPartial g i z + CKN.spatialPartial h i z

theorem CIV.spatialPartial_sub_of_differentiableAt {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) (hh : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, z.2)) z.1) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w - h w) i z = CKN.spatialPartial g i z - CKN.spatialPartial h i z

theorem CIV.spatialPartial_mul_of_differentiableAt {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) (hh : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => h (x, z.2)) z.1) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w * h w) i z = g z * CKN.spatialPartial h i z + h z * CKN.spatialPartial g i z

theorem CIV.spatialPartial_const_mul_of_differentiableAt {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (c : ℝ) (hg : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => c * g w) i z = c * CKN.spatialPartial g i z

theorem CIV.spatialPartial_time_weight_mul {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (φ : ℝ → ℝ) (hg : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, z.2)) z.1) : CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w.2 * g w) i z = φ z.2 * CKN.spatialPartial g i z

theorem CIV.timePartial_add_of_differentiableAt {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (t : ℝ) => g (z.1, t)) z.2) (hh : DifferentiableAt ℝ (fun (t : ℝ) => h (z.1, t)) z.2) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w + h w) z = CKN.timePartial g z + CKN.timePartial h z

theorem CIV.timePartial_mul_of_differentiableAt {g h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (hg : DifferentiableAt ℝ (fun (t : ℝ) => g (z.1, t)) z.2) (hh : DifferentiableAt ℝ (fun (t : ℝ) => h (z.1, t)) z.2) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => g w * h w) z = g z * CKN.timePartial h z + h z * CKN.timePartial g z

theorem CIV.timePartial_neg_rpow_mul {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (η : ℝ) (hz : z.2 < 0) (hg : DifferentiableAt ℝ (fun (t : ℝ) => g (z.1, t)) z.2) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => (-w.2) ^ η * g w) z = -(η * (-z.2) ^ (η - 1)) * g z + (-z.2) ^ η * CKN.timePartial g z

theorem CIV.timePartial_space_weight_mul {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {z : CKN.Foundation.Parabolic.ParabolicPoint} (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ) (hg : DifferentiableAt ℝ (fun (t : ℝ) => g (z.1, t)) z.2) : CKN.timePartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => ψ w.1 * g w) z = ψ z.1 * CKN.timePartial g z

theorem CIV.spatialSecondPartial_time_weight_mul {g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {i j : Fin 3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (φ : ℝ → ℝ) (hg : ∀ (x : CKN.Foundation.Parabolic.Vec3), DifferentiableAt ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => g (y, z.2)) x) (hg' : DifferentiableAt ℝ (fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.spatialPartial g i (x, z.2)) z.1) : CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => φ w.2 * g w) i j z = φ z.2 * CKN.spatialSecondPartial g i j z