The axis quotient, its integral representation, and the three-term selection

This file publishes the representation of the radial quotient u_r / r on the meridional plane as an average of ∂_r u_r along the segment from the axis (the paragraph after eq:aniso:circulation:pde), together with the pointwise bounds this representation gives on that segment, and the reflection-symmetric three-term selection used when MeridionalSmallness fails (the paragraph after eq:aniso:zoom:selected).

Smoothness and differentiability of an axial slice, at a general component

The meridional segment through the axis

The integral representation of the radial quotient

theorem CIV.radialQuotient_eq_integral (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) (x₁ x₃ : ℝ) (hx : x₁ ^ 2 + x₃ ^ 2 < 1) : radialQuotient u (meridional x₁ x₃, t) = ∫ (s : ℝ) in 0..1, CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (s * x₁) x₃, t)

The manuscript's u_r/r, extended across the axis, is the average of the radial derivative ∂_r u_r along the segment from the axis to (x₁, x₃) (the paragraph after eq:aniso:circulation:pde). Public form of the radialQuotient_eq_integral.

Bound 1: the radial quotient on a segment through the axis

theorem CIV.abs_radialQuotient_le_of_segment_bound (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) (x₁ x₃ M : ℝ) (hx : x₁ ^ 2 + x₃ ^ 2 < 1) (hM : ∀ s ∈ Set.Icc 0 1, |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (s * x₁) x₃, t)| ≤ M) : |radialQuotient u (meridional x₁ x₃, t)| ≤ M

|u_r/r| ≤ M at (x₁, x₃) whenever |∂_r u_r| ≤ M along the segment {(s x₁, x₃) : s ∈ [0, 1]} from the axis, via the integral representation radialQuotient_eq_integral (the paragraph after eq:aniso:circulation:pde).

Second partial derivatives along the meridional segment

Bound 2: ∂_z u_r / x₁ on a segment through the axis

theorem CIV.abs_spatialPartial_two_zero_div_le_of_segment_bound (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) (x₁ x₃ M : ℝ) (hx : x₁ ^ 2 + x₃ ^ 2 < 1) (hx1 : x₁ ≠ 0) (hM : ∀ a ∈ Set.uIcc 0 x₁, |CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 0 (meridional a x₃, t)| ≤ M) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 2 (meridional x₁ x₃, t) / x₁| ≤ M

|∂_z u_r / x₁| ≤ M at (x₁, x₃) with x₁ ≠ 0 whenever |∂_r ∂_z u_r| ≤ M along the segment from the axis, since ∂_z u_r vanishes on the axis (spatialPartial_two_zero_axis).

Bound 3: ∂_r u_z / x₁ on a segment through the axis

theorem CIV.abs_spatialPartial_zero_two_div_le_of_segment_bound (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) (x₁ x₃ M : ℝ) (hx : x₁ ^ 2 + x₃ ^ 2 < 1) (hx1 : x₁ ≠ 0) (hM : ∀ a ∈ Set.uIcc 0 x₁, |CKN.spatialSecondPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 0 (meridional a x₃, t)| ≤ M) : |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 0 (meridional x₁ x₃, t) / x₁| ≤ M

|∂_r u_z / x₁| ≤ M at (x₁, x₃) with x₁ ≠ 0 whenever |∂_r ∂_r u_z| ≤ M along the segment from the axis, since ∂_r u_z vanishes on the axis (spatialPartial_zero_two_axis).

Parity of the derivative fields under the meridional reflection

theorem CIV.meridionalQuantity_reflect {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (haxi : IsAxisymmetricOn u unitCylinder) (hu1 : ContDiffOn ℝ (↑1) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) {x₁ x₃ t : ℝ} (hz : (meridional x₁ x₃, t) ∈ unitCylinder) : meridionalQuantity u (meridional (-x₁) x₃, t) = meridionalQuantity u (meridional x₁ x₃, t)

Each summand of meridionalQuantity is invariant under the reflection x₁ ↦ -x₁ of the meridional plane, so the quantity itself is even: ∂_r u_r and ∂_z u_z are even, u_r/r is even, and ∂_z u_r is odd (so |∂_z u_r| is even).

(-t)^h → 0 for a general positive exponent

theorem CIV.tendsto_neg_rpow_nhdsWithin_zero {h : ℝ} (hh : 0 < h) : Filter.Tendsto (fun (t : ℝ) => (-t) ^ h) (nhdsWithin 0 (Set.Iio 0)) (nhds 0)

(-t)^h → 0 as t ↑ 0, for any positive real exponent h. Unlike tendsto_zoom_lengths, whose exponents are the fixed 1/2, 2h and 1 - 2h, this holds for an arbitrary positive h.

Membership helpers for the reflection

The three-term selection from a failure of meridional smallness

theorem CIV.exists_seq_three_terms {ρ h C : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hu : ContDiffOn ℝ (↑⊤) (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => u z) unitCylinder) (haxi : IsAxisymmetricOn u unitCylinder) (hb : AnisotropicBounds C h u) (hh : 0 < h) (hρ : ρ ≤ 1) (hnot : ¬MeridionalSmallness ρ u) : ∃ (c₀ : ℝ), 0 < c₀ ∧ ∃ (t : ℕ → ℝ) (x₁ : ℕ → ℝ) (x₃ : ℕ → ℝ), (∀ (n : ℕ), 0 ≤ x₁ n) ∧ StrictMono t ∧ Filter.Tendsto t Filter.atTop (nhds 0) ∧ (∀ (n : ℕ), meridional (x₁ n) (x₃ n) ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) ∧ (∀ (n : ℕ), t n ∈ Set.Ioo (-1) 0) ∧ ∀ (n : ℕ), c₀ < -t n * (|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 (meridional (x₁ n) (x₃ n), t n)| + |radialQuotient u (meridional (x₁ n) (x₃ n), t n)| + |CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 (meridional (x₁ n) (x₃ n), t n)|)

If MeridionalSmallness ρ u fails, the first three terms of meridionalQuantity alone — dropping |∂_z u_r|, which the anisotropic Type II bounds force to zero after multiplication by -t — still exceed a fixed positive constant along a sequence approaching the singular time, with the radial coordinate taken nonnegative by the reflection symmetry of the meridional plane. The selected points lie in vec3Ball 0 ρ and the selected times in Ioo (-1) 0, the times increase strictly to the singular time, and the inequality holds at every index: the tail on which it holds is reindexed from the start. This is the selection used after eq:aniso:zoom:selected.