Source Morrey Gradient Package #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
Gradient-slot localized source package #
The local Morrey source bounds for the pressure-gradient heat representation.
theorem
CKN.Core.Step4.localized_gradient_force_morrey_of_sws
{Ω : 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 × ℝ → ℝ}
(hφ : φ ∈ spaceTimeTestFunction Ω I)
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I Ω' J)
(hφbox : tsupport φ ⊆ Ω' ×ˢ J)
(i : Fin 3)
:
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9)) fun (z : Foundation.Parabolic.ParabolicPoint) =>
φ z * f z i) < ⊤
theorem
CKN.Core.Step4.localized_gradient_source_package_of_sws
{Ω : 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 × ℝ → ℝ}
(hφ : φ ∈ spaceTimeTestFunction Ω I)
{Ω' : Set Foundation.Parabolic.Vec3}
{J : Set ℝ}
(hbox : localBox Ω I Ω' J)
(hφbox : tsupport φ ⊆ Ω' ×ˢ J)
(z₀ : Foundation.Parabolic.ParabolicPoint)
(R : ℝ)
(hR : 0 < R)
(hq : 5 / 2 < q)
(hφcarrier : tsupport φ ⊆ ⇑Foundation.Parabolic.parabolicHomeomorph.symm ⁻¹' Metric.ball z₀ R)
(hU : morreyVecMem 3 25 (Metric.ball z₀ R) u)
(hDuNorm :
∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i)
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hDpAE :
∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (Metric.ball z₀ R)))
(hDpN : morreyVecMem (6 / 5) (min q (25 / 9)) (Metric.ball z₀ R) Dp)
:
(∀ (i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i)
MeasureTheory.volume) ∧ (∀ (j i : Fin 3),
AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceH φ u j z i)
MeasureTheory.volume) ∧ (∀ (i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) ∧ (∀ (j i : Fin 3),
HasCompactSupport fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceH φ u j z i) ∧ (∀ (i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min q (25 / 9))
fun (z : Foundation.Parabolic.ParabolicPoint) => localizedGradientSourceG φ u Du f Dp z i) < ⊤) ∧ ∀ (j i : Fin 3),
(Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (25 / 3) fun (z : Foundation.Parabolic.ParabolicPoint) =>
localizedGradientSourceH φ u j z i) < ⊤