Compact-gradient core

Time and weak-gradient cancellations for compact scalar gradient tests.

theorem CKN.Leray.associatedPressurePotentialDecay_of_compactSupport {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) : RieszPressurePotentialDecay g

A smooth compactly supported scalar test satisfies the decay hypotheses used in the noncompact Riesz duality identity.

theorem CKN.Leray.associatedPressureTimeSpatialPartialProd_commute {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : timePartialProd (spatialPartialProd g i) z = spatialPartialProd (timePartialProd g) i z

The product-coordinate time derivative commutes with a spatial partial derivative on a smooth scalar test.

theorem CKN.Leray.associatedPressureCompactGradient_timeTerm_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) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, u (Foundation.Parabolic.parabolicHomeomorph.symm z) i * timePartialProd (spatialPartialProd g i) z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The velocity pairs to zero with the time derivative of a compact smooth gradient test, by its weak divergence.

theorem CKN.Leray.associatedPressureSpatialTriple_commute {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (i j : Fin 3) (z : Foundation.Parabolic.Vec3 × ℝ) : spatialPartialProd (spatialSecondPartialProd g i j) j z = spatialPartialProd (spatialSecondPartialProd g j j) i z

A third spatial derivative has the coordinate symmetry used in gradient tests.

theorem CKN.Leray.associatedPressureCompact_memLp_two {T : ℝ} {f : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : ContDiff ℝ (↑⊤) f) (hfc : HasCompactSupport f) : MeasureTheory.MemLp f 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

A compact smooth scalar test is square-integrable on a finite time slab.

theorem CKN.Leray.associatedPressureCompactGradient_viscosity_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) : ∫ (z : Foundation.Parabolic.Vec3 × ℝ), ∑ i : Fin 3, ∑ j : Fin 3, Du (Foundation.Parabolic.parabolicHomeomorph.symm z) i j * spatialSecondPartialProd g i j z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The weak-gradient terms cancel on a compact smooth scalar gradient test. This is the viscous cancellation needed when the test is decomposed into its solenoidal and gradient parts.