Time functions in the Gronwall argument #
The Gronwall coefficient τ ↦ ‖u(τ)‖₅⁵ is integrable in time for a space-time
L⁵ field, and the squared L² distance of two finite-energy solutions is a
measurable, essentially bounded function of time. These are the inputs of the
Gronwall step of lem:pv-serrin-uniqueness.
theorem
ESS.serrin_slice_norm5_integrable
{T : ℝ}
{u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3}
(hu5 :
MeasureTheory.MemLp u (ENNReal.ofReal 5) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo 0 T))))
:
MeasureTheory.IntegrableOn
(fun (τ : ℝ) =>
(MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, τ)) (ENNReal.ofReal 5)
MeasureTheory.volume).toReal ^ 5)
(Set.Ioo 0 T) MeasureTheory.volume
The fifth power of the slice L⁵ norm is integrable in time.
theorem
ESS.serrin_distance_aestronglyMeasurable
{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)
:
The squared L² distance of two slices is measurable in time.
theorem
ESS.serrinWeak_slice_energy_bound
{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)
:
The slice energies of a finite-energy weak solution are essentially bounded.