Auxiliary lemmas

Main theorems

theorem CIV.meridional_axis_component_zero (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (haxi : IsAxisymmetricOn u unitCylinder) (ht : t ∈ Set.Ioo (-1) 0) (x₃ : ℝ) (hx : |x₃| < 1) : u (meridional 0 x₃, t) 0 = 0

Smoothness of the axial slice x ↦ u (x, t) 0

The integral representation of the radial quotient

Continuity of the parametric integral, jointly on the meridional plane

Continuity of the radial quotient across the axis

theorem CIV.continuousOn_radialQuotient_plane (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (ht : t ∈ Set.Ioo (-1) 0) : ContinuousOn (fun (y : ℝ × ℝ) => radialQuotient u (meridional y.1 y.2, t)) {y : ℝ × ℝ | y.1 ^ 2 + y.2 ^ 2 < 1}

On a time slice of the unit cylinder, radialQuotient (the manuscript's u_r/r, extended across the axis as in the paragraph after eq:aniso:G) is continuous on the whole open disk of the meridional plane {x₂ = 0}, including the axis point x₁ = x₃ = 0.

theorem CIV.continuousOn_radialQuotient_slice (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (ht : t ∈ Set.Ioo (-1) 0) : ContinuousOn (fun (x₁ : ℝ) => radialQuotient u (meridional x₁ 0, t)) (Set.Ioo (-1) 1)

The restriction of continuousOn_radialQuotient_plane to the radial axis x₃ = 0 of the meridional plane.