Endpoint mixed norms of convection products #
Products of an L∞_t L²_x factor or an L²_t L∞_x factor with a space-time
L² gradient factor lie in L²_t L¹_x or L¹_t L²_x respectively
(lem:lps-comparison).
theorem
ESS.lps_eLpNorm_two_le_sqrt
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
{C : ℝ}
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
(hC : ∫ (x : CKN.Foundation.Parabolic.Vec3), f x ^ 2 ≤ C)
:
A square-integrable function with bounded squared integral has bounded
L² seminorm.
theorem
ESS.lps_slice_eLpNorm_two_aemeasurable
{T : ℝ}
{B : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hB : MeasureTheory.AEStronglyMeasurable B (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
AEMeasurable
(fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => B (x, t)) 2 MeasureTheory.volume)
(MeasureTheory.volume.restrict (Set.Ioo 0 T))
The slice L² norm of a slab-measurable function is measurable in time.
theorem
ESS.lps_endpoint_product_l2_l1
{T : ℝ}
{A B : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{K : ENNReal}
(hB : MeasureTheory.MemLp B 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hASlice :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ)) 2 MeasureTheory.volume)
(hK : K ≠ ⊤)
(hAK :
∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ)) 2 MeasureTheory.volume ≤ K)
:
(∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ) * B (x, τ)) (ENNReal.ofReal 1)
MeasureTheory.volume) ∧ ∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ) * B (x, τ)) (ENNReal.ofReal 1)
MeasureTheory.volume ^ 2 < ⊤
An L∞_t L²_x factor times a space-time L² factor lies in L²_t L¹_x.
theorem
ESS.lps_endpoint_product_linf_l2
{T : ℝ}
{A B : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
{β : ℝ → ℝ}
(hA : MeasureTheory.AEStronglyMeasurable A (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
(hB : MeasureTheory.MemLp B 2 (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), |A (x, τ)| ≤ β τ)
(hβint : ∫⁻ (τ : ℝ) in Set.Ioo 0 T, ENNReal.ofReal (β τ) ^ 2 < ⊤)
:
(∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ) * B (x, τ)) (ENNReal.ofReal 2)
MeasureTheory.volume) ∧ ∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => A (x, τ) * B (x, τ)) (ENNReal.ofReal 2)
MeasureTheory.volume ^ 1 < ⊤
An L²_t L∞_x factor times a space-time L² factor lies in L¹_t L²_x.