meridionalQuantity ≤ meridionalG and meridionalG_nonneg (the nonnegativity of the
supremum G_ρ(t)), together with the bundled existence theorem that collects all three
consequences of MeridionalSmallness in one call.
theorem
CIV.meridionalG_nonneg
{ρ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{t : ℝ}
(hne : ∃ (x₁ : ℝ) (x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
:
theorem
CIV.meridionalQuantity_le_meridionalG
{ρ : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{t : ℝ}
(hbdd :
BddAbove
{q : ℝ | ∃ (x₁ : ℝ) (x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ ∧ q = meridionalQuantity u (meridional x₁ x₃, t)})
{x₁ x₃ : ℝ}
(hmem : meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
:
theorem
CIV.exists_meridionalG_hG_of_meridionalSmallness
{ρ η : ℝ}
(hη : 0 < η)
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hsmall : MeridionalSmallness ρ u)
(hbdd :
∀ (t : ℝ),
BddAbove
{q : ℝ | ∃ (x₁ : ℝ) (x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ ∧ q = meridionalQuantity u (meridional x₁ x₃, t)})
(hne : ∃ (x₁ : ℝ) (x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ)
:
∃ tη ∈ Set.Ioo (-1) 0,
(∀ t ∈ Set.Ioo tη 0, 0 ≤ meridionalG ρ u t) ∧ (∀ t ∈ Set.Ioo tη 0,
∀ (x₁ x₃ : ℝ),
meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ →
meridionalQuantity u (meridional x₁ x₃, t) ≤ meridionalG ρ u t) ∧ ∀ t ∈ Set.Ioo tη 0, meridionalG ρ u t ≤ η / -t