Time integration of the local pressure norm #
Tonelli converts the time integral of the spatial L^(3/2) pressure norm
into its space-time integral (lem:pressure-split).
theorem
ESS.blowupScalarTimeThreeHalves_eq
{Ω : Set CKN.Foundation.Parabolic.Vec3}
{J : Set ℝ}
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hp :
MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2))
((MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)))
:
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) (3 / 2)
(MeasureTheory.volume.restrict Ω) ^ (3 / 2) = ∫⁻ (z : CKN.Foundation.Parabolic.Vec3 × ℝ), ENNReal.ofReal |p z| ^ (3 / 2) ∂(MeasureTheory.volume.restrict Ω).prod (MeasureTheory.volume.restrict J)
The time integral of the spatial L^(3/2) norm power equals the
space-time L^(3/2) mass.
theorem
ESS.pressureSlice_memLp_ae
{J : Set ℝ}
(p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hp :
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p (z.1, z.2)) (3 / 2)
((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict J)))
:
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, t)) (3 / 2)
(MeasureTheory.volume.restrict (CKN.euclideanBall 0 1))
A space-time L^(3/2) pressure has L^(3/2) spatial slices at almost
every time.
theorem
ESS.blowupHarmonicPressure_bound
{J : Set ℝ}
(p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hp₂ :
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2)
((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict J)))
(hharm :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict J, CKN.Foundation.Heat.WeaklyHarmonicOn (CKN.euclideanBall 0 1) fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t))
:
∃ C < ⊤,
∫⁻ (t : ℝ) in J, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, t)) ⊤
(MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4))) ^ (3 / 2) ≤ C * MeasureTheory.eLpNorm (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2)
((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict J)) ^ (3 / 2)
Integrable harmonic pressure slices have an interior time-integrated supremum bound.
theorem
ESS.blowupHarmonicPressure_global_sup_integrable
(p₂ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
(hp₂ :
MeasureTheory.MemLp (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => p₂ (z.1, z.2)) (3 / 2)
((MeasureTheory.volume.restrict (CKN.euclideanBall 0 1)).prod (MeasureTheory.volume.restrict (Set.Ioo (-1) 0))))
(hharm :
∀ᵐ (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))
:
∫⁻ (t : ℝ), (Set.Ioo (-1) 0).indicator
(fun (s : ℝ) =>
MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => p₂ (x, s)) ⊤
(MeasureTheory.volume.restrict (CKN.euclideanBall 0 (3 / 4))))
t ^ (3 / 2) < ⊤
The harmonic interior supremum, extended by zero in time, has finite
L^(3/2) mass on the whole time line.