Compactness on an exhaustion of space-time #
This is the diagonal compactness passage of prop:blowup-limit, in the form
needed for the blow-up sequence: the uniform hypotheses of
lem:compactness of the CKN manuscript hold on each fixed bounded past cylinder only from a
stage-dependent index on. The growing cutoffs of
blowupLimitAssemblyCutoffField reduce this to a single application of
lem:compactness on all of space and all negative times, and the
conclusions transfer back to a subsequence of the original fields.
theorem
ESS.blowupLimitAssembly_compact_bound
{Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)}
(hQ : IsCompact Q)
:
Bounds of a compact subset of space-time in space and in past time.
theorem
ESS.blowupLimitAssembly_exhaustion_compactness
(f : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(Df : ℕ → CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hf : ∀ (n : ℕ), Measurable (f n))
(hDf : ∀ (n : ℕ), Measurable (Df n))
(hslice :
∀ (C : Set CKN.Foundation.Parabolic.Vec3),
IsCompact C →
∃ M < ⊤,
∀ (n : ℕ) (t : ℝ),
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (f n (x, t))) ^ 2 ≤ M)
(hstage :
∀ (m : ℕ),
∃ (N : ℕ),
(∀ (n : ℕ),
N ≤ n →
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(↑m + 1)) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 (↑m + 1))
(fun (x : CKN.Vec 3) => f n (x, t) i) fun (x : CKN.Vec 3) => Df n (x, t) i) ∧ (∃ G < ⊤,
∀ (n : ℕ),
N ≤ n →
∫⁻ (t : ℝ) in Set.Icc (-(↑m + 1)) 0, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (↑m + 1), ENNReal.ofReal (CKN.spatialGradientSq (f n) (Df n) (x, t)) ≤ G) ∧ ∀ (C : Set CKN.Foundation.Parabolic.Vec3),
IsCompact C →
C ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (↑m + 1) →
∀ (a b : ℝ),
Set.Icc a b ⊆ Set.Icc (-(↑m + 1)) 0 →
∀ (w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.L2Vec3),
ContDiff ℝ (↑⊤) w →
HasCompactSupport w →
tsupport w ⊆ C →
∃ (A : ℝ) (B : ℝ) (θ : ℝ),
0 ≤ A ∧ 0 ≤ B ∧ 0 < θ ∧ ∀ (n : ℕ),
N ≤ n →
∀ (s t : ℝ),
s ∈ Set.Icc a b →
t ∈ Set.Icc a b →
|(∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f n (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ)
:
∃ (φ : ℕ → ℕ),
StrictMono φ ∧ ∃ (U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3),
Measurable U ∧ ∃ (DU : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3),
Measurable DU ∧ (∀ t < 0,
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, U (x, t) i * ψ x i)
MeasureTheory.volume ∧ Filter.Tendsto
(fun (k : ℕ) => ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (φ k) (x, t) i * ψ x i)
Filter.atTop
(nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, U (x, t) i * ψ x i))) ∧ (∀ (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)),
IsCompact Q →
Q ⊆ Set.univ ×ˢ Set.Iio 0 →
Filter.Tendsto
(fun (k : ℕ) =>
MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f (φ k) z - U z) 2
(MeasureTheory.volume.restrict Q))
Filter.atTop (nhds 0)) ∧ (∀ (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)),
IsCompact Q →
Q ⊆ Set.univ ×ˢ Set.Iio 0 →
∀ (i j : Fin 3) (w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ),
MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict Q) →
Filter.Tendsto
(fun (k : ℕ) => ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Q, Df (φ k) z i j * w z)
Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in Q, DU z i j * w z))) ∧ (∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Iio 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => U (x, t) i) fun (x : CKN.Vec 3) =>
DU (x, t) i) ∧ ∀ (Q : Set (CKN.Foundation.Parabolic.Vec3 × ℝ)),
IsCompact Q →
Q ⊆ Set.univ ×ˢ Set.Iio 0 → MeasureTheory.MemLp DU 2 (MeasureTheory.volume.restrict Q)
Diagonal compactness for sequences that are uniformly controlled on each
fixed bounded past cylinder from a stage-dependent index on
(prop:blowup-limit, via lem:compactness of the CKN manuscript).