Harmonic Remainder Force Terms #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.pressure_force_memLp_and_lpNorm_growth_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), (∀ (R : ℝ),
0 < R →
MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R))) ∧ 0 ≤ Foundation.Euclidean.pressureP7GrowthConstant (mollifiedBallCutoff z.1 hρ) f s
(Foundation.Parabolic.vec3EuclideanNorm z.1 + ρ) + Foundation.Euclidean.pressureP8GrowthConstant (mollifiedBallCutoff z.1 hρ) f s
(Foundation.Parabolic.vec3EuclideanNorm z.1 + ρ) ∧ ∀ (R : ℝ),
0 < R →
MeasureTheory.lpNorm
(pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R)) ≤ (Foundation.Euclidean.pressureP7GrowthConstant (mollifiedBallCutoff z.1 hρ) f s
(Foundation.Parabolic.vec3EuclideanNorm z.1 + ρ) + Foundation.Euclidean.pressureP8GrowthConstant (mollifiedBallCutoff z.1 hρ) f s
(Foundation.Parabolic.vec3EuclideanNorm z.1 + ρ)) * (1 + R)
The force potentials have the local membership and linear growth required by the force-cancellation theorem, for almost every slice of a suitable weak solution.