Harmonic Remainder Slice SWS #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
noncomputable def
CKN.harmonicRemainderForceBound
(z : Foundation.Parabolic.ParabolicPoint)
{ρ : ℝ}
(hρ : 0 < ρ)
(f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3)
(s : ℝ)
:
Nonnegative growth coefficient for the forcing part of the harmonic pressure remainder.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
CKN.pressure_force_inner_memLp_and_lpNorm_ae_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)
{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), MeasureTheory.MemLp (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ∧ 0 ≤ harmonicRemainderForceBound z hρ f s ∧ MeasureTheory.lpNorm (pressureP7 (mollifiedBallCutoff z.1 hρ) f s + pressureP8 (mollifiedBallCutoff z.1 hρ) f s)
(ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall z.1 (13 * ρ / 20))) ≤ harmonicRemainderForceBound z hρ f s