Mixed norm limits of the cross densities

As the mollification radius tends to zero and the cutoff radius to infinity, the space-time integral of a cross density converges to minus the convection pairing and the gradient pairing. This is the limit passage on the right side of the cross-testing identity in lem:pv-serrin-uniqueness.

theorem ESS.lps_real_holder_pair {p q : ℝ} (hp : 0 < p) (hq : 0 < q) (h : p⁻¹ + q⁻¹ = 1) : p.HolderConjugate q

Real exponents with 1/p + 1/q = 1 are Hölder conjugate.

theorem ESS.lps_coordinate_aesm {T : ℝ} {F : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (i : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => F z i) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

A coordinate of an almost everywhere strongly measurable vector field on a slab is almost everywhere strongly measurable.

theorem ESS.lps_gradient_entry_aesm {T : ℝ} {F : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hF : MeasureTheory.AEStronglyMeasurable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (i j : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => F z i j) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

An entry of an almost everywhere strongly measurable gradient field on a slab is almost everywhere strongly measurable.

theorem ESS.lps_convection_aesm {T : ℝ} {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw : MeasureTheory.AEStronglyMeasurable w (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDw : MeasureTheory.AEStronglyMeasurable Dw (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (k : Fin 3) : MeasureTheory.AEStronglyMeasurable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w z j * Dw z k j) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

The advective convection of measurable fields is almost everywhere strongly measurable on a slab.

theorem ESS.lps_cross_density_limit_of_pairing {t T : ℝ} (ht : t ≤ T) {w z : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw Dz : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pw : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hPairInt : ∀ (k : Fin 3), ∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => serrinCutoff n q.1 * serrinSM (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) n q * serrinSM (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w r j * Dw r k j) n q) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) (hPairLim : ∀ (k : Fin 3), Filter.Tendsto (fun (n : ℕ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCutoff n q.1 * serrinSM (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) n q * serrinSM (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w r j * Dw r k j) n q) Filter.atTop (nhds (∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), z q k * ∑ j : Fin 3, w q j * Dw q k j))) (hPairProd : ∀ (k : Fin 3), MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => z q k * ∑ j : Fin 3, w q j * Dw q k j) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) (hDz : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dz r k j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDw : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dw r k j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hz2 : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hz52 : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hpw : MeasureTheory.MemLp pw (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : (∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity w Dw pw z Dz n (serrinCutoff n)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity w Dw pw z Dz n (serrinCutoff n) q) Filter.atTop (nhds ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, z q k * ∑ j : Fin 3, w q j * Dw q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dz q k j * Dw q k j))

Integrability and the limit of the space-time integral of a cross density, given the pairing limit of the convection term. The remaining terms are controlled by the L² gradients, the L^(5/2) tested velocity and the L^(5/3) pressure.

theorem ESS.lps_mixed_cross_density_limit {t T px qx pt qt : ℝ} (ht : t ≤ T) {w z : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw Dz : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pw : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hpx1 : 1 ≤ px) (hqx1 : 1 ≤ qx) (hpt1 : 1 ≤ pt) (hqt1 : 1 ≤ qt) (hSpace : px.HolderConjugate qx) (hTime : pt.HolderConjugate qt) (hzMeas : ∀ (k : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hNMeas : ∀ (k : Fin 3), MeasureTheory.AEStronglyMeasurable (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w r j * Dw r k j) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hzSlice : ∀ (k : Fin 3), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, τ) k) (ENNReal.ofReal px) MeasureTheory.volume) (hNSlice : ∀ (k : Fin 3), ∀ᵐ (τ : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, w (x, τ) j * Dw (x, τ) k j) (ENNReal.ofReal qx) MeasureTheory.volume) (hzMoment : ∀ (k : Fin 3), ∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => z (x, τ) k) (ENNReal.ofReal px) MeasureTheory.volume ^ pt < ⊤) (hNMoment : ∀ (k : Fin 3), ∫⁻ (τ : ℝ) in Set.Ioo 0 T, MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ j : Fin 3, w (x, τ) j * Dw (x, τ) k j) (ENNReal.ofReal qx) MeasureTheory.volume ^ qt < ⊤) (hDz : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dz r k j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDw : ∀ (k j : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => Dw r k j) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hz2 : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hz52 : ∀ (k : Fin 3), MeasureTheory.MemLp (fun (r : CKN.Foundation.Parabolic.ParabolicPoint) => z r k) (ENNReal.ofReal (5 / 2)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hpw : MeasureTheory.MemLp pw (ENNReal.ofReal (5 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : (∀ᶠ (n : ℕ) in Filter.atTop, MeasureTheory.Integrable (serrinCrossDensity w Dw pw z Dz n (serrinCutoff n)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) ∧ Filter.Tendsto (fun (n : ℕ) => ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), serrinCrossDensity w Dw pw z Dz n (serrinCutoff n) q) Filter.atTop (nhds ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, z q k * ∑ j : Fin 3, w q j * Dw q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dz q k j * Dw q k j))

Integrability and the limit of the space-time integral of a cross density when the tested velocity and the rival convection have conjugate finite mixed norms. The pressure term retains the finite-energy exponents 5/2 and 5/3.