Identity #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.pressureSliceResidual
{Ω : Set Foundation.Parabolic.Vec3}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(ψ : Foundation.Parabolic.Vec3 → ℝ)
(s : ℝ)
:
The spatial pressure residual at a fixed time for a compactly supported test.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.pressureSliceResidual_locallyIntegrable
{Ω : 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}
(h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hψΩ : tsupport ψ ⊆ Ω)
:
The pressure residual is locally integrable on the time interval.
theorem
CKN.pressure_viscous_test_integral_zero
{Ω : 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}
(h : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{ψ : Foundation.Parabolic.Vec3 → ℝ}
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(hψΩ : tsupport ψ ⊆ Ω)
{θ : ℝ → ℝ}
(hθ : ContDiff ℝ (↑⊤) θ)
(hθc : HasCompactSupport θ)
(hθI : tsupport θ ⊆ I)
:
∫ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet Ω I, ∑ i : Fin 3,
∑ j : Fin 3,
Du z i j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureTestParabolic ψ θ w i) j z = 0
The viscous term of a separated pressure test has zero space-time integral.