Lin34 Centred Pairing SWS

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

The centred identification data at solution level

The slice identity of Lin34CentredPairing.lean is fed the slice data of a suitable weak solution: the integrability of the two nonlinearities on the support of the cut-off, the local integrability of the velocity, and the divergence-free slice condition tested against every compactly supported smooth function at once. The result is the pair of hypotheses that the Calderón--Zygmund estimate for the centred potential of prop:lin34 consumes.

theorem CKN.lin34_centredP1_cz_data_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), (∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x = pressureSecondPairing (lin34CentredSource u z.1 hρ s) ψ) ∧ ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume

The identification data for the centred first potential at solution level. For a suitable weak solution and almost every time of the cylinder Q_ρ(z₀), the whole-space distributional identity of prop:pressure-decomposition holds for the centred potential against the centred source eq:Uhat, simultaneously for every compactly supported smooth spatial test function, together with the integrability of that pairing.