Fixed derivative decomposition on backward local cylinders #
The fixed-source construction is applied on an arbitrary backward cylinder, including cylinders ending at the final carrier time. The source argument specializes the same-repository fixed-source Morrey estimates to this geometry. The selected derivative is retained in the signed Riesz and remainder identity.
theorem
CKN.Core.Step4.originClause_local_derivative_morrey_of_remainder
{τ 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}
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hrem :
∃ (M : ℝ → ENNReal),
AEMeasurable M MeasureTheory.volume ∧ ∫⁻ (s : ℝ), M s ^ (3 / 2) < ⊤ ∧ ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
∀ x ∈ Foundation.Parabolic.vec3Ball z.1 (ρ / 2),
‖classicalGradient
(harmonicPressurePart (mollifiedBallCutoff z.1 hρ) u (sourceSliceCentredMean z.1 ρ u) p s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
x i‖ₑ ≤ M s)
(hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(hbox : localBox Ω I (Foundation.Parabolic.vec3Ball z.1 ρ) (Set.Ioc (z.2 - ρ ^ 2) z.2))
(hU :
∀ (j : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 3 τ
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
u w j) < ⊤)
(hD :
∀ (j k : Fin 3),
Foundation.Parabolic.Morrey.morreyNorm 2 (25 / 8)
((Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ).indicator fun (w : Foundation.Parabolic.ParabolicPoint) =>
Du w j k) < ⊤)
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hDp : Measurable Dp)
(hweak :
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
MeasureTheory.LocallyIntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Dp (y, s) i)
(Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) MeasureTheory.volume ∧ HasWeakPartialDerivOn (Foundation.Parabolic.vec3Ball z.1 (ρ / 2)) i (fun (y : Vec 3) => p (y, s))
fun (y : Vec 3) => Dp (y, s) i)
(i : Fin 3)
:
On one backward cylinder, the fixed harmonic/far temporal envelope gives Morrey control of the same selected weak derivative on its spatial half-ball. The source and force classes are derived from suitability and the stated velocity and gradient Morrey data on the localization cylinder.