Identification Extension Pairing Source

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

Support and integrability of the eight cut-off pressure sources

The paper's pressure representation prop:pressure-decomposition writes the localized pressure η p as a remainder p₁ plus the eight source potentials p₂, …, p₈ (eq:p1-bound, eq:p234-bound, eq:p56-bound, eq:p78-bound). Each of those potentials is a Newtonian or Newtonian-derivative potential of an integrand built from the cut-off η, the velocity u, the pressure p and the force f, evaluated on the time slice t = s.

This file records the bookkeeping needed to feed those potentials into the potential calculus: that the spatial derivatives and the spatial Laplacian of a cut-off are again supported in the cut-off's support (and hence compactly supported), a general criterion turning an integrability hypothesis on a set K into global integrability of a product with a smooth function supported in K, and the resulting integrability and compact-support statements for the eight source integrands.

The eight source integrands are, in the order used below,

• η · p (remainder/p₁ slot, eq:p1-bound),
• ∂ᵢ∂ⱼη · Uᵢⱼ, Uᵢⱼ · ∂ᵢη, Uᵢⱼ · ∂ⱼη (p₂, p₃, p₄, eq:p234-bound),
• p · Δη, ∂ⱼη · p (p₅, p₆, eq:p56-bound),
• η · fⱼ, ∂ⱼη · fⱼ (p₇, p₈, eq:p78-bound),

where Uᵢⱼ = pressureUTensor u c (·, s) i j.

Support of the spatial derivatives of a cut-off

theorem CKN.pressureCutoff_tsupport_spatialDeriv_subset (η : Foundation.Parabolic.Vec3 → ℝ) (i : Fin 3) : tsupport (spatialDeriv η i) ⊆ tsupport η

The first spatial derivative ∂ᵢη of a cut-off is supported in the support of η (prop:pressure-decomposition).

theorem CKN.pressureCutoff_tsupport_mixedSecond_subset (η : Foundation.Parabolic.Vec3 → ℝ) (i j : Fin 3) : tsupport (mixedSecond η i j) ⊆ tsupport η

The mixed second derivative ∂ᵢ∂ⱼη of a cut-off is supported in the support of η (prop:pressure-decomposition).

theorem CKN.pressureCutoff_tsupport_spatialLaplacian_subset (η : Foundation.Parabolic.Vec3 → ℝ) : tsupport (spatialLaplacian η) ⊆ tsupport η

The spatial Laplacian Δη of a cut-off is supported in the support of η (prop:pressure-decomposition).

theorem CKN.pressureCutoff_hasCompactSupport_spatialDeriv {η : Foundation.Parabolic.Vec3 → ℝ} (hηc : HasCompactSupport η) (i : Fin 3) : HasCompactSupport (spatialDeriv η i)

The first spatial derivative of a compactly supported cut-off is compactly supported (prop:pressure-decomposition).

theorem CKN.pressureCutoff_hasCompactSupport_mixedSecond {η : Foundation.Parabolic.Vec3 → ℝ} (hηc : HasCompactSupport η) (i j : Fin 3) : HasCompactSupport (mixedSecond η i j)

The mixed second derivative of a compactly supported cut-off is compactly supported (prop:pressure-decomposition).

theorem CKN.pressureCutoff_hasCompactSupport_spatialLaplacian {η : Foundation.Parabolic.Vec3 → ℝ} (hηc : HasCompactSupport η) : HasCompactSupport (spatialLaplacian η)

The spatial Laplacian of a compactly supported cut-off is compactly supported (prop:pressure-decomposition).

Integrability against a locally bounded source

theorem CKN.pressureCutoff_integrable_mul_of_tsupport_subset {θ g : Foundation.Parabolic.Vec3 → ℝ} {K : Set Foundation.Parabolic.Vec3} (hθ : Continuous θ) (hθc : HasCompactSupport θ) (hθK : tsupport θ ⊆ K) (hg : MeasureTheory.IntegrableOn g K MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => θ y * g y) MeasureTheory.volume

If θ is a continuous compactly supported function whose support lies in a set K, and g is integrable on K, then θ · g is integrable on all of ℝ³ (prop:pressure-decomposition). This is the criterion used to turn the slice-integrability hypotheses on the eight sources into global integrability of the potentials' integrands.

The eight cut-off pressure sources: integrability

theorem CKN.pressureCutoff_cutoffPressure_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hp : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * p (y, s)) MeasureTheory.volume

The localized pressure integrand η · p(·, s) is integrable (eq:p1-bound).

theorem CKN.pressureCutoff_hessianTensor_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hU : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j) (tsupport η) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) MeasureTheory.volume

The p₂ integrand ∂ᵢ∂ⱼη · Uᵢⱼ is integrable (eq:p234-bound).

theorem CKN.pressureCutoff_tensorGradientFirst_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hU : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j) (tsupport η) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume

The p₃ integrand Uᵢⱼ · ∂ᵢη is integrable (eq:p234-bound).

theorem CKN.pressureCutoff_tensorGradientSecond_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hU : ∀ (i j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j) (tsupport η) MeasureTheory.volume) (i j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume

The p₄ integrand Uᵢⱼ · ∂ⱼη is integrable (eq:p234-bound).

theorem CKN.pressureCutoff_pressureLaplacian_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hp : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) MeasureTheory.volume

The p₅ integrand p(·, s) · Δη is integrable (eq:p56-bound).

theorem CKN.pressureCutoff_pressureGradient_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hp : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (tsupport η) MeasureTheory.volume) (j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) MeasureTheory.volume

The p₆ integrand ∂ⱼη · p(·, s) is integrable (eq:p56-bound).

theorem CKN.pressureCutoff_forceCutoff_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hf : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (tsupport η) MeasureTheory.volume) (j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume

The p₇ integrand η · fⱼ(·, s) is integrable (eq:p78-bound).

theorem CKN.pressureCutoff_forceGradient_integrable {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hη : ContDiff ℝ (↑⊤) η) (hηc : HasCompactSupport η) (hf : ∀ (j : Fin 3), MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => f (y, s) j) (tsupport η) MeasureTheory.volume) (j : Fin 3) : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) MeasureTheory.volume

The p₈ integrand ∂ⱼη · fⱼ(·, s) is integrable (eq:p78-bound).

The eight cut-off pressure sources: compact support

theorem CKN.pressureCutoff_hessianTensor_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hηc : HasCompactSupport η) (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j

The p₂ integrand ∂ᵢ∂ⱼη · Uᵢⱼ has compact support (eq:p234-bound).

theorem CKN.pressureCutoff_tensorGradientFirst_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hηc : HasCompactSupport η) (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y

The p₃ integrand Uᵢⱼ · ∂ᵢη has compact support (eq:p234-bound).

theorem CKN.pressureCutoff_tensorGradientSecond_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hηc : HasCompactSupport η) (i j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y

The p₄ integrand Uᵢⱼ · ∂ⱼη has compact support (eq:p234-bound).

theorem CKN.pressureCutoff_pressureLaplacian_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hηc : HasCompactSupport η) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y

The p₅ integrand p(·, s) · Δη has compact support (eq:p56-bound).

theorem CKN.pressureCutoff_pressureGradient_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hηc : HasCompactSupport η) (j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)

The p₆ integrand ∂ⱼη · p(·, s) has compact support (eq:p56-bound).

theorem CKN.pressureCutoff_forceCutoff_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hηc : HasCompactSupport η) (j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j

The p₇ integrand η · fⱼ(·, s) has compact support (eq:p78-bound).

theorem CKN.pressureCutoff_forceGradient_hasCompactSupport {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hηc : HasCompactSupport η) (j : Fin 3) : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j

The p₈ integrand ∂ⱼη · fⱼ(·, s) has compact support (eq:p78-bound).