Potentials

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

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

noncomputable def CKN.pressureNewtonianPotential (g : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : ℝ

The Newtonian potential with the paper's sign convention N = -newtonianKernel.

Equations

• CKN.pressureNewtonianPotential g x = ∫ (y : CKN.Foundation.Parabolic.Vec3), -CKN.Foundation.Heat.newtonianKernel (x - y) * g y

noncomputable def CKN.pressureNewtonianDerivativePotential (i : Fin 3) (g : Foundation.Parabolic.Vec3 → ℝ) (x : Foundation.Parabolic.Vec3) : ℝ

The first derivative potential, written as -∂ⱼN * g = ∂ⱼ(newtonianKernel) * g.

Equations

• CKN.pressureNewtonianDerivativePotential i g x = ∫ (y : CKN.Foundation.Parabolic.Vec3), CKN.spatialDeriv CKN.Foundation.Heat.newtonianKernel i (x - y) * g y

theorem CKN.pressureNewtonianPotential_locallyIntegrable {g : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) : MeasureTheory.LocallyIntegrable (pressureNewtonianPotential g) MeasureTheory.volume

theorem CKN.pressureNewtonianDerivativePotential_locallyIntegrable {g : Foundation.Parabolic.Vec3 → ℝ} (i : Fin 3) (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) : MeasureTheory.LocallyIntegrable (pressureNewtonianDerivativePotential i g) MeasureTheory.volume

theorem CKN.pressureNewtonianPotential_mul_smooth_integrable {g φ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureNewtonianPotential g x * φ x) MeasureTheory.volume

theorem CKN.pressureNewtonianDerivativePotential_mul_smooth_integrable {i : Fin 3} {g φ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => pressureNewtonianDerivativePotential i g x * φ x) MeasureTheory.volume

theorem CKN.pressureNewtonianPotential_pairing {g φ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianPotential g x * φ x = ∫ (y : Foundation.Parabolic.Vec3), g y * ∫ (x : Foundation.Parabolic.Vec3), -Foundation.Heat.newtonianKernel (x - y) * φ x

theorem CKN.pressureNewtonianPotential_adjoint {ψ : Foundation.Parabolic.Vec3 → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (y : Foundation.Parabolic.Vec3) : ∫ (x : Foundation.Parabolic.Vec3), -Foundation.Heat.newtonianKernel (x - y) * spatialLaplacian ψ x = ψ y

theorem CKN.pressureNewtonianPotential_distributional_pairing {g ψ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) : ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianPotential g x * spatialLaplacian ψ x = ∫ (y : Foundation.Parabolic.Vec3), g y * ψ y

theorem CKN.pressureNewtonianDerivativePotential_pairing {i : Fin 3} {g φ H : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (hinner : ∀ (y : Foundation.Parabolic.Vec3), ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * φ x = H y) : ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i g x * φ x = ∫ (y : Foundation.Parabolic.Vec3), g y * H y

theorem CKN.pressureNewtonianDerivativePotential_distributional_pairing {i : Fin 3} {g ψ : Foundation.Parabolic.Vec3 → ℝ} (hg : MeasureTheory.Integrable g MeasureTheory.volume) (hgc : HasCompactSupport g) (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hinner : ∀ (y : Foundation.Parabolic.Vec3), ∫ (x : Foundation.Parabolic.Vec3), spatialDeriv Foundation.Heat.newtonianKernel i (x - y) * spatialLaplacian ψ x = spatialDeriv ψ i y) : ∫ (x : Foundation.Parabolic.Vec3), pressureNewtonianDerivativePotential i g x * spatialLaplacian ψ x = ∫ (y : Foundation.Parabolic.Vec3), g y * spatialDeriv ψ i y