Spatial weak derivatives on a slab from weak derivatives of the time slices #
If almost every time slice of a slab function has a spatial weak partial derivative, and both are
square integrable on the slabs strictly inside, then the space-time integration by parts identity
holds against smooth compactly supported tests on the slab (prop:lps-local-strong).
theorem
ESS.LPS.lps_test_slice
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hd : ContDiff ℝ (↑⊤) φ)
(hc : HasCompactSupport φ)
(t : ℝ)
:
(ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => φ (x, t)) ∧ HasCompactSupport fun (x : CKN.Foundation.Parabolic.Vec3) => φ (x, t)
A time slice of a smooth compactly supported space-time function is smooth with compact support.
theorem
ESS.LPS.lps_smooth_hasWeakPartialDerivOn
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(j : Fin 3)
:
A smooth function has its derivative as weak partial derivative on the whole space.
theorem
ESS.LPS.lps_slab_spatial_weak_of_slices
{a T : ℝ}
(hab : a < T)
(j : Fin 3)
{F G : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hslice :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a T), CKN.HasWeakPartialDerivOn Set.univ j (fun (x : CKN.Vec 3) => F (x, t)) fun (x : CKN.Vec 3) => G (x, t))
(hF :
∀ (a' b' : ℝ), a < a' → a' < b' → b' < T → MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.vlSlab a' b')))
(hG :
∀ (a' b' : ℝ), a < a' → a' < b' → b' < T → MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.vlSlab a' b')))
{φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a T))
:
∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a T, F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a T, G z * φ z
Integration by parts on a slab against smooth compactly supported tests, from weak spatial derivatives of the time slices.