The cross-testing identity

For two finite-energy weak solutions with pressures, one of which lies in space-time L⁵, the pairing of their slices at almost every time equals the initial pairing minus the time integrals of the convection and gradient pairings. This is the cross-testing identity of lem:pv-serrin-uniqueness, obtained here without Serrin regularity: the pairing is computed on mollified slices and the mollification and cutoff are removed.

theorem ESS.serrin_intervalIntegral_eq_slab {t : ℝ} (ht : 0 ≤ t) {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) : ∫ (τ : ℝ) in 0..t, ∫ (y : CKN.Foundation.Parabolic.Vec3), F (y, τ) = ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), F q

A time integral of spatial integrals is the space-time integral over the slab, for an integrable density.

theorem ESS.serrin_holder_ofReal {p q : ℝ} (hp : 0 < p) (hq : 0 < q) (h : p⁻¹ + q⁻¹ = 1) : (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) 1

Conjugate real exponents give a Hölder triple of ENNReal.ofReal exponents.

theorem ESS.serrin_holder_ofReal3 {p q r : ℝ} (hp : 0 < p) (hq : 0 < q) (hr : 0 < r) (h : p⁻¹ + q⁻¹ = r⁻¹) : (ENNReal.ofReal p).HolderTriple (ENNReal.ofReal q) (ENNReal.ofReal r)

Real exponents with 1/p + 1/q = 1/r give a Hölder triple.

theorem ESS.serrin_one_le_ofReal {p : ℝ} (hp : 1 ≤ p) : 1 ≤ ENNReal.ofReal p

1 ≤ ofReal p for 1 ≤ p.

theorem ESS.serrin_convection_memLp {T r s : ℝ} (hr : 0 < r) (hs : 0 < s) (hrs : r⁻¹ + 2⁻¹ = s⁻¹) {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dz : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw : MeasureTheory.MemLp w (ENNReal.ofReal r) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hDz : MeasureTheory.MemLp Dz 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (k : Fin 3) : MeasureTheory.MemLp (fun (q : CKN.Foundation.Parabolic.ParabolicPoint) => ∑ j : Fin 3, w q j * Dz q k j) (ENNReal.ofReal s) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))

Convection terms ∑ⱼ wⱼ ∂ⱼ zₖ of a field in L^r with a square-integrable gradient.

theorem ESS.serrin_intervalIntegrable_of_slab {t : ℝ} (ht : 0 ≤ t) {F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.Integrable F (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 t)))) : IntervalIntegrable (fun (τ : ℝ) => ∫ (y : CKN.Foundation.Parabolic.Vec3), F (y, τ)) MeasureTheory.volume 0 t

The spatial integrals of an integrable slab density are interval integrable.

theorem ESS.serrinMol_initial {T : ℝ} {a : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du p) (n : ℕ) (k : Fin 3) (y : CKN.Foundation.Parabolic.Vec3) : serrinMol u (serrinKernel n) k y 0 = CKN.mollify (fun (x : CKN.Vec 3) => a x k) (serrinRadius n) ⋯ y

The initial mollified components are the mollified datum.

theorem ESS.serrin_slice_pairing_limit {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : Filter.Tendsto (fun (n : ℕ) => ∫ (y : CKN.Foundation.Parabolic.Vec3), serrinCutoff n y * CKN.mollify f (serrinRadius n) ⋯ y * CKN.mollify g (serrinRadius n) ⋯ y) Filter.atTop (nhds (∫ (y : CKN.Foundation.Parabolic.Vec3), f y * g y))

Cutoff-weighted pairings of mollified square-integrable fields converge.

theorem ESS.serrin_cross_identity {T : ℝ} {a b : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {u v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pu pv : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsSerrinWeakSolution T a u Du pu) (hV : IsSerrinWeakSolution T b v Dv pv) (hu5 : MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) (hv103 : MeasureTheory.MemLp v (ENNReal.ofReal (10 / 3)) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T)))) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), (∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, v (x, t) k * u (x, t) k) - ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin 3, b x k * a x k = ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, u q k * ∑ j : Fin 3, v q j * Dv q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Du q k j * Dv q k j) + ((-∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, v q k * ∑ j : Fin 3, u q j * Du q k j) - ∫ (q : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo 0 t), ∑ k : Fin 3, ∑ j : Fin 3, Dv q k j * Du q k j)

The cross-testing identity for two finite-energy weak solutions with pressures, the first in space-time L⁵ and the second in L^{10/3}.