Is Bounded Near #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
def
CIV.IsBoundedNear
(u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(x : CKN.Foundation.Parabolic.Vec3)
:
u is bounded near x if it is bounded, by some constant, on some backward
parabolic neighbourhood of x whose time window has length the square of its spatial
radius: ∃ r, M, |u| ≤ M on B(x, r) × (-r², 0). This is the scale-invariant relative
of BoundedNearOrigin, centred at a general point, that names the failure set of
lem:aniso:annulus (design note R12).
Equations
- CIV.IsBoundedNear u x = ∃ (r : ℝ) (M : ℝ), 0 < r ∧ ∀ y ∈ CKN.Foundation.Parabolic.vec3Ball x r, ∀ t ∈ Set.Ioo (-r ^ 2) 0, CKN.Foundation.Parabolic.vec3EuclideanNorm (u (y, t)) ≤ M