Display (3.5) on a slice, with the analytic slots discharged

Display (3.5) of the pressure-gradient section selects, for almost every time of the one-sided interval J_ρ, a weak spatial gradient of the pressure slice on the half ball B_{ρ/2}(x₀) together with its L^{6/5} bound. The general form of that selection carries three analytic hypotheses: the interior regularity of the harmonic part of the local pressure decomposition, the first-order identification of the first pressure potential, and the weak gradient of the two force potentials.

This file removes the first of the three outright, and reduces the other two to named inputs which are visibly about the data and not about the pressure: the divergence-form characterization of the slice source V and the distributional divergence-freedom of the force in space-time.

theorem CKN.Core.Step4.slice_selected_gradient_ae_of_sws_of_source_data (C_CZ C₁₇ C₁₁ : ℝ) (hC₁₇ : 1000 * Foundation.Heat.harmonicInteriorDisplayConstant ≤ C₁₇) {E F : ℝ → ℝ} {Ω : 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 V : 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) (hC₁₁ : 0 ≤ C₁₁) (hE : ∀ (s : ℝ), 0 ≤ E s) (hF : ∀ (s : ℝ), 0 ≤ F s) (hP1 : ∀ (i : Fin 3) (G : Foundation.Parabolic.Vec3 → ℝ), MeasureTheory.MemLp G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume → HasCompactSupport G → ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ∧ (∀ (j : Fin 3) (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i G x * spatialDeriv ψ j x = -∫ (x : Foundation.Parabolic.Vec3), D x j * ψ x) ∧ MeasureTheory.eLpNorm D (ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ ENNReal.ofReal C_CZ * MeasureTheory.eLpNorm G (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) (hCZ_p1 : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (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) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (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) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ C₁₁ * E s ^ (2 / 3)) (hP78 : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ F s) (hV : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (i : Fin 3), MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume) ∧ ∀ (i : Fin 3), HasCompactSupport fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (hVpair : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∑ i : Fin 3, ∫ (x : Foundation.Parabolic.Vec3), V (x, s) i * spatialDeriv ψ i 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) ψ) (hloc : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3), MeasureTheory.LocallyIntegrable (fun (x : Foundation.Parabolic.Vec3) => f (x, s) i) MeasureTheory.volume) (hdiv : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∫ (x : Foundation.Parabolic.Vec3), ∑ i : Fin 3, f (x, s) i * (fderiv ℝ ψ x) (basisVec i) = 0) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (D : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3), (∀ (k : Fin 3), MeasureTheory.LocallyIntegrableOn (fun (x : Foundation.Parabolic.Vec3) => D x k) (euclideanBall z.1 (ρ / 2)) MeasureTheory.volume) ∧ MeasureTheory.MemLp D (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ∧ (∀ (k : Fin 3), HasWeakPartialDerivOn (euclideanBall z.1 (ρ / 2)) k (fun (x : Vec 3) => p (x, s)) fun (x : Vec 3) => D x k) ∧ ∀ (k : Fin 3), MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => D x k) (ENNReal.ofReal (6 / 5)) (MeasureTheory.volume.restrict (euclideanBall z.1 (ρ / 2))) ≤ ENNReal.ofReal C_CZ * ∑ i : Fin 3, MeasureTheory.eLpNorm (fun (x : Foundation.Parabolic.Vec3) => V (x, s) i) (ENNReal.ofReal (6 / 5)) MeasureTheory.volume + ENNReal.ofReal (C₁₇ * (MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => p (x, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 ρ)) + C₁₁ * E s ^ (2 / 3) + F s) * ρ ^ (-1 / 2))

Display (3.5) on a slice of a suitable weak solution, with the interior regularity of the harmonic part discharged from the solution, the force slot discharged from the distributional divergence-freedom of the force, and the first-order identification discharged from the divergence-form characterization of the slice source.

Almost every slice of the pressure has a Vec3-valued weak spatial gradient on B_{ρ/2}(x₀), in L^{6/5} there, bounded by the Calderón–Zygmund norm of the divergence-form source and the ρ^{-1/2}-weighted L^{3/2} norm of the pressure.