Time-cutoff test fields and their L² time continuity

Multiplying a space-time test field by a smooth cutoff in time gives a test field on a shorter slab; its time derivative splits by the product rule. A compactly supported continuous field is continuous in time with values in L² (lem:lps-continuation).

theorem ESS.lps_cutoff_test_mem_right {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b c β : ℝ} {η : ℝ → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → V} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) (hη : ContDiff ℝ (↑⊤) η) (hηs : tsupport η ⊆ Set.Iic β) (hβ : β < b) : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b)

A test field on (a, c) multiplied by a smooth time cutoff supported before β < b is a test field on (a, b).

theorem ESS.lps_cutoff_test_mem_left {V : Type} [NormedAddCommGroup V] [NormedSpace ℝ V] {a b c α : ℝ} {η : ℝ → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → V} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) (hη : ContDiff ℝ (↑⊤) η) (hηs : tsupport η ⊆ Set.Ici α) (hα : b < α) : (fun (z : CKN.Foundation.Parabolic.Vec3 × ℝ) => η z.2 • φ z) ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo b c)

A test field on (a, c) multiplied by a smooth time cutoff supported after α > b is a test field on (b, c).

theorem ESS.lps_cutoff_timePartial {η : ℝ → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hφ : ContDiff ℝ (↑⊤) φ) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.timePartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => η y.2 * φ y) z = deriv η z.2 * φ z + η z.2 * CKN.timePartial φ z

Product rule for the time derivative of a cutoff test field.

theorem ESS.lps_cutoff_spatialPartial {η : ℝ → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (j : Fin 3) (z : CKN.Foundation.Parabolic.ParabolicPoint) : CKN.spatialPartial (fun (y : CKN.Foundation.Parabolic.ParabolicPoint) => η y.2 * φ y) j z = η z.2 * CKN.spatialPartial φ j z

Spatial derivatives commute with the time cutoff.

theorem ESS.lps_test_slice_l2_tendsto {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : Continuous φ) (hφc : HasCompactSupport φ) (b : ℝ) : Filter.Tendsto (fun (t : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => φ (x, t) - φ (x, b)) 2 MeasureTheory.volume) (nhds b) (nhds 0)

A continuous compactly supported field is continuous in time with values in L².

theorem ESS.lps_abs_integral_mul_le {f g : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf : MeasureTheory.MemLp f 2 MeasureTheory.volume) (hg : MeasureTheory.MemLp g 2 MeasureTheory.volume) : |∫ (x : CKN.Foundation.Parabolic.Vec3), f x * g x| ≤ (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal * (MeasureTheory.eLpNorm g 2 MeasureTheory.volume).toReal

Cauchy–Schwarz for scalar L² functions.

theorem ESS.lps_pairing_tendsto {ι : Type} {l : Filter ι} {f g : ι → CKN.Foundation.Parabolic.Vec3 → ℝ} {f₀ g₀ : CKN.Foundation.Parabolic.Vec3 → ℝ} (hf₀ : MeasureTheory.MemLp f₀ 2 MeasureTheory.volume) (hg₀ : MeasureTheory.MemLp g₀ 2 MeasureTheory.volume) (hf : ∀ᶠ (i : ι) in l, MeasureTheory.MemLp (f i) 2 MeasureTheory.volume) (hg : ∀ᶠ (i : ι) in l, MeasureTheory.MemLp (g i) 2 MeasureTheory.volume) (hfl : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => f i x - f₀ x) 2 MeasureTheory.volume) l (nhds 0)) (hgl : Filter.Tendsto (fun (i : ι) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => g i x - g₀ x) 2 MeasureTheory.volume) l (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (x : CKN.Foundation.Parabolic.Vec3), f i x * g i x) l (nhds (∫ (x : CKN.Foundation.Parabolic.Vec3), f₀ x * g₀ x))

The L² pairing is continuous along families that converge in L².