The stagewise hypotheses for the blow-up sequence #
For the blow-up sequence of prop:blowup-limit, built from the trace
representative of lem:weak-cont-L3, each fixed bounded past cylinder has,
from some index on, weak spatial gradients on the time slices, a uniform
local gradient energy bound (the local energy step), and a uniform pairing
modulus (the pairing-modulus step). These are the stagewise hypotheses of
blowupLimitAssembly_exhaustion_compactness.
theorem
ESS.blowupLimitAssembly_trace_indicator_bound
(v :
↑(Set.Icc (-(3 / 4) ^ 2) 0) →
↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)))))
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(M : ℝ)
(hvbound : ∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)), ‖v t‖ ≤ M)
(hW :
∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x))
(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
The weakly continuous trace, as a pointwise representative extended by zero, has global L³ slices bounded by the trace bound.
theorem
ESS.blowupLimitAssembly_trace_stages
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hu :
MeasureTheory.AEStronglyMeasurable u
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hDu :
MeasureTheory.AEStronglyMeasurable Du
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hp :
MeasureTheory.AEStronglyMeasurable p
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL2 :
essSup
(fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ‖u (x, t)‖ₑ ^ 2)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(henergy :
∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤)
(hpLp :
MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2))
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
(hL3 :
essSup
(fun (t : ℝ) =>
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3)
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0)) < ⊤)
(hgrad :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3),
CKN.HasWeakGradientOn (CKN.Foundation.Parabolic.vec3Ball 0 1) (fun (x : CKN.Vec 3) => u (x, t) i)
fun (x : CKN.Vec 3) => Du (x, t) i)
(hS2 :
∀ ψ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ∑ i : Fin 3, u z i * CKN.spatialPartial ψ i z = 0)
(hS3 :
∀ φ ∈ CKN.spaceTimeTestFunction (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0),
∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), -∑ i : Fin 3, u z i * CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) z - ∑ i : Fin 3,
∑ j : Fin 3,
u z i * u z j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z + ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) j z - p z * ∑ i : Fin 3, CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => φ y i) i z - ∑ i : Fin 3, 0 z i * φ z i = 0)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ : ℝ)
(r : ℕ → ℝ)
(hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2)))
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
(hr : ∀ (k : ℕ), 0 < r k)
(hr0 : Filter.Tendsto r Filter.atTop (nhds 0))
(v :
↑(Set.Icc (-(3 / 4) ^ 2) 0) →
↥(MeasureTheory.Lp CKN.Foundation.Parabolic.L2Vec3 3
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)))))
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(hWmeas : Measurable W)
(hW :
∀ (t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, t)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => CKN.weakContL3OfLp (↑↑(v t) x))
(htrace :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-(3 / 4) ^ 2) 0), ∃ (ht : t ∈ Set.Icc (-(3 / 4) ^ 2) 0),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
W (x, ⟨t, ht⟩)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4))]
fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t))
(hsourceFormula :
∀ (ψ : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
tsupport ψ ⊆ CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4) →
∀ (s t : ↑(Set.Icc (-(3 / 4) ^ 2) 0)),
(∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v t) y).ofLp i * ψ y i) - ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4), ∑ i : Fin 3, (↑↑(v s) y).ofLp i * ψ y i = ∫ (τ : ℝ) in ↑s..↑t, ∫ (y : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 1, ∑ i : Fin 3,
∑ j : Fin 3,
u (y, τ) i * u (y, τ) j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y - ∑ i : Fin 3,
∑ j : Fin 3,
Du (y, τ) i j * CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) j y + p (y, τ) * ∑ i : Fin 3, CKN.spatialDeriv (fun (z : CKN.Foundation.Parabolic.Vec3) => ψ z i) i y)
(Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3)
(hDm : Measurable Dm)
(hDmEq : goodPointDomain.indicator Dm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator Du)
(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) => blowupLimitTraceRescaling W x₀ t₀ (r n) (x, t) i) fun (x : CKN.Vec 3) =>
blowupGradient x₀ t₀ (r n) Dm (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 (blowupLimitTraceRescaling W x₀ t₀ (r n)) (blowupGradient x₀ t₀ (r n) Dm)
(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,
blowupLimitTraceRescaling W x₀ t₀ (r n) (x, t) i * (w x).ofLp i) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3,
blowupLimitTraceRescaling W x₀ t₀ (r n) (x, s) i * (w x).ofLp i| ≤ A * dist t s + B * dist t s ^ θ
The blow-up sequence built from the trace representative satisfies the stagewise hypotheses of the exhaustion compactness theorem.