Weak pairings for Leray solutions

Space-time integrability and weak derivative pairings used in the pressure identity.

theorem CKN.Leray.associatedPressureSolution_velocity_memLp_two_productSlab {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) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => u (Foundation.Parabolic.parabolicHomeomorph.symm z)) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

The velocity has finite space-time energy on the ordinary product-space time slab.

theorem CKN.Leray.associatedPressureSolution_gradient_memLp_two_productSlab {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) : MeasureTheory.MemLp (fun (z : Foundation.Parabolic.Vec3 × ℝ) => Du (Foundation.Parabolic.parabolicHomeomorph.symm z)) 2 (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)))

The weak gradient has finite space-time energy on the ordinary product-space time slab.

def CKN.Leray.associatedPressureScalarSliceWeakTest {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hgc : HasCompactSupport g) (t : ℝ) : WeakTestFunction Set.univ

A compactly supported smooth space-time function restricted to a spatial weak test.

Equations

• CKN.Leray.associatedPressureScalarSliceWeakTest hg hgc t = { toFun := fun (x : CKN.Vec 3) => g (x, t), contDiff := ⋯, hasCompactSupport := ⋯, tsupport_subset := ⋯ }

theorem CKN.Leray.associatedPressureWeakDivergence_pairing_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 * spatialPartialProd g i z ∂MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo 0 T)) = 0

The Leray weak-divergence clause pairs to zero with any compact smooth scalar test on the finite-time slab.

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

The Leray weak-gradient clause gives the distributional integration by parts formula against any compact smooth scalar test on the finite-time slab.