Force Cancellation

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

def CKN.SmoothCompactTest (ψ : Foundation.Parabolic.Vec3 → ℝ) : Prop

The test functions used for a distributional spatial divergence.

Equations

• CKN.SmoothCompactTest ψ = ((∀ (n : ℕ), ContDiff ℝ (↑↑n) ψ) ∧ HasCompactSupport ψ)

def CKN.DistributionalDivergenceFree (F : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3) : Prop

Distributional divergence-free data, with the spatial test class explicit.

Equations

• CKN.DistributionalDivergenceFree F = ∀ (ψ : CKN.Foundation.Parabolic.Vec3 → ℝ), CKN.SmoothCompactTest ψ → ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, F x i * CKN.spatialDeriv ψ i x = 0

theorem CKN.pressure_force_pairing_zero_of_distributionalDivergenceFree {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hη : SmoothCompactTest η) (hdiv : DistributionalDivergenceFree fun (x : Foundation.Parabolic.Vec3) => f (x, s)) (hInt7 : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume) (hSupp7 : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) (hInt8 : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) MeasureTheory.volume) (hSupp8 : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) (ψ : Foundation.Parabolic.Vec3 → ℝ) : SmoothCompactTest ψ → ∫ (x : Foundation.Parabolic.Vec3), (pressureP7 η f s x + pressureP8 η f s x) * spatialLaplacian ψ x = 0

The force potentials have zero Laplacian pairing under distributional divergence cancellation.

theorem CKN.pressure_force_eq_zero_of_distributionalDivergenceFree {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hη : SmoothCompactTest η) (hdiv : DistributionalDivergenceFree fun (x : Foundation.Parabolic.Vec3) => f (x, s)) (hInt7 : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume) (hSupp7 : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) (hInt8 : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) MeasureTheory.volume) (hSupp8 : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) (hmem : ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (pressureP7 η f s + pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hgrowth : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (pressureP7 η f s + pressureP8 η f s) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C * (1 + ρ)) : pressureP7 η f s + pressureP8 η f s =ᵐ[MeasureTheory.volume] 0

A global harmonic force potential vanishes once its local integrability and linear growth are supplied.