The reduction of MeridionalSmallness (eq:aniso:small, the conclusion of
prop:aniso:small) to the single-term bound on u_r / r that the swirl equation's maximum
principle (eq:aniso:closure:w) consumes as its smallness hypothesis, the pointwise domination
radialQuotient and the other components of eq:aniso:G by their sum being the only step needed.
theorem
CIV.abs_spatialPartial_radial_le_meridionalQuantity
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 0) 0 z| ≤ meridionalQuantity u z
theorem
CIV.abs_spatialPartial_axial_le_meridionalQuantity
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
|CKN.spatialPartial (fun (w : CKN.Foundation.Parabolic.ParabolicPoint) => u w 2) 2 z| ≤ meridionalQuantity u z
theorem
CIV.tendsto_radialQuotient_of_meridionalSmallness
{ρ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsmall : MeridionalSmallness ρ u)
(ε : ℝ)
:
0 < ε →
∃ t₀ ∈ Set.Ioo (-1) 0,
∀ t ∈ Set.Ioo t₀ 0,
∀ (x₁ x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ → -t * |radialQuotient u (meridional x₁ x₃, t)| ≤ ε
theorem
CIV.swirl_hG_of_meridionalSmallness
{ρ Rstar η : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsmall : MeridionalSmallness ρ u)
(hη : 0 < η)
(hRstar : Rstar ≤ ρ)
:
∃ tη ∈ Set.Ioo (-1) 0,
∀ t ∈ Set.Ioo tη 0,
∀ (x₁ x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 Rstar → |radialQuotient u (meridional x₁ x₃, t)| ≤ η / -t