Weak derivatives of kernel convolutions of slab fields #
A space-time weak spatial derivative is, for every kernel and at every point,
an almost-everywhere-in-time identity between convolutions. These identities
are the input of the energy identities for the specified first gradient of a
strong solution (prop:lps-local-strong).
theorem
ESS.LPS.lps_conv_deriv_ae
{a b : ℝ}
{u v : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(j : Fin 3)
(hweak :
∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b),
∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, u p * CKN.spatialPartial φ j p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, v p * φ p)
{κ : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hκ : CKN.IsVlKernel κ)
(x : CKN.Foundation.Parabolic.Vec3)
:
∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), CKN.vlConvT (CKN.vlDeriv κ j) u x s = CKN.vlConvT κ v x s
A weak spatial derivative of a slab field is, for every kernel and at every point, an almost-everywhere-in-time identity between convolutions.
theorem
ESS.LPS.lps_ae_slice_of_ae_time
{a b : ℝ}
{F G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF : MeasureTheory.StronglyMeasurable F)
(hG : MeasureTheory.StronglyMeasurable G)
(h :
∀ (x : CKN.Foundation.Parabolic.Vec3), ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), F (x, s) = G (x, s))
:
From an identity for every point and almost every time to an identity for almost every time and almost every point.