Delta PCentred

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

The centred tensor and its distributional pressure identity.

def CKN.pressureUHat (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (z : Foundation.Parabolic.ParabolicPoint) (i j : Fin 3) : ℝ

Fully centered velocity tensor used in the pressure-pairing identities.

Equations

• CKN.pressureUHat u c z i j = -(u z i - c z.2 i) * (u z j - c z.2 j)

theorem CKN.pressure_delta_p_centred_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) {c : ℝ → Foundation.Parabolic.Vec3} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψΩ : tsupport ψ ⊆ Ω) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict I, ∫ (x : Foundation.Parabolic.Vec3) in Ω, p (x, s) * spatialLaplacian ψ x = (∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, ∑ j : Fin 3, pressureUHat u c (x, s) i j * mixedSecond ψ i j x) - ∫ (x : Foundation.Parabolic.Vec3) in Ω, ∑ i : Fin 3, f (x, s) i * spatialDeriv ψ i x