Stagewise bounds for the rescaled trace #
For the blow-up sequence of prop:blowup-limit built from the trace
representative: a measurable choice of the source gradient, agreement of
the rescaled trace with the zero-extended rescaled velocity on fixed
cylinders, the local gradient energy bound from the local energy step, and
the uniform compact slice bound.
theorem
ESS.blowupLimitAssembly_exists_measurable_version
{β : Type u_1}
[TopologicalSpace β]
[Zero β]
[MeasurableSpace β]
[BorelSpace β]
[TopologicalSpace.PseudoMetrizableSpace β]
{F : CKN.Foundation.Parabolic.ParabolicPoint → β}
(hF :
MeasureTheory.AEStronglyMeasurable F
(MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))))
:
∃ (Fm : CKN.Foundation.Parabolic.ParabolicPoint → β),
Measurable Fm ∧ F =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))] Fm ∧ goodPointDomain.indicator Fm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator F
A field that is almost everywhere strongly measurable on the source cylinder has a measurable version whose zero extension agrees almost everywhere with its own.
theorem
ESS.blowupLimitAssembly_blowupGradient_ae_eq
{Du Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hDmEq : goodPointDomain.indicator Dm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator Du)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r : ℝ)
(hr : 0 < r)
:
blowupGradient x₀ t₀ r Dm =ᵐ[MeasureTheory.volume] blowupGradient x₀ t₀ r Du
Almost-everywhere equal zero extensions have almost-everywhere equal blow-up gradients.
theorem
ESS.blowupLimitAssembly_trace_ae_eq_blowupVelocity
{u um : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hum : Measurable um)
(hu :
u =ᵐ[MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))] um)
(W : CKN.Foundation.Parabolic.Vec3 × ↑(Set.Icc (-(3 / 4) ^ 2) 0) → CKN.Foundation.Parabolic.Vec3)
(hW : Measurable W)
(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))
{x₀ : CKN.Foundation.Parabolic.Vec3}
(hx₀ : CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ ≤ 1 / 2)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
{r R a : ℝ}
(hr : 0 < r)
(hrR : r * R < 1 / 4)
(hra : r ^ 2 * -a < 1 / 4)
:
blowupLimitTraceRescaling W x₀ t₀
r =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball 0 R ×ˢ Set.Ioo a 0)]
blowupVelocity x₀ t₀ r u
The rescaled trace agrees almost everywhere with the zero-extended rescaled velocity on every fixed past cylinder at small scales.
theorem
ESS.measurable_blowupLimitAssembly_blowupGradient
{Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hDm : Measurable Dm)
(x₀ : CKN.Foundation.Parabolic.Vec3)
(t₀ r : ℝ)
:
Measurable (blowupGradient x₀ t₀ r Dm)
The rescaled measurable gradient is measurable.
theorem
ESS.blowupLimitAssembly_trace_gradient_energy
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
{Du Dm : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hDm : Measurable Dm)
(hDmEq : goodPointDomain.indicator Dm =ᵐ[MeasureTheory.volume] goodPointDomain.indicator Du)
{x₀ : CKN.Foundation.Parabolic.Vec3}
(hx₀ : CKN.Foundation.Parabolic.vec3EuclideanNorm x₀ ≤ 1 / 2)
{t₀ : ℝ}
(ht₀ : t₀ ∈ Set.Icc (-(1 / 4)) 0)
{r R : ℝ}
(hr : 0 < r)
(hR : 0 < R)
(hrR : r * R < 1 / 4)
(hrR2 : r ^ 2 * R < 3 / 4)
(f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3)
(C : ℝ)
(hint :
MeasureTheory.IntegrableOn
(fun (z : CKN.Foundation.Parabolic.ParabolicPoint) =>
CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) z)
(CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo (-R) 0)) MeasureTheory.volume)
(hbound :
2 * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.euclideanBall 0 R) (Set.Ioo (-R) 0), CKN.spatialGradientSq (parabolicRescaleVelocity x₀ t₀ r u) (parabolicRescaleGradient x₀ t₀ r Du) z ≤ C)
:
∫⁻ (t : ℝ) in Set.Icc (-R) 0, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in CKN.Foundation.Parabolic.vec3Ball 0 R, ENNReal.ofReal (CKN.spatialGradientSq f (blowupGradient x₀ t₀ r Dm) (x, t)) ≤ ENNReal.ofReal (C / 2)
The local gradient energy of the rescaled measurable gradient on a fixed ball and past time interval is bounded by the rescaled local energy estimate.
theorem
ESS.blowupLimitAssembly_trace_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)
(t₀ : ℝ)
(r : ℕ → ℝ)
(hr : ∀ (n : ℕ), 0 < r n)
(C : Set CKN.Foundation.Parabolic.Vec3)
(hC : IsCompact C)
:
∃ M' < ⊤,
∀ (n : ℕ) (t : ℝ),
∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in C, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (blowupLimitTraceRescaling W x₀ t₀ (r n) (x, t))) ^ 2 ≤ M'
Every rescaled trace slice has a uniform local L² bound on each compact set, for all scales and all times.