Critical scaling in the fixed pressure split

The velocity and whole-space pressure have invariant critical slice masses. The harmonic remainder has vanishing mixed supremum mass on each bounded spatial region under rescaling.

theorem ESS.pressureSplitRieszPressure_essSup_slice_bound {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict pressureSplitDomain)) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict pressureSplitDomain)) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict pressureSplitTime) < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, ∀ (i : Fin 3), CKN.HasWeakGradientOn pressureSplitBall (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) : let F := CKN.pressureSplitTensor u; have hF := ⋯; essSup (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => pressureSplitRieszPressure F hF (x, t)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (MeasureTheory.volume.restrict pressureSplitTime) ≤ ENNReal.ofReal (CKN.Leray.rieszPressureOperatorBound (3 / 2) pressureSplitRieszPressure_essSup_slice_bound._proof_1 * (9 * pressureSplitVelocityLpBound u ^ 2))

The fixed whole-space pressure has the claimed essentially uniform spatial L^(3/2) bound on the source time interval.

theorem ESS.pressureSplit_rescaled_critical_slice_masses {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {p₁ : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict pressureSplitDomain)) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict pressureSplitTime) < ⊤) (hp₁ : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => p₁ (x, s)) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume) (x₀ : CKN.Foundation.Parabolic.Vec3) (t₀ r : ℝ) (hr : 0 < r) : ∀ᵐ (t : ℝ), ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (parabolicRescaleVelocity x₀ t₀ r (goodPointDomain.indicator u) (x, t))) ^ 3 = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (goodPointDomain.indicator u (CKN.Foundation.Parabolic.parabolicHomeomorph.symm (y, CKN.scalingTime r t₀ t)))) ^ 3 ∧ ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |parabolicRescalePressure x₀ t₀ r (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => (Set.Ioo (-1) 0).indicator (fun (s : ℝ) => p₁ (z.1, s)) z.2) (x, t)| ^ (3 / 2) = ∫⁻ (y : CKN.Foundation.Parabolic.Vec3), ENNReal.ofReal |(Set.Ioo (-1) 0).indicator (fun (s : ℝ) => p₁ (y, s)) (CKN.scalingTime r t₀ t)| ^ (3 / 2)

The critical velocity and whole-space pressure slice masses are invariant under the parabolic rescaling of the fixed pressure split.

theorem ESS.pressureSplit_remainder_mixed_sup_norm_tendsto_zero {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 pressureSplitDomain)) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict pressureSplitDomain)) (hpmeas : MeasureTheory.AEStronglyMeasurable p (MeasureTheory.volume.restrict pressureSplitDomain)) (hL2 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ‖u (x, t)‖ₑ ^ 2) (MeasureTheory.volume.restrict pressureSplitTime) < ⊤) (henergy : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hp : MeasureTheory.MemLp p (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict pressureSplitDomain)) (hL3 : essSup (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3) in pressureSplitBall, ENNReal.ofReal (CKN.Foundation.Parabolic.vec3EuclideanNorm (u (x, t))) ^ 3) (MeasureTheory.volume.restrict pressureSplitTime) < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict pressureSplitTime, ∀ (i : Fin 3), CKN.HasWeakGradientOn pressureSplitBall (fun (x : CKN.Vec 3) => u (x, t) i) fun (x : CKN.Vec 3) => Du (x, t) i) (hdiv : ∀ χ ∈ CKN.spaceTimeTestFunction pressureSplitBall pressureSplitTime, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, ∑ i : Fin 3, u z i * CKN.spatialPartial χ i z = 0) (hMomentum : ∀ φ ∈ CKN.spaceTimeTestFunction pressureSplitBall pressureSplitTime, ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in pressureSplitDomain, -∑ 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) (x₀ : CKN.Foundation.Parabolic.Vec3) (hx₀ : x₀ ∈ closure (CKN.Foundation.Parabolic.vec3Ball 0 (1 / 2))) (t₀ : ℝ) {Ω : Set CKN.Foundation.Parabolic.Vec3} (hΩmeas : MeasurableSet Ω) (hΩbounded : Bornology.IsBounded Ω) (r : ℕ → ℝ) (hr : ∀ (k : ℕ), 0 < r k) (hr0 : Filter.Tendsto r Filter.atTop (nhds 0)) : let F := CKN.pressureSplitTensor u; have hF := ⋯; have p₁ := pressureSplitRieszPressure F hF; have p₂ := pressureSplitRemainder p p₁; Filter.Tendsto (fun (k : ℕ) => (∫⁻ (t : ℝ), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => parabolicRescalePressure x₀ t₀ (r k) (goodPointDomain.indicator p₂) (x, t)) ⊤ (MeasureTheory.volume.restrict Ω) ^ (3 / 2)) ^ (2 / 3)) Filter.atTop (nhds 0)

The mixed L^(3/2) supremum norm expression of the rescaled fixed harmonic remainder tends to zero on every bounded measurable spatial region.