Meridional G

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

noncomputable def CIV.meridionalG (ρ : ℝ) (u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The supremum G_ρ(t) of eq:aniso:G, over the meridional-plane points of B(ρ).

Equations

• One or more equations did not get rendered due to their size.

theorem CIV.meridionalG_le_of_meridionalSmallness {ρ η : ℝ} (hη : 0 < η) {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hsmall : MeridionalSmallness ρ u) (hne : ∃ (x₁ : ℝ) (x₃ : ℝ), meridional x₁ x₃ ∈ CKN.Foundation.Parabolic.vec3Ball 0 ρ) : ∃ tη ∈ Set.Ioo (-1) 0, ∀ t ∈ Set.Ioo tη 0, meridionalG ρ u t ≤ η / -t

The reduction of MeridionalSmallness (eq:aniso:small) to the pointwise decay G_ρ(t) ≤ η/(-t) that lem:aniso:closure's Grönwall step consumes.

No boundedness of the meridional quantity set is needed: the bound is proved by csSup_le, which needs only that the set is nonempty and that every element is at most η/(-t).