Lin34 Slice Force Lp

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

The force potential p₇ + p₈ is L^{3/2} on a.e. time slice

The decomposition prop:pressure-decomposition, grouped in cor:CZ-harmonic, splits the local pressure into a Calderón–Zygmund part, a harmonic remainder, and the force potentials p₇ and p₈ built from the cutoff η and the force f of a suitable weak solution def:sws. This file records the time-slice form of the force estimate needed by the quantitative Hölder consumer prop:lin34: for almost every time in the lower half of a parabolic cylinder, the sum p₇ + p₈ is L^{3/2} on every round ball of the spatial slice.

The proof combines three ingredients from CKN/Pressure/PkBoundsP7Solution.lean and CKN/Pressure/HarmonicRemainderForceTerms.lean: the a.e.-in-time slice data for the force, the L^q membership of the two families of sources η fⱼ and (∂ⱼ η) fⱼ, and the local L^{3/2} theory of the Newtonian potentials CKN.Foundation.Euclidean.pressureP7_add_pressureP8_memLp_and_lpNorm_growth.

Step 1: a.e. slice data for the force

Step 2: the two families of L^q sources

Step 3: local support and ball-inclusion helpers

The time-slice L^{3/2} statement for the force potentials

theorem CKN.lin34_force_slice_memLp_ae {Ω : 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), ∀ (x : Foundation.Parabolic.Vec3) (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 x R))

prop:lin34 (force side), in the form consumed by the quantitative Hölder estimate: for almost every time s in the lower half of a parabolic cylinder whose closure lies in the carrier, the force potentials p₇ + p₈ of lem:pk-bounds built from the ball cutoff at z and radius ρ are L^{3/2} on every round ball of the spatial slice.