Nonlinear gradient cancellation

Cancellation of the convection and pressure terms on compact scalar gradient tests.

theorem CKN.Leray.associatedPressureCompactGradient_nonlinearPressure_cancel {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (hgsupp : tsupport g ⊆ Set.univ ×ˢ Set.Ioo 0 T) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * u (Foundation.Parabolic.parabolicHomeomorph.symm z) j * spatialSecondPartialProd g i j z + rieszPressureSpaceTime (3 / 2) associatedPressureCompactGradient_nonlinearPressure_cancel._proof_1 (associatedPressureTensor T u) ⋯ z * rieszPressureJointLaplacian g z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The nonlinear and pressure terms cancel on a compact smooth gradient test, by the proved noncompact Riesz duality identity.

theorem CKN.Leray.associatedPressureCompactGradient_momentum_zero {T : ℝ} {a : Foundation.Parabolic.Vec3 → Foundation.Parabolic.Vec3} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} (hLH : IsLerayHopfSolution T a u Du) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (hgsupp : tsupport g ⊆ Set.univ ×ˢ Set.Ioo 0 T) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), -∑ i : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * timePartialProd (spatialPartialProd g i) z - ∑ i : Fin 3, ∑ j : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * u (Foundation.Parabolic.parabolicHomeomorph.symm z) j * spatialSecondPartialProd g i j z + ∑ i : Fin 3, ∑ j : Fin 3, Du (Foundation.Parabolic.parabolicHomeomorph.symm z) i j * spatialSecondPartialProd g i j z - rieszPressureSpaceTime (5 / 3) associatedPressureCompactGradient_momentum_zero._proof_1 (associatedPressureTensor T u) ⋯ z * rieszPressureJointLaplacian g z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The complete Leray momentum functional vanishes on the gradient of a compact smooth scalar potential, for the canonical associated pressure.