Blowup H1 Slices #
Spatial Sobolev slice bounds for the rescaled endpoint sequence.
theorem
ESS.blowup_memLp_two_of_energy
{E : Type u_1}
[NormedAddCommGroup E]
{S : Set CKN.Foundation.Parabolic.ParabolicPoint}
{v : CKN.Foundation.Parabolic.ParabolicPoint → E}
(hv : MeasureTheory.AEStronglyMeasurable v (MeasureTheory.volume.restrict S))
(hfinite : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in S, ‖v z‖ₑ ^ 2 < ⊤)
:
A measurable field with finite squared energy belongs to local L².
theorem
ESS.blowup_h1_slices_of_data
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{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 → ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hdata : CKN.IsSuitableWeakSolutionData Ω I q u Du p f)
{Ω' : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : CKN.localBox Ω I Ω' J)
{x₀ : CKN.Foundation.Parabolic.Vec3}
{r : ℝ}
(hball : CKN.Foundation.Parabolic.vec3Ball x₀ r ⊆ Ω')
(i : Fin 3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∃ (v : CKN.H1Function (CKN.Foundation.Parabolic.vec3Ball x₀ r)),
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
u (x, s) i) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r)]
v.toFun ∧ (fun (x : CKN.Foundation.Parabolic.Vec3) =>
Du (x, s) i) =ᵐ[MeasureTheory.volume.restrict (CKN.Foundation.Parabolic.vec3Ball x₀ r)]
v.grad
Each component of a suitable velocity has an H¹ representative on almost every spatial ball slice of a local box.