Fixed jointly measurable pressure decomposition on an inner ball

One pressure field and two matrices of completed Riesz representatives are chosen from suitability. Their measurable remainder represents the classical harmonic and far-force gradient on almost every slice of the target carrier.

Identification of one measurable pressure remainder

The same selected pressure derivative is decomposed into completed Riesz fields and a measurable remainder. Weak derivative uniqueness identifies that remainder with the classical harmonic and far-force gradient on slices.

theorem CKN.Core.Step4.ae_fixed_remainder_eq_classical_gradient {Ω : 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) {J : Set ℝ} (hJ : MeasurableSet J) (hJsub : J ⊆ Set.Ioc (z.2 - ρ ^ 2) z.2) {Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hDp : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) {T F : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ} (hT : ∀ (j i : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j i (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff z.1 hρ) (spatialDeriv (mollifiedBallCutoff z.1 hρ)) u Du (sourceSliceCentredMean z.1 ρ u) w j) (y, s)) (hF : ∀ (j i : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => F j i (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => mollifiedBallCutoff z.1 hρ w.1 * f w j) (y, s)) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i + ∑ j : Fin 3, T j i (y, s) - ∑ j : Fin 3, F j i (y, s)) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 (ρ / 2))] fun (y : Foundation.Parabolic.Vec3) => classicalGradient (harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) y i

The algebraically defined remainder of a fixed weak pressure gradient agrees with the smooth harmonic and far-force remainder on almost every slice.

theorem CKN.Core.Step4.closure_fixed_pressure_cylinder_subset_doubled_ball (z₀ : Foundation.Parabolic.ParabolicPoint) {R : ℝ} (hR : 0 < R) : closure (Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) R) ⊆ Metric.ball z₀ (2 * R)

The fixed radius localization with shifted top time lies in the doubled parabolic ball containing the suitable solution.

theorem CKN.Core.Step4.exists_measurable_fixed_pressure_decomposition_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) {R : ℝ} (hR : 0 < R) (hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I) : have η := mollifiedBallCutoff z₀.1 hR; have c := sourceSliceCentredMean z₀.1 R u; have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du c; have Q := Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) R; have J := Set.Ioo (z₀.2 - R ^ 2 / 4) (z₀.2 + R ^ 2 / 4); ∃ (Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (T : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (Tforce : Fin 3 → Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ) (H : Fin 3 → Foundation.Parabolic.ParabolicPoint → ℝ), Measurable Dp ∧ (∀ (j i : Fin 3), Measurable (T j i)) ∧ (∀ (j i : Fin 3), Measurable (Tforce j i)) ∧ (∀ (i : Fin 3), Measurable (H i)) ∧ (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball z₀.1 (R / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z₀.1 (R / 2)) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) ∧ (∀ (j i : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => T j i (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => Q.indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => V w j) (y, s)) ∧ (∀ (j i : Fin 3), ∀ᵐ (s : ℝ), (fun (y : Foundation.Parabolic.Vec3) => Tforce j i (y, s)) =ᵐ[MeasureTheory.volume] Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ fun (y : Foundation.Parabolic.Vec3) => Q.indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => η w.1 * f w j) (y, s)) ∧ (∀ (i : Fin 3) (w : Foundation.Parabolic.ParabolicPoint), Dp w i = -∑ j : Fin 3, T j i w + H i w + ∑ j : Fin 3, Tforce j i w) ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict J, ∀ (i : Fin 3), (fun (y : Foundation.Parabolic.Vec3) => H i (y, s)) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z₀.1 (R / 2))] fun (y : Foundation.Parabolic.Vec3) => classicalGradient (harmonicPressurePart η u c p s + pressureP8 η f s) y i

Suitability yields a single measurable weak pressure gradient and its fixed signed completed-Riesz decomposition, with a measurable remainder identified with the classical harmonic and far-force gradient on slices.