Riesz Second Exterior #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Pressure-sign convention for the second Newtonian derivative outside the source support.
Equations
Instances For
theorem
CKN.Foundation.Euclidean.rieszSecondL2_exterior_potential_aestronglyMeasurable
{i j : Fin 3}
{b : Parabolic.Vec3 → ℝ}
{A U : Set Parabolic.Vec3}
(hb : MeasureTheory.Integrable b MeasureTheory.volume)
(hU : IsOpen U)
(hbA : ∀ y ∉ A, b y = 0)
{δ : ℝ}
(hδ : 0 < δ)
(hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y))
:
MeasureTheory.AEStronglyMeasurable
(fun (x : Parabolic.Vec3) =>
∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * b y)
(MeasureTheory.volume.restrict U)
theorem
CKN.Foundation.Euclidean.rieszSecondL2_exterior_potential_bound
{i j : Fin 3}
{b : Parabolic.Vec3 → ℝ}
{A U : Set Parabolic.Vec3}
(hb : MeasureTheory.Integrable b MeasureTheory.volume)
:
IsOpen U →
∀ (hbA : ∀ y ∉ A, b y = 0) {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y))
{x : Parabolic.Vec3} (hx : x ∈ U),
‖∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * b y‖ ≤ 4 * (4 * Real.pi)⁻¹ * ((δ / 3) ^ 3)⁻¹ * ∫ (y : Parabolic.Vec3), ‖b y‖
theorem
CKN.Foundation.Euclidean.rieszSecondL2_exterior_potential_integrableOn_compact
{i j : Fin 3}
{b : Parabolic.Vec3 → ℝ}
(hb : MeasureTheory.Integrable b MeasureTheory.volume)
{A U C : Set Parabolic.Vec3}
(hU : IsOpen U)
(hbA : ∀ y ∉ A, b y = 0)
:
Bornology.IsBounded A →
∀ {δ : ℝ} (hδ : 0 < δ) (hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y)) (hC : IsCompact C)
(hCU : C ⊆ U),
MeasureTheory.IntegrableOn
(fun (x : Parabolic.Vec3) =>
∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * b y)
C MeasureTheory.volume
theorem
CKN.Foundation.Euclidean.rieszSecondL2_exterior_representation
{i j : Fin 3}
(hL2 : RieszSecondL2Input i j)
{b : Parabolic.Vec3 → ℝ}
(hb₂ : MeasureTheory.MemLp b 2 MeasureTheory.volume)
{A U : Set Parabolic.Vec3}
(hU : IsOpen U)
(hbA : ∀ y ∉ A, b y = 0)
(hAb : Bornology.IsBounded A)
{δ : ℝ}
(hδ : 0 < δ)
(hsep : ∀ x ∈ U, ∀ y ∈ A, δ ≤ Parabolic.vec3EuclideanNorm (x - y))
:
rieszSecondL2MeasurableOperator hL2 (MeasureTheory.MemLp.toLp b hb₂) =ᵐ[MeasureTheory.volume.restrict U]
fun (x : Parabolic.Vec3) =>
∫ (y : Parabolic.Vec3), (-spatialDeriv (spatialDeriv Heat.newtonianKernel i) j) (x - y) * b y