The identification data on a parabolic cylinder #
The identification data for the leading local pressure, specialized to the
cut-off mollifiedBallCutoff z.1 hρ of the parabolic cylinder of radius ρ
about z and to the ball average of the velocity used as the subtracted
constant. The conclusion is stated on the cylinder's time interval, which is
the form the slice pressure estimates consume.
theorem
CKN.pressureP1_cz_identification_data_ae_of_sws_cylinder
{Ω : 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), (∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s x * spatialLaplacian ψ x)
MeasureTheory.volume →
∫ (x : Foundation.Parabolic.Vec3), pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s x * spatialLaplacian ψ x = pressureSecondPairing
(fun (i j : Fin 3) (x : Foundation.Parabolic.Vec3) =>
mollifiedBallCutoff z.1 hρ x * pressureUTensor u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
(x, s) i j)
ψ) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ),
ContDiff ℝ (↑⊤) ψ →
HasCompactSupport ψ →
MeasureTheory.Integrable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureP1 (mollifiedBallCutoff z.1 hρ) u
(fun (t : ℝ) (j : Fin 3) =>
⨍ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball z.1 ρ, u (y, t) j)
p f s x * spatialLaplacian ψ x)
MeasureTheory.volume
The Calderón--Zygmund identification data for the leading local pressure on
the parabolic cylinder of radius ρ about z: for almost every time of the
cylinder, the whole-space pairing identity and the pairing integrability hold
simultaneously for every compactly supported smooth spatial test function, with
tensor source the cut-off velocity tensor.