Pk Bounds P7 #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
The HLS input for one derivative potential. The pointwise domination hypothesis is the kernel comparison used when the pressure potential is defined from an integrable compactly supported slice.
theorem
CKN.pressureNewtonianDerivativePotential_eLpNorm15_le_hls
{g : Foundation.Parabolic.Vec3 → ℝ}
(i : Fin 3)
(hg : Measurable g)
(hfinite : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2) < ⊤)
(hzero : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2) ≠ 0)
(hgood :
∀ᵐ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.maximalMajorant g x ≠ 0 ∧ Foundation.Euclidean.maximalMajorant g x ≠ ⊤)
{K : ℝ}
(hdom :
∀ᵐ (x : Foundation.Parabolic.Vec3), ‖pressureNewtonianDerivativePotential i g x‖ₑ ≤ ENNReal.ofReal K * Foundation.Euclidean.rieszPotentialOne g x)
:
MeasureTheory.eLpNorm' (fun (x : Foundation.Parabolic.Vec3) => pressureNewtonianDerivativePotential i g x) 15
MeasureTheory.volume ≤ ENNReal.ofReal K * Foundation.Euclidean.hlsRieszConstant * (∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2)) ^ (2 / 5)
theorem
CKN.pressureNewtonianDerivativePotential_eLpNorm15_le_hls_unconditional
{g : Foundation.Parabolic.Vec3 → ℝ}
(i : Fin 3)
(hg : Measurable g)
(hfinite : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2) < ⊤)
(hzero : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2) ≠ 0)
(hgood :
∀ᵐ (x : Foundation.Parabolic.Vec3), Foundation.Euclidean.maximalMajorant g x ≠ 0 ∧ Foundation.Euclidean.maximalMajorant g x ≠ ⊤)
:
MeasureTheory.eLpNorm' (fun (x : Foundation.Parabolic.Vec3) => pressureNewtonianDerivativePotential i g x) 15
MeasureTheory.volume ≤ ENNReal.ofReal (4 * Real.pi)⁻¹ * Foundation.Euclidean.hlsRieszConstant * (∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2)) ^ (2 / 5)
theorem
CKN.pressureNewtonianDerivativePotential_eLpNorm15_le_hls_of_zero_or_good
{g : Foundation.Parabolic.Vec3 → ℝ}
(i : Fin 3)
(hg : Measurable g)
(hfinite : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2) < ⊤)
:
MeasureTheory.eLpNorm' (fun (x : Foundation.Parabolic.Vec3) => pressureNewtonianDerivativePotential i g x) 15
MeasureTheory.volume ≤ ENNReal.ofReal (4 * Real.pi)⁻¹ * Foundation.Euclidean.hlsRieszConstant * (∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |g y| ^ (5 / 2)) ^ (2 / 5)
theorem
CKN.pressureP7_eLpNorm15_le_components
{η : Foundation.Parabolic.Vec3 → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{s : ℝ}
{A : Fin 3 → ENNReal}
(hmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x)
MeasureTheory.volume)
(hA :
∀ (j : Fin 3),
MeasureTheory.eLpNorm'
(fun (x : Foundation.Parabolic.Vec3) =>
pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x)
15 MeasureTheory.volume ≤ A j)
:
theorem
CKN.pressureP7_eLpNorm15_le_hls_of_aestronglyMeasurable
{η : Foundation.Parabolic.Vec3 → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{s : ℝ}
(hgmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume)
(hmeas :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x)
MeasureTheory.volume)
(hfinite : ∀ (j : Fin 3), ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |η y * f (y, s) j| ^ (5 / 2) < ⊤)
:
MeasureTheory.eLpNorm' (pressureP7 η f s) 15 MeasureTheory.volume ≤ ∑ j : Fin 3,
ENNReal.ofReal (4 * Real.pi)⁻¹ * Foundation.Euclidean.hlsRieszConstant * (∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |η y * f (y, s) j| ^ (5 / 2)) ^ (2 / 5)
Cylinder assembly in the same scale-interface form as the other pressure
terms. The preceding theorem supplies the fixed-time HLS estimate used to
instantiate hP₇; the cylinder step is purely the time/space Hölder algebra.