Time slices of finite-energy weak solutions #
Almost every time slice of a space-time L^q field is in L^q, and almost
every slice of a finite-energy weak solution has a square-integrable weak
gradient with vanishing trace. These are the fixed-time inputs of the
cross-testing identity in lem:pv-serrin-uniqueness.
theorem
ESS.serrin_slice_memLp_ae
{E : Type}
[NormedAddCommGroup E]
{T : ℝ}
{f : CKN.Foundation.Parabolic.ParabolicPoint → E}
{q : ENNReal}
(hq0 : q ≠ 0)
(hqtop : q ≠ ⊤)
(hf : MeasureTheory.MemLp f q (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => f (x, s)) q MeasureTheory.volume
Almost every time slice of a space-time L^q field on the slab is in L^q.
theorem
ESS.serrin_trace_zero_of_divFree
{w : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3}
{Dw : CKN.Foundation.Parabolic.Vec3 → Fin 3 → CKN.Foundation.Parabolic.Vec3}
(hw : MeasureTheory.MemLp w 2 MeasureTheory.volume)
(hDw : MeasureTheory.MemLp Dw 2 MeasureTheory.volume)
(hgrad : ∀ (i : Fin 3), CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => w x i) fun (x : CKN.Vec 3) => Dw x i)
(hdiv :
∀ (ψ : CKN.WeakTestFunction Set.univ),
∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, w x i * ψ.partialDeriv i x = 0)
:
∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Dw x i i = 0
A square-integrable weakly differentiable field that is weakly divergence free has an almost everywhere vanishing gradient trace.
theorem
ESS.serrinWeak_slices_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}
{p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ}
(hU : IsSerrinWeakSolution T a u Du p)
:
∀ᵐ (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 ∧ (∀ (i : Fin 3),
CKN.HasWeakGradientOn Set.univ (fun (x : CKN.Vec 3) => u (x, s) i) fun (x : CKN.Vec 3) => Du (x, s) i) ∧ (∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, Du (x, s) i i = 0) ∧ MeasureTheory.LocallyIntegrable (fun (x : CKN.Foundation.Parabolic.Vec3) => p (x, s)) MeasureTheory.volume
Almost every time slice of a finite-energy weak solution is square integrable with a square-integrable weak gradient of vanishing trace, and its pressure slice is locally integrable.