Four-term identification on interior collars #
theorem
CKN.Core.Step4.ae_actual_pressure_eq_four_terms_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) =>
have hρ := ⋯;
have η := mollifiedBallCutoff z.1 hρ;
have c := sourceSliceCentredMean z.1 ((R₀ - R₁) / 2) u;
-∑ j : Fin 3, T j i (x, s) + classicalGradient (harmonicPressurePart η u c p s) x i + gapForceIncrement z hρ u p f i (x, s) - ∑ j : Fin 3,
Foundation.Euclidean.rieszSecondGradientExtensionOperator (Foundation.Euclidean.rieszSecondL2Input j i) ⋯
(centredRawSourceCorrection (Foundation.Parabolic.vec3Ball 0 R₀) η (spatialDeriv η)
(fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (fun (y : Foundation.Parabolic.Vec3) => f (y, s))
(fun (y : Foundation.Parabolic.Vec3) => Du (y, s)) (c s) j)
x
The actual weak pressure derivative is the signed raw Riesz sum, harmonic derivative, force increment, and signed centred-source correction.