Parabolic Rescaling Axisymmetric

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

theorem CIV.rotField_smul_comp (φ c R : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : rotField φ (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => c • u (R • w.1, R ^ 2 * w.2)) z = c • rotField φ u (R • z.1, R ^ 2 * z.2)

The rotation of a rescaled field equals the rescaling of the rotated field: rotField φ (R·, R²·) (c u) = c · rotField φ u at the rescaled point.

theorem CIV.angularMean_smul_comp (c R : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : angularMean (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => c • u (R • w.1, R ^ 2 * w.2)) z = c • angularMean u (R • z.1, R ^ 2 * z.2)

The angular mean commutes with the parabolic rescaling: 𝒫(c u(R·, R²·)) = c · 𝒫u at the rescaled point.

theorem CIV.isAxisymmetricOn_smul_comp_of_isAxisymmetricOn {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {R : ℝ} (hR0 : 0 < R) (hR1 : R ≤ 1) (haxi : IsAxisymmetricOn u unitCylinder) : IsAxisymmetricOn (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => R • u (R • w.1, R ^ 2 * w.2)) unitCylinder

If u is axisymmetric on the unit cylinder, then the parabolically rescaled field R u(R·, R²·) is also axisymmetric on the unit cylinder, for 0 < R ≤ 1.