Slice identities from space-time identities #
prop:lps-smoothing: a space-time identity tested against products χ(t) ψ(x)
holds, for almost every time, against every spatial test ψ of a linear family.
The slab measure factors as space times the time interval.
theorem
ESS.lps_memLp_slab_of_space
{a b : ℝ}
{g : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hg : MeasureTheory.MemLp g 2 MeasureTheory.volume)
:
MeasureTheory.MemLp (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g p.1) 2
(MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b))
A square-integrable function of space alone is square-integrable on a slab.
theorem
ESS.lps_integrable_slice_pairing
{a b : ℝ}
{A : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ}
{f : CKN.Foundation.Parabolic.Vec3 → ℝ}
(hA : MeasureTheory.MemLp A 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b)))
(hf : MeasureTheory.MemLp f 2 MeasureTheory.volume)
:
MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => A p * f p.1)
(MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a b)))
The slice pairing of an L² space-time field with a spatial L² function is
integrable in time.
theorem
ESS.lps_ae_slice_test_single
{a b : ℝ}
{N : ℕ}
(A : Fin N → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hA : ∀ (k : Fin N), MeasureTheory.MemLp (A k) 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b)))
(f : Fin N → CKN.Foundation.Parabolic.Vec3 → ℝ)
(hf : ∀ (k : Fin N), MeasureTheory.MemLp (f k) 2 MeasureTheory.volume)
(hzero :
∀ (χ : ℝ → ℝ),
ContDiff ℝ (↑⊤) χ →
HasCompactSupport χ →
tsupport χ ⊆ Set.Ioo a b →
∫ (t : ℝ) in Set.Ioo a b, χ t * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin N, A k (x, t) * f k x = 0)
:
Slice identity for one fixed test: a space-time identity against χ(t)ψ(x) for every
smooth χ compactly supported in (a,b) gives the identity for almost every time.
theorem
ESS.lps_ae_slice_test_eq_zero
{a b : ℝ}
{N : ℕ}
{T : Type u_1}
[AddCommGroup T]
[Module ℝ T]
(A : Fin N → CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ)
(hA : ∀ (k : Fin N), MeasureTheory.MemLp (A k) 2 (MeasureTheory.volume.restrict (Set.univ ×ˢ Set.Ioo a b)))
(ι : T →ₗ[ℝ] Fin N → CKN.Foundation.Parabolic.Vec3 → ℝ)
(hι : ∀ (ψ : T) (k : Fin N), MeasureTheory.MemLp (ι ψ k) 2 MeasureTheory.volume)
(hzero :
∀ (ψ : T) (χ : ℝ → ℝ),
ContDiff ℝ (↑⊤) χ →
HasCompactSupport χ →
tsupport χ ⊆ Set.Ioo a b →
∫ (t : ℝ) in Set.Ioo a b, χ t * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ k : Fin N, A k (x, t) * ι ψ k x = 0)
:
Slice identity for a linear family of tests: the identity holds for almost every time against every test simultaneously.