Decomposition Potentials

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

The eight explicit potentials in the local pressure decomposition.

noncomputable def CKN.pressureP2 (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

Newtonian potential of the tensor paired with the second derivatives of the cutoff.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.pressureP3 (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

First Newtonian derivative potential for the first tensor-cutoff cross term.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.pressureP4 (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

First Newtonian derivative potential for the second tensor-cutoff cross term.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def CKN.pressureP5 (η : Foundation.Parabolic.Vec3 → ℝ) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

Pressure correction involving the Laplacian of the cutoff.

Equations

• CKN.pressureP5 η p s x = -CKN.pressureNewtonianPotential (fun (y : CKN.Foundation.Parabolic.Vec3) => p (y, s) * CKN.spatialLaplacian η y) x

noncomputable def CKN.pressureP6 (η : Foundation.Parabolic.Vec3 → ℝ) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

Pressure correction involving the gradient of the cutoff.

Equations

• CKN.pressureP6 η p s x = -2 * ∑ j : Fin 3, CKN.pressureNewtonianDerivativePotential j (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv η j y * p (y, s)) x

noncomputable def CKN.pressureP7 (η : Foundation.Parabolic.Vec3 → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

First Newtonian derivative potential of the cutoff force.

Equations

• CKN.pressureP7 η f s x = -∑ j : Fin 3, CKN.pressureNewtonianDerivativePotential j (fun (y : CKN.Foundation.Parabolic.Vec3) => η y * f (y, s) j) x

noncomputable def CKN.pressureP8 (η : Foundation.Parabolic.Vec3 → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

Newtonian potential of the force paired with the cutoff gradient.

Equations

• CKN.pressureP8 η f s x = -∑ j : Fin 3, CKN.pressureNewtonianPotential (fun (y : CKN.Foundation.Parabolic.Vec3) => CKN.spatialDeriv η j y * f (y, s) j) x

noncomputable def CKN.pressureP1 (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) : Foundation.Parabolic.Vec3 → ℝ

Localized pressure after subtracting the seven explicit cutoff and forcing corrections.

Equations

• One or more equations did not get rendered due to their size.

theorem CKN.pressure_decomposition_pointwise (η : Foundation.Parabolic.Vec3 → ℝ) (u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (c : ℝ → Foundation.Parabolic.Vec3) (p : Foundation.Parabolic.ParabolicPoint → ℝ) (f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3) (s : ℝ) (x : Foundation.Parabolic.Vec3) : η x * p (x, s) = pressureP1 η u c p f s x + pressureP2 η u c s x + pressureP3 η u c s x + pressureP4 η u c s x + pressureP5 η p s x + pressureP6 η p s x + pressureP7 η f s x + pressureP8 η f s x

theorem CKN.pressureP2_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) : MeasureTheory.LocallyIntegrable (pressureP2 η u c s) MeasureTheory.volume

theorem CKN.pressureP3_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) : MeasureTheory.LocallyIntegrable (pressureP3 η u c s) MeasureTheory.volume

theorem CKN.pressureP4_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) : MeasureTheory.LocallyIntegrable (pressureP4 η u c s) MeasureTheory.volume

theorem CKN.pressureP5_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hInt : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) MeasureTheory.volume) (hSupp : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) : MeasureTheory.LocallyIntegrable (pressureP5 η p s) MeasureTheory.volume

theorem CKN.pressureP6_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) : MeasureTheory.LocallyIntegrable (pressureP6 η p s) MeasureTheory.volume

theorem CKN.pressureP7_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) : MeasureTheory.LocallyIntegrable (pressureP7 η f s) MeasureTheory.volume

theorem CKN.pressureP8_locallyIntegrable {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) : MeasureTheory.LocallyIntegrable (pressureP8 η f s) MeasureTheory.volume

theorem CKN.pressureP2_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => mixedSecond η i j y * pressureUTensor u c (y, s) i j) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP2 η u c s x * spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), mixedSecond η i j y * pressureUTensor u c (y, s) i j * ψ y

theorem CKN.pressureP5_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) MeasureTheory.volume) (hSupp : HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => p (y, s) * spatialLaplacian η y) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP5 η p s x * spatialLaplacian ψ x = -∫ (y : Foundation.Parabolic.Vec3), p (y, s) * spatialLaplacian η y * ψ y

theorem CKN.pressureP8_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * f (y, s) j) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP8 η f s x * spatialLaplacian ψ x = -∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * f (y, s) j * ψ y

theorem CKN.pressureP6_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => spatialDeriv η j y * p (y, s)) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP6 η p s x * spatialLaplacian ψ x = -2 * ∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), spatialDeriv η j y * p (y, s) * spatialDeriv ψ j y

theorem CKN.pressureP7_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume) (hSupp : ∀ (j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP7 η f s x * spatialLaplacian ψ x = -∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), η y * f (y, s) j * spatialDeriv ψ j y

theorem CKN.pressureP3_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η i y) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP3 η u c s x * spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), pressureUTensor u c (y, s) i j * spatialDeriv η i y * spatialDeriv ψ j y

theorem CKN.pressureP4_distributional_pairing {η : Foundation.Parabolic.Vec3 → ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {c : ℝ → Foundation.Parabolic.Vec3} {s : ℝ} {ψ : Foundation.Parabolic.Vec3 → ℝ} (hInt : ∀ (i j : Fin 3), MeasureTheory.Integrable (fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) MeasureTheory.volume) (hSupp : ∀ (i j : Fin 3), HasCompactSupport fun (y : Foundation.Parabolic.Vec3) => pressureUTensor u c (y, s) i j * spatialDeriv η j y) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureP4 η u c s x * spatialLaplacian ψ x = ∑ i : Fin 3, ∑ j : Fin 3, ∫ (y : Foundation.Parabolic.Vec3), pressureUTensor u c (y, s) i j * spatialDeriv η j y * spatialDeriv ψ i y