Source data for the blow-up estimates #
The hypotheses of thm:ess-local give the source suitability and the fixed
pressure split data (lem:pressure-split) in the shapes used by the
blow-up estimates of prop:blowup-limit.
theorem
ESS.blowupLimitAssembly_source_pressure_data
{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))))
(hpmeas :
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)
:
have p₁ := pressureSplitRieszPressure (CKN.pressureSplitTensor u) ⋯;
CKN.IsSuitableWeakSolution (CKN.Foundation.Parabolic.vec3Ball 0 (3 / 4)) (Set.Ioo (-1) 0) 3 u Du p 0 ∧ MeasureTheory.AEStronglyMeasurable (goodPointDomain.indicator u) MeasureTheory.volume ∧ MeasureTheory.AEStronglyMeasurable p₁ (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo (-1) 0)) ∧ (∃ Mᵤ < ⊤,
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable
(fun (x : CKN.Foundation.Parabolic.Vec3) => goodPointDomain.indicator u (x, s)) MeasureTheory.volume ∧ MeasureTheory.eLpNorm
(fun (x : CKN.Foundation.Parabolic.Vec3) =>
CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (x, s)))
3 MeasureTheory.volume ≤ Mᵤ) ∧ (∃ Mₚ < ⊤,
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s))
MeasureTheory.volume ∧ MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (3 / 2)
MeasureTheory.volume ≤ Mₚ) ∧ MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2) - p₁ (z.1, z.2)) (3 / 2)
((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod
(MeasureTheory.volume.restrict (Set.Ioo (-1) 0))) ∧ ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) =>
p (x, t) - p₁ (x, t)
The source hypotheses give suitability on the inner cylinder, the measurability of the zero-extended velocity, and the pressure split data with the harmonic remainder written as p - p₁.