Local Energy Weak Gradient

Supporting estimates for the Navier–Stokes development.

theorem CKN.energyL2_components_memLp {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (henergy : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0))) ∧ MeasureTheory.MemLp Du 2 (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))

The local energy bound makes velocity and weak gradient square integrable on the cylinder. This is the L² input for local mollification.

theorem CKN.essLocal_sliceGradient_integrationByParts {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hu : MeasureTheory.AEStronglyMeasurable u (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (hDu : MeasureTheory.AEStronglyMeasurable Du (MeasureTheory.volume.restrict (spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0)))) (henergy : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in spaceTimeSet (Foundation.Parabolic.vec3Ball 0 1) (Set.Ioo (-1) 0), ‖u z‖ₑ ^ 2 + ‖Du z‖ₑ ^ 2 < ⊤) (hgrad : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo (-1) 0), ∀ (i : Fin 3), HasWeakGradientOn (Foundation.Parabolic.vec3Ball 0 1) (fun (x : Vec 3) => u (x, t) i) fun (x : Vec 3) => Du (x, t) i) {ψ : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hψ : ContDiff ℝ (↑⊤) ψ) (hψc : HasCompactSupport ψ) (hψsupport : tsupport ψ ⊆ Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0) (i j : Fin 3) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0, u z i * spatialPartial (have this := ψ; this) j z = -∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Foundation.Parabolic.vec3Ball 0 1 ×ˢ Set.Ioo (-1) 0, Du z i j * ψ z

Slice weak gradients give the space-time integration-by-parts identity on the full local cylinder. This is the product-coordinate form used by the mollified-gradient argument.