Blowup Ten Thirds #
Space-time integrability of the rescaled velocity at exponent 10/3.
theorem
ESS.blowup_uniform_tenThirds_scalar
(x₀ : CKN.Foundation.Parabolic.Vec3)
(r : ℝ)
(hr : 0 < r)
(J : Set ℝ)
(hJ : J.OrdConnected)
(g : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(Dg : ℕ → CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3)
(hgm :
∀ (k : ℕ),
MeasureTheory.AEStronglyMeasurable (g k)
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)))
(hDgm :
∀ (k : ℕ),
MeasureTheory.AEStronglyMeasurable (Dg k)
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)))
(hSlice :
∀ (k : ℕ),
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : CKN.H1Function (CKN.Foundation.Parabolic.vec3Ball x₀ r)),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
g k (x, s)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r)]
v.toFun ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) =>
Dg k (x, s)) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r)]
v.grad)
(hg₂ :
∀ (k : ℕ), MeasureTheory.MemLp (g k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)))
(hDg₂ :
∀ (k : ℕ), MeasureTheory.MemLp (Dg k) 2 (MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)))
(A G : ENNReal)
(hA : A < ⊤)
(hG : G < ⊤)
(hAsup :
∀ (k : ℕ),
essSup
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g k (x, s)) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r)))
(MeasureTheory.volume.restrict J) ≤ A)
(hGsup :
∀ (k : ℕ),
MeasureTheory.eLpNorm
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.Foundation.Parabolic.vec3EuclideanNorm (Dg k z)) 2
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)) ≤ G)
(hJfin : MeasureTheory.volume J < ⊤)
:
∃ K < ⊤,
∀ (k : ℕ),
MeasureTheory.MemLp (g k) (ENNReal.ofReal (10 / 3))
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)) ∧ MeasureTheory.eLpNorm (g k) (ENNReal.ofReal (10 / 3))
(MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r ×ˢ J)) ^ (10 / 3) ≤ K
Uniform slice L² and gradient L² control gives a uniform
space-time L^(10/3) bound on a ball cylinder.