The bilinear estimate for the Duhamel map

For velocities in L⁵ ∩ L⁴ of the slab ℝ³ × (0, σ), the forcing tensor lies in L^{5/2} ∩ L² and vanishes off the slab, and the Duhamel map of prop:pv-local-solution is quadratically Lipschitz for the norm ‖·‖₅ + ‖·‖₄, with a constant independent of σ.

theorem ESS.pvSlabTensor_memLp_both {σ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU5 : MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (hU4 : MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (i j : Fin 3) : MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume ∧ MeasureTheory.MemLp (pvSlabTensor σ U U i j) (ENNReal.ofReal 2) MeasureTheory.volume

The quadratic tensor of a velocity in L⁵ ∩ L⁴ of the slab lies in L^{5/2} ∩ L².

theorem ESS.pvSlabForce_memLp_both {σ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hU5 : MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (hU4 : MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) (i j : Fin 3) : MeasureTheory.MemLp (pvSlabForce σ U i j) (ENNReal.ofReal (5 / 2)) MeasureTheory.volume ∧ MeasureTheory.MemLp (pvSlabForce σ U i j) 2 MeasureTheory.volume

The forcing tensor of a velocity in L⁵ ∩ L⁴ of the slab lies in L^{5/2} ∩ L².

theorem ESS.pvSlabForce_pos_time {σ : ℝ} {U : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (i j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : pvSlabForce σ U i j z ≠ 0) : 0 < z.2

The forcing tensor vanishes at nonpositive times.

theorem ESS.pvLocalMap_lipschitz : ∃ (K : ENNReal), K ≠ ⊤ ∧ ∀ (a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (σ : ℝ), 0 < σ → ∀ (U V : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3), MeasureTheory.MemLp U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) → MeasureTheory.MemLp U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) → MeasureTheory.MemLp V (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) → MeasureTheory.MemLp V (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) → MeasureTheory.eLpNorm (pvLocalMap a σ U - pvLocalMap a σ V) (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm (pvLocalMap a σ U - pvLocalMap a σ V) (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) ≤ K * (MeasureTheory.eLpNorm (U - V) (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm (U - V) (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))) * (MeasureTheory.eLpNorm U (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm U (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + (MeasureTheory.eLpNorm V (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ))) + MeasureTheory.eLpNorm V (ENNReal.ofReal 4) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 σ)))))

The Duhamel map is quadratically Lipschitz for ‖·‖₅ + ‖·‖₄ on the slab, with a constant independent of the length of the slab.