Theta Transport Divergence Form

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

theorem CIV.zoomTheta_transport_divergenceForm (lam h rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hR : p.1.1 ≠ -(rc / lam)) : zoomVRec lam h rc zc u p * dr (zoomTheta lam h rc zc u) p + zoomWRec lam h rc zc u p * dz (zoomTheta lam h rc zc u) p = dr (fun (q : (ℝ × ℝ) × ℝ) => zoomVRec lam h rc zc u q * zoomTheta lam h rc zc u q) p + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomWRec lam h rc zc u q * zoomTheta lam h rc zc u q) p + zoomVRec lam h rc zc u p / (rc / lam + p.1.1) * zoomTheta lam h rc zc u p

theorem CIV.zoomTheta_pde_divergenceForm (lam h rc zc : ℝ) (hlam : 0 < lam) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (pr : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (hsol : IsClassicalSolutionOn u pr f unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (p : (ℝ × ℝ) × ℝ) (hp : zoomPointRec lam h rc zc p ∈ unitCylinder) (hR : p.1.1 ≠ -(rc / lam)) : dtPast (zoomTheta lam h rc zc u) p + dr (fun (q : (ℝ × ℝ) × ℝ) => zoomVRec lam h rc zc u q * zoomTheta lam h rc zc u q) p + dz (fun (q : (ℝ × ℝ) × ℝ) => zoomWRec lam h rc zc u q * zoomTheta lam h rc zc u q) p = dr (dr (zoomTheta lam h rc zc u)) p + 1 / (rc / lam + p.1.1) * dr (zoomTheta lam h rc zc u) p + (lam ^ (2 * h)) ^ 2 * dz (dz (zoomTheta lam h rc zc u)) p - zoomTheta lam h rc zc u p / (rc / lam + p.1.1) ^ 2 + 1 / (rc / lam + p.1.1) * dz (fun (q : (ℝ × ℝ) × ℝ) => zoomSRec lam h rc zc u q ^ 2) p + lam ^ 4 * lam ^ (2 * h) * curlComp f 1 (zoomPointRec lam h rc zc p)