A measurable weak pressure gradient on an interior origin ball

The slice derivatives of eq:pressure-gradient-morrey have one measurable representative on the whole time interval. Its derivatives on all open subdomains share one exceptional set of times, as needed in prop:bootstrap.

Spatial pressure gradients from suitability

The local slice estimate eq:pressure-gradient-morrey applies to the centred tensor source constructed from a suitable weak solution. Spatial gluing then produces weak derivatives on the whole origin ball for almost every time in the solution interval, as required by prop:bootstrap.

theorem CKN.Core.Step4.origin_local_slice_gradient_ae_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), (∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ ∀ (k : Fin 3), HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D x k

A suitable solution has a spatial weak pressure gradient on almost every half-ball slice of each interior cylinder (eq:pressure-gradient-morrey).

theorem CKN.Core.Step4.origin_slice_gradient_ae_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR : 0 < R) (hRone : R < 1) (k : Fin 3) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, ∃ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g (Foundation.Parabolic.vec3Ball 0 R) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R) k (fun (x : Vec 3) => p (x, t)) g

Spatial gluing of the half-ball slice gradients in prop:bootstrap: the pressure has a weak partial derivative on the origin ball for almost every time of the entire solution interval.

theorem CKN.Core.Step4.origin_measurable_weak_gradient_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR : 0 < R) (hRone : R < 1) : ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), Measurable Dp ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) (Foundation.Parabolic.vec3Ball 0 R) MeasureTheory.volume ∧ (HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => Dp (x, s) k) ∧ ∀ (W : Set Foundation.Parabolic.Vec3), IsOpen W → W ⊆ Foundation.Parabolic.vec3Ball 0 R → ∀ (g : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.LocallyIntegrableOn g W MeasureTheory.volume → HasWeakPartialDerivOn W k (fun (x : Vec 3) => p (x, s)) g → (fun (x : Foundation.Parabolic.Vec3) => Dp (x, s) k) =ᵐ[MeasureTheory.volume.restrict W] g

Suitability supplies a measurable field whose slices are weak pressure derivatives on the interior ball, with uniqueness on every open subdomain.