Pk Bounds P7 Solution #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.eLpNorm'_prod_three_halves
{P : Foundation.Parabolic.Vec3 × ℝ → ℝ}
{B : Set Foundation.Parabolic.Vec3}
{T : Set ℝ}
(hP : MeasureTheory.AEStronglyMeasurable P (MeasureTheory.volume.restrict (B ×ˢ T)))
{D : ℝ → ENNReal}
(hD :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, MeasureTheory.eLpNorm' (fun (x : Foundation.Parabolic.Vec3) => P (x, s)) 15 MeasureTheory.volume ≤ D s)
:
MeasureTheory.eLpNorm' P (3 / 2) (MeasureTheory.volume.restrict (B ×ˢ T)) ≤ (∫⁻ (s : ℝ) in T, (D s * MeasureTheory.volume B ^ (3 / 5)) ^ (3 / 2)) ^ (2 / 3)
theorem
CKN.sws_p7_slice_data
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{η : Foundation.Parabolic.Vec3 → ℝ}
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
(hηc : HasCompactSupport η)
(hηΩ : tsupport η ⊆ Ω)
(hηbound : ∀ (y : Foundation.Parabolic.Vec3), |η y| ≤ 1)
(hηsupport : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ)
(hηmeas : MeasureTheory.AEStronglyMeasurable η MeasureTheory.volume)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀), MeasureTheory.AEStronglyMeasurable (fun (x : Foundation.Parabolic.Vec3) => f (x, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) ∧ ∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ‖f (x, s)‖ₑ ^ q < ⊤ ∧ ∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j)
MeasureTheory.volume ∧ MeasureTheory.AEStronglyMeasurable
(fun (x : Foundation.Parabolic.Vec3) =>
pressureNewtonianDerivativePotential j (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) x)
MeasureTheory.volume ∧ ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal |η y * f (y, s) j| ^ (5 / 2) < ⊤
theorem
CKN.force_time_norm_bound
{H : ℝ → ENNReal}
{T : Set ℝ}
{q A : ℝ}
(hq : 0 < q)
(hA : 0 ≤ A)
(hHae : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict T, H s < ⊤)
(hglobal : ∫⁻ (s : ℝ) in T, H s ≤ ENNReal.ofReal (A ^ q))
:
MeasureTheory.eLpNorm' (fun (s : ℝ) => (H s).toReal ^ (1 / q)) q (MeasureTheory.volume.restrict T) ≤ ENNReal.ofReal A
theorem
CKN.sws_force_time_data
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{q : ℝ}
{u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3}
{p : Foundation.Parabolic.ParabolicPoint → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
{x₀ : Foundation.Parabolic.Vec3}
{t₀ ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I)
:
AEMeasurable (fun (s : ℝ) => ∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ‖f (x, s)‖ₑ ^ q)
(MeasureTheory.volume.restrict (Set.Ioc (t₀ - ρ ^ 2) t₀)) ∧ ∫⁻ (s : ℝ) in Set.Ioc (t₀ - ρ ^ 2) t₀, ∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ‖f (x, s)‖ₑ ^ q ≤ ENNReal.ofReal ((ρ ^ (5 / q - 3) * lambda q f (x₀, t₀) ρ) ^ q)
theorem
CKN.pressureP7_eLpNorm15_le_slice_holder
{η : Foundation.Parabolic.Vec3 → ℝ}
{f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
{x₀ : Foundation.Parabolic.Vec3}
{q ρ s : ℝ}
(hq : 5 / 2 < q)
(hηbound : ∀ (y : Foundation.Parabolic.Vec3), |η y| ≤ 1)
(hηsupp : tsupport η ⊆ Foundation.Parabolic.vec3Ball x₀ ρ)
(hf :
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => f (y, s))
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)))
(hI : ∫⁻ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, ‖f (y, s)‖ₑ ^ q < ⊤)
(hsource :
∀ (j : Fin 3),
MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => η y * f (y, s) j) MeasureTheory.volume)
(hpotential :
∀ (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 ≤ 3 * (ENNReal.ofReal (4 * Real.pi)⁻¹ * Foundation.Euclidean.hlsRieszConstant) * MeasureTheory.eLpNorm' (fun (y : Foundation.Parabolic.Vec3) => f (y, s)) q
(MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ)) * MeasureTheory.volume (Foundation.Parabolic.vec3Ball x₀ ρ) ^ (2 / 5 - 1 / q)