Slice Bounds #
Supporting results for the Constantin–Ignatova–Vicol axisymmetric regularity theorem.
theorem
CIV.IsLocallyBoundedOn.ae_slice_bound
{m : ℕ}
{I J : Set ℝ}
{q : CKN.Vec m × ℝ → ℝ}
(hq : IsLocallyBoundedOn m I q)
(hJ : IsCompact J)
(hJI : J ⊆ I)
:
If q is locally bounded on I, then for every compact J ⊆ I there exists M ≥ 0 such
that for almost every time slice τ ∈ J, the spatial function x ↦ q(x, τ) is bounded by M
almost everywhere in x.
theorem
CIV.IsLocallyBoundedOn.ae_slice_measurable
{m : ℕ}
{I : Set ℝ}
{q : CKN.Vec m × ℝ → ℝ}
(hq : IsLocallyBoundedOn m I q)
:
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Vec m) => q (x, τ)) MeasureTheory.volume
If q is locally bounded on I, then for almost every τ ∈ I the slice
x ↦ q(x, τ) is AEStronglyMeasurable on ℝ^m.
theorem
CIV.IsAdmissibleDrift.ae_slice
{m : ℕ}
{I J : Set ℝ}
{B : CKN.Vec m × ℝ → CKN.Vec m}
{divB : CKN.Vec m × ℝ → ℝ}
(hB : IsAdmissibleDrift m I B divB)
(hJ : IsCompact J)
(hJI : J ⊆ I)
:
If B is an admissible drift on I, then for every compact J ⊆ I there exists Λ ≥ 0
such that for almost every τ ∈ J the slice B(·, τ) is bounded and Λ-Lipschitz in x,
|divB(·, τ)| ≤ Λ, and divB(·, τ) is the weak divergence of B(·, τ).