Separated space-time test fields #
A product χ(t) ψ(x) of a smooth compactly supported time cutoff and a smooth
compactly supported spatial field is a space-time test field on any slab
containing the support of χ. Its partial derivatives split accordingly
(lem:lps-H1-estimate).
theorem
ESS.lps_memLp_slab_to_prod
{a b : ℝ}
{E : Type}
[NormedAddCommGroup E]
{F : CKN.Foundation.Parabolic.ParabolicPoint → E}
{p : ENNReal}
(hF : MeasureTheory.MemLp F p (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b))))
:
MeasureTheory.MemLp
(fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => F (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) p
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))
A square-integrable field on the slab is square integrable on the product space with the product slab measure.
theorem
ESS.lps_setIntegral_slab_to_prod
{a b : ℝ}
(F : CKN.Foundation.Parabolic.ParabolicPoint → ℝ)
:
The slab integral of a field equals the product-space integral of its coordinate representative.
The support of a separated field lies in the product of the supports.
theorem
ESS.lps_separated_test_mem
{a b : ℝ}
{χ : ℝ → ℝ}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(hχc : HasCompactSupport χ)
(hχs : tsupport χ ⊆ Set.Ioo a b)
(hf : ContDiff ℝ (↑⊤) f)
(hfc : HasCompactSupport f)
:
(fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => χ z.2 * f z.1) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)
The scalar space-time test function χ(t) f(x).
theorem
ESS.lps_separated_timePartial
{χ : ℝ → ℝ}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hχ : ContDiff ℝ (↑⊤) χ)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => χ y.2 * f y.1) z = deriv χ z.2 * f z.1
The time derivative of a separated test function.
theorem
ESS.lps_separated_spatialPartial
{χ : ℝ → ℝ}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hf : ContDiff ℝ (↑⊤) f)
(j : Fin 3)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
:
CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => χ y.2 * f y.1) j z = χ z.2 * CKN.spatialDeriv f j z.1
The spatial derivative of a separated test function.