Mollified time primitives of a field with a square-integrable time derivative

For a slab field w whose weak time derivative r is square integrable, and a smooth compact spatial kernel k, the convolution k ⋆ w has, at every point of space, the weak time derivative k ⋆ r. It is therefore an absolutely continuous function of time, equal almost everywhere to an explicit primitive with an averaged constant (prop:lps-local-strong).

theorem ESS.LPS.lps_conv_hasWeakDeriv {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (x : CKN.Foundation.Parabolic.Vec3) : CKN.HasWeakDerivOn (Set.Ioo a b) (fun (s : ℝ) => CKN.vlConvT k w x s) fun (s : ℝ) => CKN.vlConvT k r x s

The spatial convolution of a slab field with a smooth compact kernel has, at every point of space, the convolved time derivative as weak time derivative.

noncomputable def ESS.LPS.lpsPrimConst (a b : ℝ) (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : CKN.Foundation.Parabolic.Vec3) : ℝ

The averaged constant of the mollified time primitive.

Equations

• ESS.LPS.lpsPrimConst a b k w r x = (b - a)⁻¹ * ∫ (s : ℝ) in Set.Ioo a b, CKN.vlConvT k w x s - ∫ (q : ℝ) in a..s, CKN.vlConvT k r x q

noncomputable def ESS.LPS.lpsPrim (a b : ℝ) (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (x : CKN.Foundation.Parabolic.Vec3) (t : ℝ) : ℝ

The mollified time primitive x, t ↦ c(x) + ∫ₐᵗ (k ⋆ r)(x, q) dq.

Equations

• ESS.LPS.lpsPrim a b k w r x t = ESS.LPS.lpsPrimConst a b k w r x + ∫ (q : ℝ) in a..t, CKN.vlConvT k r x q

theorem ESS.LPS.lps_conv_intervalIntegrable {a b : ℝ} {r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hab : a < b) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (x : CKN.Foundation.Parabolic.Vec3) : IntervalIntegrable (fun (s : ℝ) => CKN.vlConvT k r x s) MeasureTheory.volume a b

theorem ESS.LPS.lps_prim_increment {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hab : a < b) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (x : CKN.Foundation.Parabolic.Vec3) (s : ℝ) : s ∈ Set.Icc a b → ∀ t ∈ Set.Icc a b, lpsPrim a b k w r x t - lpsPrim a b k w r x s = ∫ (q : ℝ) in s..t, CKN.vlConvT k r x q

The mollified primitive is an interval integral of the convolved time derivative.

theorem ESS.LPS.lps_prim_ae_eq {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (x : CKN.Foundation.Parabolic.Vec3) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), CKN.vlConvT k w x t = lpsPrim a b k w r x t

The convolution of the field is, at every point and for almost every time, the mollified primitive.

theorem ESS.LPS.lps_stronglyMeasurable_timePrimitive {B : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hB : MeasureTheory.StronglyMeasurable B) (a : ℝ) : MeasureTheory.StronglyMeasurable fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => ∫ (q : ℝ) in a..p.2, B (p.1, q)

Measurability of the primitive in the time variable of a jointly measurable integrand.

theorem ESS.LPS.lps_prim_stronglyMeasurable {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) : MeasureTheory.StronglyMeasurable fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => lpsPrim a b k w r p.1 p.2

theorem ESS.LPS.lps_slab_integrable_sq {a b : ℝ} {g : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) : MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => g p ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b)))

A square-integrable slab field is square integrable for the product of the spatial measure with the restriction to (a, b].

theorem ESS.LPS.lps_prim_slice_ae {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∀ᵐ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT k w x t = lpsPrim a b k w r x t

For almost every time, the convolution of the time slice is the mollified primitive almost everywhere in space.

theorem ESS.LPS.lps_prim_energy {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hweak : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, w p * CKN.timePartial φ p = -∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, r p * φ p) {k : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) : (∀ t ∈ Set.Icc a b, MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsPrim a b k w r x t ^ 2) MeasureTheory.volume) ∧ MeasureTheory.Integrable (fun (p : CKN.Foundation.Parabolic.Vec3 × ℝ) => lpsPrim a b k w r p.1 p.2 ^ 2) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioc a b))) ∧ ∀ s ∈ Set.Icc a b, ∀ t ∈ Set.Icc a b, s ≤ t → (∫ (x : CKN.Foundation.Parabolic.Vec3), lpsPrim a b k w r x t ^ 2) - ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsPrim a b k w r x s ^ 2 = 2 * ∫ (q : ℝ) in s..t, ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsPrim a b k w r x q * CKN.vlConvT k r x q

Square integrability of the mollified primitive at every time and on the slab, and its energy identity in time (prop:lps-local-strong).

theorem ESS.LPS.lps_prim_sub_kernel {a b : ℝ} {w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hab : a < b) (hwm : MeasureTheory.StronglyMeasurable w) (hrm : MeasureTheory.StronglyMeasurable r) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hr : MeasureTheory.MemLp r 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) {k l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) (x : CKN.Foundation.Parabolic.Vec3) {t : ℝ} (ht : t ∈ Set.Icc a b) : lpsPrim a b (k - l) w r x t = lpsPrim a b k w r x t - lpsPrim a b l w r x t

The mollified primitive is linear in the kernel.