Compact spatial slice bounds for the blow-up trace #
The all-time measurable trace has uniformly bounded rescaled L² slices on
each compact spatial set. This is the slice input to
CKN.Leray.lem_compactness.
theorem
ESS.blowup_limit_trace_rescaled_compact_slice_bound
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(M : ℝ)
(hsource :
∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
MeasureTheory.MemLp
((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) 3
MeasureTheory.volume ∧ MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm
((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)) x))
3 MeasureTheory.volume ≤ ENNReal.ofReal M)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(r : ℝ)
(hr : 0 < r)
(C : Set CKN.Foundation.Parabolic.Vec3)
(hC : IsCompact C)
(t : ↑(Set.Icc (-(3 / 4) ^ 2) 0))
:
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal
(CKN.Foundation.Parabolic.vec3EuclideanNorm
(r • (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator
(fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t)) (x₀ + r • x))) ^ 2 ≤ (ENNReal.ofReal M * MeasureTheory.volume C ^ (1 / 6)) ^ 2
A uniformly bounded source L³ trace gives a uniform rescaled local
L² bound on every time slice.
theorem
ESS.blowup_limit_trace_terminal_rescaling_tendsto_zero
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(hsource :
∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
MeasureTheory.MemLp
((CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, t)) 3
MeasureTheory.volume)
(t₀ : ↑(Set.Icc (-(3 / 4) ^ 2) 0))
(x₀ c : CKN.Foundation.Parabolic.Vec3)
(r : ℕ → ℝ)
(hr : ∀ (k : ℕ), 0 < r k)
(hr0 : Filter.Tendsto r Filter.atTop (nhds 0))
:
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
r k • (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)).indicator (fun (y : CKN.Foundation.Parabolic.Vec3) => W (y, t₀))
(x₀ + r k • x))
2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball c 1)))
Filter.atTop (nhds 0)
Every fixed terminal trace slice has strongly vanishing local L²
rescalings, by absolute continuity of its source L³ integral.