Identification of the prescribed weak pressure gradient on clipped cells

The pressure gradient is the one supplied by the consumer. Uniqueness of locally integrable weak derivatives identifies it on the intersection of the consumer carrier and the local pressure ball, on one common time set.

theorem CKN.Core.Step4.ae_actual_pressure_eq_centred_decomposition_on_clipped_cell {Ω : 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 Dp : 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) (hDp : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) (J : Set ℝ) : have η := mollifiedBallCutoff z.1 hρ; have c := sourceSliceCentredMean z.1 ρ u; have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du c; ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2 ∩ J), ∀ (i : Fin 3), (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 (ρ / 2) ∩ Foundation.Parabolic.vec3Ball 0 R₁)] fun (x : Foundation.Parabolic.Vec3) => -∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => V (y, s) j) x + classicalGradient (harmonicPressurePart η u c p s + pressureP8 η f s) x i + ∑ j : Fin 3, Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯ (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x

The actual prescribed weak pressure gradient has the fixed signed centred-source decomposition on each clipped cell and time intersection.

theorem CKN.Core.Step4.raw_divergence_source_memLp_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), ∀ (j : Fin 3), MeasureTheory.MemLp ((Foundation.Parabolic.vec3Ball z.1 ρ).indicator fun (y : Foundation.Parabolic.Vec3) => ∑ k : Fin 3, Du (y, s) j k * u (y, s) k - f (y, s) j) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume

Suitability supplies the raw localized divergence source's operator-domain regularity on almost every slice of its cylinder.

noncomputable def CKN.Core.Step4.rawCorrectedPressureRemainder (R₀ : ℝ) (z : Foundation.Parabolic.ParabolicPoint) {ρ : ℝ} (hρ : 0 < ρ) (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) (i : Fin 3) (w : Foundation.Parabolic.ParabolicPoint) : ℝ

The explicit complementary gradient after replacing the centred source by the raw source on the outer origin ball.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.Core.Step4.ae_actual_pressure_eq_raw_riesz_corrected_on_clipped_cell (R₀ R₁ : ℝ) (hR₁ : 0 < R₁) (hR₁₀ : R₁ ≤ R₀) (hR₀one : R₀ ≤ 1) {Ω : 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 Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) (hdom : closure (Foundation.Parabolic.parabolicCylinder 0 0 1) ⊆ spaceTimeSet Ω I) (hDp : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∀ (i : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) (Foundation.Parabolic.vec3Ball 0 R₁) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball 0 R₁) i (fun (y : Vec 3) => p (y, s)) fun (y : Vec 3) => Dp (y, s) i) (T : 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 0 0 R₀).indicator (fun (w : Foundation.Parabolic.ParabolicPoint) => ∑ k : Fin 3, Du w j k * u w k - f w j) (y, s)) {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) ^ 2) z.2 ∩ Set.Ioc (-R₁ ^ 2) 0), ∀ (i : Fin 3), (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i) =ᵐ[MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball z.1 (ρ / 2) ∩ Foundation.Parabolic.vec3Ball 0 R₁)] fun (x : Foundation.Parabolic.Vec3) => -∑ j : Fin 3, T j i (x, s) + rawCorrectedPressureRemainder R₀ z hρ u Du p f i (x, s)

The consumer's actual weak pressure gradient equals the selected raw Riesz field plus the explicit complementary gradient on almost every slice of each clipped cell. No quantitative estimate or choice of Dp is assumed.