Meridional Norm

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

theorem CIV.vec3EuclideanNorm_meridional (x₁ x₃ : ℝ) : CKN.Foundation.Parabolic.vec3EuclideanNorm (meridional x₁ x₃) = √(x₁ ^ 2 + x₃ ^ 2)

The Euclidean norm of a meridional vector (x₁, 0, x₃) reduces to the 2D Euclidean norm of (x₁, x₃).

theorem CIV.meridional_mem_vec3Ball_zero_iff (x₁ x₃ r : ℝ) : meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 r ↔ x₁ ^ 2 + x₃ ^ 2 < r ^ 2 ∧ 0 < r

A meridional vector lies in the Euclidean ball of radius r centred at the origin iff x₁² + x₃² < r² and r > 0. For r ≤ 0 the ball is empty, so the equivalence holds vacuously on both sides.

theorem CIV.meridional_mem_unitCylinder_iff (x₁ x₃ t : ℝ) : (meridional x₁ x₃, t) ∈ unitCylinder ↔ x₁ ^ 2 + x₃ ^ 2 < 1 ∧ -1 < t ∧ t < 0

A point (meridional x₁ x₃, t) lies in the unit cylinder B(1) × (-1, 0) iff x₁² + x₃² < 1 and -1 < t < 0.