Lipschitz bounds for the forcing of the short-time construction #
The cut-off pressure is Lipschitz in L² and L^{5/2} with respect to the
quadratic tensor, and the forcing tensor -(U ⊗ U + p I) is quadratically
Lipschitz with respect to the velocity in L⁴ and L⁵ of the slab. These give
the bilinear estimate of prop:pv-local-solution.
theorem
ESS.pvSlabPressure_ae_eq_indicator
{σ r : ℝ}
(hr : 1 < r)
{W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hW2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ W W i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hWr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ W W i j) (ENNReal.ofReal r) MeasureTheory.volume)
:
pvSlabPressure σ W =ᵐ[MeasureTheory.volume]
(CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)).indicator (CKN.Leray.rieszPressureSpaceTime r hr (pvSlabTensor σ W W) hWr)
The cut-off pressure agrees almost everywhere with the cut-off Riesz
pressure at any exponent r > 1 at which the tensor is integrable.
theorem
ESS.pvSlabPressure_memLp
{σ r : ℝ}
(hr : 1 < r)
{W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hW2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ W W i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hWr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ W W i j) (ENNReal.ofReal r) MeasureTheory.volume)
:
The cut-off pressure lies in L^r whenever the tensor lies in L² ∩ L^r.
theorem
ESS.pvSlabPressure_sub_eLpNorm_le
{σ r : ℝ}
(hr : 1 < r)
{U V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hV2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ V V i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hUr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal r) MeasureTheory.volume)
(hVr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ V V i j) (ENNReal.ofReal r) MeasureTheory.volume)
:
MeasureTheory.eLpNorm (pvSlabPressure σ U - pvSlabPressure σ V) (ENNReal.ofReal r) MeasureTheory.volume ≤ ENNReal.ofReal (CKN.Leray.rieszPressureOperatorBound r hr) * ∑ i : Fin 3,
∑ j : Fin 3,
MeasureTheory.eLpNorm (pvSlabTensor σ U U i j - pvSlabTensor σ V V i j) (ENNReal.ofReal r) MeasureTheory.volume
The cut-off pressure is Lipschitz with respect to the tensor, at any exponent
r > 1 at which both tensors are integrable.
theorem
ESS.pvSlabTensor_sub_eLpNorm_le
{σ : ℝ}
{p r : ENNReal}
(hr : 1 ≤ r)
[p.HolderTriple p r]
{U V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU : MeasureTheory.MemLp U p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hV : MeasureTheory.MemLp V p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(i j : Fin 3)
:
MeasureTheory.eLpNorm (pvSlabTensor σ U U i j - pvSlabTensor σ V V i j) r MeasureTheory.volume ≤ MeasureTheory.eLpNorm (U - V) p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) * (MeasureTheory.eLpNorm U p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm V p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
The difference of two quadratic tensors is bounded by the distance of the velocities times the sum of their sizes.
theorem
ESS.pvSlabForce_sub_eLpNorm_le
{σ r : ℝ}
(hr : 1 < r)
{p : ENNReal}
[p.HolderTriple p (ENNReal.ofReal r)]
{U V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hU : MeasureTheory.MemLp U p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hV : MeasureTheory.MemLp V p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))))
(hU2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hV2 : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ V V i j) (ENNReal.ofReal 2) MeasureTheory.volume)
(hUr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal r) MeasureTheory.volume)
(hVr : ∀ (i j : Fin 3), MeasureTheory.MemLp (pvSlabTensor σ V V i j) (ENNReal.ofReal r) MeasureTheory.volume)
(i j : Fin 3)
:
MeasureTheory.eLpNorm (pvSlabForce σ U i j - pvSlabForce σ V i j) (ENNReal.ofReal r) MeasureTheory.volume ≤ (1 + 9 * ENNReal.ofReal (CKN.Leray.rieszPressureOperatorBound r hr)) * (MeasureTheory.eLpNorm (U - V) p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) * (MeasureTheory.eLpNorm U p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm V p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))))
The forcing tensor is quadratically Lipschitz in the velocity.