Square-integrable fields on a space-time slab

Fubini on the slab ℝ³ × (a, τ): square-integrable slab fields have square-integrable time slices for almost every time, their slice energies are integrable in time, and kernel convolutions of slab fields are again square-integrable on the slab, with the L¹ norm of the kernel as the Young constant. These are the measure-theoretic steps of lem:localized-vorticity-energy of the Escauriaza–Seregin–Šverák manuscript.

theorem CKN.vlConv_integral_sq_le {k h : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) (hh : MeasureTheory.MemLp h 2 MeasureTheory.volume) : ∫ (x : Foundation.Parabolic.Vec3), vlConv k h x ^ 2 ≤ (∫ (y : Foundation.Parabolic.Vec3), |k y|) ^ 2 * ∫ (x : Foundation.Parabolic.Vec3), h x ^ 2

Young's inequality for the squared L² integral.

theorem CKN.vlSlab_integral_eq {a τ : ℝ} {F : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (vlSlab a τ))) : ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in vlSlab a τ, F p = ∫ (s : ℝ) in Set.Ioo a τ, ∫ (y : Foundation.Parabolic.Vec3), F (y, s)

Slab integrals as iterated integrals, time outside.

theorem CKN.vlSlab_slice_memLp {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hgm : MeasureTheory.StronglyMeasurable g) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a τ), MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => g (y, s)) 2 MeasureTheory.volume

Almost every time slice of a square-integrable slab field is square integrable.

theorem CKN.vlSlab_sliceSq_integrableOn {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : MeasureTheory.IntegrableOn (fun (s : ℝ) => ∫ (y : Foundation.Parabolic.Vec3), g (y, s) ^ 2) (Set.Ioo a τ) MeasureTheory.volume

The slice energy of a square-integrable slab field is integrable in time.

theorem CKN.vlSlab_integral_sq {a τ : ℝ} {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : ∫ (p : Foundation.Parabolic.Vec3 × ℝ) in vlSlab a τ, g p ^ 2 = ∫ (s : ℝ) in Set.Ioo a τ, ∫ (y : Foundation.Parabolic.Vec3), g (y, s) ^ 2

The slab energy is the time integral of the slice energies.

theorem CKN.vlConvT_stronglyMeasurable {k : Foundation.Parabolic.Vec3 → ℝ} (hk : Continuous k) {w : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : MeasureTheory.StronglyMeasurable w) : MeasureTheory.StronglyMeasurable fun (p : Foundation.Parabolic.Vec3 × ℝ) => vlConvT k w p.1 p.2

Kernel convolutions of a measurable field are jointly measurable.

theorem CKN.vlConvT_memLp {a τ : ℝ} {k : Foundation.Parabolic.Vec3 → ℝ} (hk : IsVlKernel k) {w : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hwm : MeasureTheory.StronglyMeasurable w) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : MeasureTheory.MemLp (fun (p : Foundation.Parabolic.Vec3 × ℝ) => vlConvT k w p.1 p.2) 2 (MeasureTheory.volume.restrict (vlSlab a τ))

Kernel convolutions of square-integrable slab fields are square integrable on the slab.

theorem CKN.vlSlab_memLp_mono {a τ t : ℝ} (ht : t ≤ τ) {g : Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a τ))) : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (vlSlab a t))

Restriction of a slab field to a shorter slab.