Interior regularity of the harmonic pressure part on a slice

The harmonic summand p₂ + p₃ + p₄ + p₅ + p₆ of the local pressure decomposition eq:pk is a Newtonian potential whose density is carried by the cutoff annulus B_{3ρ/4}(x₀) \ B_{13ρ/20}(x₀). On the inner ball B_{ρ/2}(x₀) the kernel is therefore smooth in the evaluation point, and the potential inherits every finite order of differentiability (eq:har-Ck).

This file records the order-one consequence in the almost-every-time form that display (3.5) of the pressure-gradient section consumes: for a suitable weak solution and almost every time of the one-sided interval J_ρ, the harmonic pressure part is C¹ on B_{ρ/2}(x₀), so its weak gradient there is its classical gradient.

theorem CKN.Core.Step4.contDiffOn_harmonicPressurePart_of_terms {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} {B : Set Foundation.Parabolic.Vec3} (h2 : ContDiffOn ℝ (↑1) (pressureP2 η u c s) B) (h3 : ContDiffOn ℝ (↑1) (pressureP3 η u c s) B) (h4 : ContDiffOn ℝ (↑1) (pressureP4 η u c s) B) (h5 : ContDiffOn ℝ (↑1) (pressureP5 η p s) B) (h6 : ContDiffOn ℝ (↑1) (pressureP6 η p s) B) : ContDiffOn ℝ (↑1) (harmonicPressurePart η u c p s) B

The five annular potentials of the local pressure decomposition are each C¹ on the inner ball, hence so is their sum.

theorem CKN.Core.Step4.slice_harmonic_part_contDiffOn_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), ContDiffOn ℝ (↑1) (harmonicPressurePart (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 s) (euclideanBall z.1 (ρ / 2))

Almost every slice of the harmonic pressure part of a suitable weak solution is C¹ on the inner ball B_{ρ/2}(x₀). This is eq:har-Ck at order one, in the shape display (3.5) consumes.