The pressure-gradient field on the origin carrier

Display eq:pressure-gradient-morrey selects, for almost every time of the solution interval, a weak spatial gradient of the pressure slice on a ball around the origin, together with its L^{6/5} bound on a smaller ball. The one-sided estimate prop:bootstrap consumes a single space-time field with three properties: joint measurability on the carrier, integrability on every compactly interior box, and the space-time integration-by-parts identity against test functions supported in the carrier.

This module performs that passage. The selection is made on each member of a compact exhaustion of the time interval and the resulting fields are glued; the field is then cut off outside the spatial ball of the carrier, which changes neither the pairing identity, since the test functions vanish there, nor the slice bounds. The output also records the identification of the field with every slice weak gradient, which is what pins it almost everywhere.

theorem CKN.Core.Step4.originClauseRestrict_prod_eq (S : Set Foundation.Parabolic.Vec3) (T : Set ℝ) : MeasureTheory.volume.restrict (S ×ˢ T) = (MeasureTheory.volume.restrict S).prod (MeasureTheory.volume.restrict T)

The restriction of the space-time volume to a product box is the product of the restrictions.

theorem CKN.Core.Step4.exists_originClause_pressure_gradient_field {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q R₀ 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} {K : Fin 3 → ℝ → ENNReal} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hR₁ : 0 < R₁) (hR₁R₀ : R₁ < R₀) (hR₀ : R₀ < 3 / 4) (hslice : ∀ (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 ∧ MeasureTheory.eLpNorm g (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)) ≤ K k t) (hKtop : ∀ (k : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, K k t ≠ ⊤) (hKint : ∀ (k : Fin 3) (T : Set ℝ), IsCompact (closure T) → closure T ⊆ I → MeasureTheory.Integrable (fun (t : ℝ) => (K k t).toReal) (MeasureTheory.volume.restrict T)) : ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3), (∀ (i : Fin 3), AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I))) ∧ (∀ (U : Set Foundation.Parabolic.Vec3) (T : Set ℝ), localBox Ω I U T → U ⊆ Foundation.Parabolic.vec3Ball 0 R₁ → ∀ (i : Fin 3), MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i) (MeasureTheory.volume.restrict (spaceTimeSet U T))) ∧ (∀ (i : Fin 3), ∀ ψ ∈ spaceTimeTestFunction Set.univ Set.univ, tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I → ∫ (z : Foundation.Parabolic.ParabolicPoint), p z * spatialPartial ψ i z = -∫ (z : Foundation.Parabolic.ParabolicPoint), Dp z i * ψ z) ∧ (∀ (i : 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₀) i (fun (x : Vec 3) => p (x, t)) g → (fun (x : Foundation.Parabolic.Vec3) => Dp (x, t) i) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)] g) ∧ (∀ (i : Fin 3), ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict I, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => Dp (x, t) i) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball 0 R₁)) ≤ K i t) ∧ ∀ z ∉ Foundation.Parabolic.vec3Ball 0 R₁ ×ˢ I, Dp z = 0

The space-time field of display eq:pressure-gradient-morrey on the origin carrier vec3Ball 0 R₁ ×ˢ I. From slice weak gradients on the ball of radius R₀ with an L^{6/5} majorant K on the ball of radius R₁, integrable on every compactly interior time window, one obtains a single field with the measurability, integrability and pairing properties consumed by the one-sided estimate, identified almost everywhere with the slice gradients and vanishing off the carrier.