Interior collars for the origin pressure decomposition #
The half-gap collar stays inside the outer data cylinder for every centre in the closed inner carrier, so the actual pressure gradient admits the raw-source decomposition on that collar.
theorem
CKN.Core.Step4.half_gap_collar_closure_subset_outer
{R₀ R₁ : ℝ}
(hR₁ : 0 < R₁)
(hgap : R₁ < R₀)
{z : Foundation.Parabolic.ParabolicPoint}
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
:
closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ((R₀ - R₁) / 2)) ⊆ Foundation.Parabolic.parabolicCylinder 0 0 R₀
The closed half-gap collar lies in the outer open-backward cylinder.
theorem
CKN.Core.Step4.half_gap_ball_subset_outer
{R₀ R₁ : ℝ}
(hR₁ : 0 < R₁)
(hgap : R₁ < R₀)
{z : Foundation.Parabolic.ParabolicPoint}
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
:
Foundation.Parabolic.vec3Ball z.1 ((R₀ - R₁) / 2) ⊆ Foundation.Parabolic.vec3Ball 0 R₀
The spatial half-gap ball stays inside the outer data ball.
theorem
CKN.Core.Step4.ae_actual_pressure_eq_raw_riesz_half_gap_collar
(R₀ R₁ : ℝ)
(hR₁ : 0 < R₁)
(hgap : 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}
{r : ℝ}
(hr : 0 < r)
(hcell : r ≤ (R₀ - R₁) / 4)
(hz : z ∈ closure (Foundation.Parabolic.parabolicCylinder 0 0 R₁))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - r ^ 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 r ∩ Foundation.Parabolic.vec3Ball 0 R₁)]
fun (x : Foundation.Parabolic.Vec3) =>
-∑ j : Fin 3, T j i (x, s) + rawCorrectedPressureRemainder R₀ z ⋯ u Du p f i (x, s)
The actual pressure gradient has the raw-source decomposition using the interior half-gap collar.