Endpoint cutoff pairings on the space-time slab

The two endpoint pairings needed for the convection term of the cross density: an L²_t L∞_x velocity against an L²_t L¹_x convection, and an L∞_t L²_x velocity against an L¹_t L²_x convection (lem:lps-comparison).

theorem ESS.lps_slice_aesm {T : ℝ} {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.AEStronglyMeasurable (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, t)) MeasureTheory.volume

Almost every time slice of a slab-measurable function is measurable.

theorem ESS.lps_slab_lintegral_eq {T : ℝ} {h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hh : MeasureTheory.AEStronglyMeasurable h (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 T), ‖h z‖ₑ = ∫⁻ (t : ℝ) in Set.Ioo 0 T, ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖h (x, t)‖ₑ

Tonelli on the slab for the extended norm of a measurable function.

theorem ESS.lps_slice_lintegral_aemeasurable {T : ℝ} {h : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hh : MeasureTheory.AEStronglyMeasurable h (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : AEMeasurable (fun (t : ℝ) => ∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖h (x, t)‖ₑ) (MeasureTheory.volume.restrict (Set.Ioo 0 T))

The slice L¹ norm of a slab-measurable function is measurable in time.

theorem ESS.lps_lintegral_mul_ne_top_of_sq {μ : MeasureTheory.Measure ℝ} {a b : ℝ → ENNReal} (ha : AEMeasurable a μ) (hb : AEMeasurable b μ) (ha2 : ∫⁻ (t : ℝ), a t ^ 2 ∂μ < ⊤) (hb2 : ∫⁻ (t : ℝ), b t ^ 2 ∂μ < ⊤) : ∫⁻ (t : ℝ), a t * b t ∂μ ≠ ⊤

Cauchy–Schwarz in time for two profiles with finite square moments.

theorem ESS.lps_endpoint_cutoff_pairing_limit_linf_l1 {T t : ℝ} (ht : t ≤ T) {f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {β : ℝ → ℝ} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hβmeas : AEMeasurable (fun (τ : ℝ) => ENNReal.ofReal (β τ)) (MeasureTheory.volume.restrict (Set.Ioo 0 T))) (hβ : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), |f (x, τ)| ≤ β τ) (hβint : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, ENNReal.ofReal (β τ) ^ 2 < ⊤) (hgSlice : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, τ)) MeasureTheory.volume) (hgMoment : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, (∫⁻ (x : CKN.Foundation.Parabolic.Vec3), ‖g (x, τ)‖ₑ) ^ 2 < ⊤) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f z * g z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t))) ∧ (∀ (n : ℕ), MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinCutoff n z.1 * serrinSM f n z * serrinSM g n z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCutoff n z.1 * serrinSM f n z * serrinSM g n z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), f z * g z))

Endpoint pairing of a velocity component with an essentially bounded L²_t spatial profile against an L²_t L¹_x convection component: the cutoff-weighted product of the spatial mollifications is integrable and its integral converges to that of the product.

theorem ESS.lps_endpoint_cutoff_pairing_limit_l2_l2 {T t : ℝ} (ht : t ≤ T) {f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {K : ENNReal} (hf : MeasureTheory.AEStronglyMeasurable f (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hg : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hfSlice : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, τ)) 2 MeasureTheory.volume) (hK : K ≠ ⊤) (hfBound : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, τ)) 2 MeasureTheory.volume ≤ K) (hgSlice : ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, τ)) 2 MeasureTheory.volume) (hgMoment : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g (x, τ)) 2 MeasureTheory.volume < ⊤) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => f z * g z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t))) ∧ (∀ (n : ℕ), MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => serrinCutoff n z.1 * serrinSM f n z * serrinSM g n z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCutoff n z.1 * serrinSM f n z * serrinSM g n z) Filter.atTop (nhds (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), f z * g z))

Endpoint pairing of an L∞_t L²_x velocity component against an L¹_t L²_x convection component.