Weak derivatives at every time for continuous curves #
If a space-time family has a distributional spatial derivative on a slab and
its time slices agree almost everywhere with curves continuous in L², then
the curves satisfy the weak derivative relation at every time of the closed
interval: the tested relation is continuous in time and vanishes after
integration against every time test.
theorem
ESS.integral_slab_separated
{a b : ℝ}
{F : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{g : CKN.Foundation.Parabolic.Vec3 → ℝ}
{θ : ℝ → ℝ}
(hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hg : Continuous g)
(hgc : HasCompactSupport g)
(hθ : Continuous θ)
(hθb : ∃ (C : ℝ), ∀ (t : ℝ), ‖θ t‖ ≤ C)
:
Fubini for a square-integrable field against a separated test.
theorem
ESS.curve_weakPartial_of_slab
{a b : ℝ}
(hab : a < b)
{j : Fin 3}
{F₁ F₂ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
(hF₁ : MeasureTheory.MemLp F₁ 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hF₂ : MeasureTheory.MemLp F₂ 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b)))
(hweak : IsSpaceTimeWeakPartial (CKN.vlSlab a b) j F₁ F₂)
{Z₁ Z₂ : ↑(Set.Icc a b) → ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)}
(hZ₁ : Continuous Z₁)
(hZ₂ : Continuous Z₂)
(h₁ :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (ht : t ∈ Set.Icc a b),
↑↑(Z₁ ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, t))
(h₂ :
∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ (ht : t ∈ Set.Icc a b),
↑↑(Z₂ ⟨t, ht⟩) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, t))
(ψ : CKN.Foundation.Parabolic.Vec3 → ℝ)
(hψ : ContDiff ℝ (↑⊤) ψ)
(hψc : HasCompactSupport ψ)
(t : ↑(Set.Icc a b))
:
∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(Z₁ t) x * CKN.spatialDeriv ψ j x = -∫ (x : CKN.Foundation.Parabolic.Vec3), ↑↑(Z₂ t) x * ψ x
The weak derivative relation for continuous curves at every time.