Serrin Estimate

The weak derivative identity is stable under subtraction of L² fields.

theorem ESS.serrin_weakPartialDeriv_sub {f g df dg : CKN.Foundation.Parabolic.Vec3 → ℝ} {i : Fin 3} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) (hdf : MeasureTheory.MemLp df 2 MeasureTheory.volume) (hdg : MeasureTheory.MemLp dg 2 MeasureTheory.volume) (hF : CKN.HasWeakPartialDerivOn Set.univ i f df) (hG : CKN.HasWeakPartialDerivOn Set.univ i g dg) : CKN.HasWeakPartialDerivOn Set.univ i (f - g) (df - dg)

The weak derivative identity is stable under subtraction of L² fields.

theorem ESS.serrin_slice_memLp_two_ae {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} (hLH : CKN.IsLerayHopfSolution T a u Du) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s)) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => Du (x, s)) 2 MeasureTheory.volume

Almost every time slice of a Leray–Hopf field and its weak gradient are square-integrable.

theorem ESS.serrin_trilinear_young {A B C : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) (hC : 0 ≤ C) : A * B ^ (2 / 5) * C ^ (8 / 5) ≤ 1 / 2 * C ^ 2 + 32 / 5 * A ^ 5 * B ^ 2

Young's inequality in the exponents used in the relative-energy estimate for lem:pv-serrin-uniqueness.

theorem ESS.serrin_interpolation_young {K A B D N : ℝ} (hK : 0 ≤ K) (hA : 0 ≤ A) (hB : 0 ≤ B) (hD : 0 ≤ D) (hN : N ≤ K * B ^ (2 / 5) * D ^ (3 / 5)) : A * N * D ≤ 1 / 2 * D ^ 2 + 32 / 5 * (K * A) ^ 5 * B ^ 2

The spatial interpolation bound and Young's inequality give the integrable-coefficient estimate used in the zero-start comparison in lem:pv-serrin-uniqueness.

theorem ESS.serrin_vector_spatial_tenThirds {w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} (hw2 : MeasureTheory.MemLp w 2 MeasureTheory.volume) (hH1 : Fin 3 → CKN.H1Function Set.univ) (hFun : ∀ (i : Fin 3), (hH1 i).toFun = fun (x : CKN.Foundation.Parabolic.Vec3) => w x i) (hGrad : ∀ (i : Fin 3), (hH1 i).grad = fun (x : CKN.Foundation.Parabolic.Vec3) (j : Fin 3) => Dw x i j) : MeasureTheory.eLpNorm w (ENNReal.ofReal (10 / 3)) MeasureTheory.volume ≤ 3 * CKN.gagliardoNirenbergSobolevConstant ^ (3 / 5) * 2 ^ (3 / 5) * MeasureTheory.eLpNorm w 2 MeasureTheory.volume ^ (2 / 5) * MeasureTheory.eLpNorm Dw 2 MeasureTheory.volume ^ (3 / 5)

Vector-valued spatial interpolation from componentwise H¹ data. The finite-dimensional constant is kept explicit for use in the cross-testing estimate in lem:pv-serrin-uniqueness.

theorem ESS.serrin_difference_initial_trace_l2_ae {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} (hU : CKN.IsLerayHopfSolution T a u Du) : Filter.Tendsto (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) - a x) 2 MeasureTheory.volume) (nhdsWithin 0 (Set.Ioi 0) ⊓ MeasureTheory.ae (MeasureTheory.volume.restrict (Set.Ioo 0 T))) (nhds 0)

The strong initial trace of a Leray--Hopf field gives convergence of its spatial L² distance to the datum along almost every time.