Morrey membership of the fixed near-force source #
Local force integrability on a finite fixed carrier gives the target source Morrey class. The cutoff is bounded by one, and no spatial supremum bound on the force is used.
Morrey membership of the fixed force-free pressure source #
The localization cylinder is inside the prescribed velocity and gradient carrier. Suitability controls its fixed spatial mean through the local energy bound, and the force-free tensor estimate then gives the target source class.
theorem
CKN.Core.Step4.fixed_pressure_cylinder_subset_ball
(z₀ : Foundation.Parabolic.ParabolicPoint)
{R : ℝ}
(hR : 0 < R)
:
Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) R ⊆ Metric.ball z₀ R
The fixed pressure localization lies in the original radius ball.
theorem
CKN.Core.Step4.fixed_centred_source_morrey_lt_top_of_sws
{τ q : ℝ}
(hq : 5 / 2 < q)
(hτ : 25 / 3 ≤ τ)
(hτhi : τ ≤ 25)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{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)
(z₀ : Foundation.Parabolic.ParabolicPoint)
{R : ℝ}
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
(hu : morreyVecMem 3 τ (Metric.ball z₀ R) u)
(hDu :
∀ (i : Fin 3), morreyVecMem 2 (25 / 8) (Metric.ball z₀ R) fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i)
(i : Fin 3)
:
have η := mollifiedBallCutoff z₀.1 hR;
have V := sourceMorreyCutoffVCentredTensorSpacetime η (spatialDeriv η) u Du (sourceSliceCentredMean z₀.1 R u);
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) (min (1 / τ + 8 / 25)⁻¹ q)
((Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) R).indicator
fun (w : Foundation.Parabolic.ParabolicPoint) => V w i) < ⊤
The fixed force-free centred source has finite target Morrey seminorm under the velocity and gradient hypotheses of the pressure transfer.
theorem
CKN.Core.Step4.fixed_near_force_source_morrey_lt_top_of_sws
{κ q : ℝ}
(hκ : 6 / 5 ≤ κ)
(hκq : κ ≤ q)
{Ω : Set Foundation.Parabolic.Vec3}
{I : Set ℝ}
{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)
(z₀ : Foundation.Parabolic.ParabolicPoint)
{R : ℝ}
(hR : 0 < R)
(hdom : Metric.ball z₀ (2 * R) ⊆ spaceTimeSet Ω I)
(j : Fin 3)
:
Foundation.Parabolic.Morrey.morreyNorm (6 / 5) κ
((Foundation.Parabolic.parabolicCylinder z₀.1 (z₀.2 + R ^ 2 / 4) R).indicator
fun (w : Foundation.Parabolic.ParabolicPoint) => mollifiedBallCutoff z₀.1 hR w.1 * f w j) < ⊤
The fixed near-force source has finite target Morrey seminorm directly from the suitable solution's local force integrability.