Global centred-source estimates #
The local norm data of def:sws give compactly supported L^{6/5} sources
and the explicit centred majorant used in eq:pressure-gradient-decomposition.
noncomputable def
CKN.Core.Step4.centredSWSCentredMajorant
(x : Foundation.Parabolic.Vec3)
(ρ q : ℝ)
(u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(s : ℝ)
:
The global componentwise source majorant in eq:pressure-gradient-decomposition,
including the constant-mean correction and the localized force norm.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.Core.Step4.centredSWS_source_data_ae
{Ω : 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)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
(c : ℝ → Foundation.Parabolic.Vec3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), (∀ (i : Fin 3),
MeasureTheory.MemLp
(fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) u Du c (x, s) i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume) ∧ ∀ (i : Fin 3),
HasCompactSupport fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) u Du c (x, s) i
Suitable-solution data supply global source membership and compact support
for any time-dependent spatial centring vector in eq:pressure-gradient-decomposition.
theorem
CKN.Core.Step4.centredSWS_source_bound_ae
{Ω : 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)
{z : Foundation.Parabolic.ParabolicPoint}
{ρ : ℝ}
(hρ : 0 < ρ)
(hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (i : Fin 3),
MeasureTheory.eLpNorm
(fun (x : Foundation.Parabolic.Vec3) =>
sourceMorreyCutoffVCentredTensorSpacetime (mollifiedBallCutoff z.1 hρ)
(spatialDeriv (mollifiedBallCutoff z.1 hρ)) u Du (sourceSliceCentredMean z.1 ρ u) (x, s) i)
(ENNReal.ofReal (6 / 5)) MeasureTheory.volume ≤ centredSWSCentredMajorant z.1 ρ q u Du f s
The quantitative centred bound for eq:pressure-gradient-decomposition, with all
local source estimates extracted from the suitable weak solution.