Gradient Slot Duhamel Atoms #
Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.
theorem
CKN.Core.Step3.gradientSlot_tested_integrable_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)
{Dp : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3}
(hDpInt :
∀ (i : Fin 3),
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i)
(MeasureTheory.volume.restrict (spaceTimeSet Ω' J)))
{ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hψ : ψ ∈ spaceTimeTestFunction Set.univ Set.univ)
(i : Fin 3)
:
MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => u z i * (timePartial φ z * ψ z))
MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => f z i * (φ z * ψ z)) MeasureTheory.volume ∧ (∀ (j : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
u z i * u z j * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w * ψ w) j z)
MeasureTheory.volume) ∧ (∀ (j : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => Du z i j * (spatialPartial φ j z * ψ z))
MeasureTheory.volume) ∧ (∀ (j : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => u z i * (spatialPartial φ j z * spatialPartial ψ j z))
MeasureTheory.volume) ∧ (∀ (j : Fin 3),
MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => u z i * (spatialSecondPartial φ j j z * ψ z))
MeasureTheory.volume) ∧ MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) =>
p z * spatialPartial (fun (w : Foundation.Parabolic.ParabolicPoint) => φ w * ψ w) i z)
MeasureTheory.volume ∧ MeasureTheory.Integrable (fun (z : Foundation.Parabolic.ParabolicPoint) => Dp z i * (φ z * ψ z))
MeasureTheory.volume ∧ MeasureTheory.Integrable
(fun (z : Foundation.Parabolic.ParabolicPoint) => φ z * ψ z * localizedConvection u Du z i)
MeasureTheory.volume
Integrability of the atoms of the cutoff-tested local equation of paper
label lem:local-equation. Given a suitable weak solution, a spatial test
cutoff φ supported in a local box, a second smooth compactly supported
factor ψ, and a pressure gradient integrable on that box, every term of the
tested equation — the time derivative slot, the force term, the convective
products, the gradient slot, the mixed derivative slots, the pressure slot,
the pressure-gradient slot, and the localization of the convection — is
integrable on all of space-time.