Continuous L² curves from mollified time primitives

The mollified primitives of a field with a square-integrable time derivative are Hölder continuous L²-valued curves, with an explicit energy identity in time (prop:lps-local-strong).

noncomputable def ESS.LPS.lpsCurve (a b : ℝ) (k : CKN.Foundation.Parabolic.Vec3 → ℝ) (w r : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (t : ℝ) (h : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsPrim a b k w r x t) 2 MeasureTheory.volume) : ↥(MeasureTheory.Lp ℝ 2 MeasureTheory.volume)

The time slice of the mollified primitive as an element of L²(ℝ³).

Equations

• ESS.LPS.lpsCurve a b k w r t h = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => ESS.LPS.lpsPrim a b k w r x t) h

theorem ESS.LPS.lps_prim_memLp {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 : ℝ} (ht : t ∈ Set.Icc a b) : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsPrim a b k w r x t) 2 MeasureTheory.volume

theorem ESS.LPS.lpsCurve_eq {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 : ℝ} (ht : t ∈ Set.Icc a b) : lpsCurve a b k w r t ⋯ = MeasureTheory.MemLp.toLp (fun (x : CKN.Foundation.Parabolic.Vec3) => lpsPrim a b k w r x t) ⋯

theorem ESS.LPS.lpsCurve_norm_sq {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 : ℝ} (ht : t ∈ Set.Icc a b) : ‖lpsCurve a b k w r t ⋯‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsPrim a b k w r x t ^ 2

theorem ESS.LPS.lpsCurve_sub_norm_sq {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 l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) {t : ℝ} (ht : t ∈ Set.Icc a b) : ‖lpsCurve a b k w r t ⋯ - lpsCurve a b l w r t ⋯‖ ^ 2 = ∫ (x : CKN.Foundation.Parabolic.Vec3), lpsPrim a b (k - l) w r x t ^ 2

theorem ESS.LPS.lpsCurve_dist_sq_le_time {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 t' : ℝ} (ht : t ∈ Set.Icc a b) (ht' : t' ∈ Set.Icc a b) (htt : t' ≤ t) : ‖lpsCurve a b k w r t ⋯ - lpsCurve a b k w r t' ⋯‖ ^ 2 ≤ (t - t') * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, CKN.vlConvT k r p.1 p.2 ^ 2

The curve of a mollified primitive is Hölder continuous in time.

theorem ESS.LPS.lpsCurve_continuous {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) : Continuous fun (t : ↑(Set.Icc a b)) => lpsCurve a b k w r ↑t ⋯

theorem ESS.LPS.lps_curve_dist_sq_le {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 l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) {U V : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hUm : MeasureTheory.StronglyMeasurable U) (hVm : MeasureTheory.StronglyMeasurable V) (hU : MeasureTheory.MemLp U 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hV : MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (c : ℝ) (hpair : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT (k - l) w x s * CKN.vlConvT (k - l) r x s = c * ∫ (x : CKN.Foundation.Parabolic.Vec3), U (x, s) * V (x, s)) {t : ℝ} (ht : t ∈ Set.Icc a b) : ‖lpsCurve a b k w r t ⋯ - lpsCurve a b l w r t ⋯‖ ^ 2 ≤ ((b - a)⁻¹ * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, CKN.vlConvT (k - l) w p.1 p.2 ^ 2) + |c| * ((∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, U p ^ 2) + ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, V p ^ 2)

The uniform Cauchy estimate for two mollified curves, in terms of the L² size of the convolved field and of a pair of dual fields whose slice pairing represents the slice pairing of the convolutions.

theorem ESS.LPS.lps_slab_sq_sub_le {a b : ℝ} {f g h : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hf : MeasureTheory.MemLp f 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hg : MeasureTheory.MemLp g 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hh : MeasureTheory.MemLp h 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (f p - g p) ^ 2 ≤ (2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (f p - h p) ^ 2) + 2 * ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (g p - h p) ^ 2

A slab integral of a square of a convolution difference is bounded by the two distances to a common limit.

theorem ESS.LPS.lps_slab_conv_sub_eq {a b : ℝ} {w : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hwm : MeasureTheory.StronglyMeasurable w) (hw : MeasureTheory.MemLp w 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) {k l : CKN.Foundation.Parabolic.Vec3 → ℝ} (hk : CKN.IsVlKernel k) (hl : CKN.IsVlKernel l) : ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, CKN.vlConvT (k - l) w p.1 p.2 ^ 2 = ∫ (p : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab a b, (CKN.vlConvT k w p.1 p.2 - CKN.vlConvT l w p.1 p.2) ^ 2

The convolution with a difference of kernels is the difference of the convolutions on almost every time slice.

theorem ESS.LPS.lps_integral_mul_tendsto {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {F G : ℕ → α → ℝ} {f g : α → ℝ} (hF : ∀ (n : ℕ), MeasureTheory.MemLp (F n) 2 μ) (hG : ∀ (n : ℕ), MeasureTheory.MemLp (G n) 2 μ) (hf : MeasureTheory.MemLp f 2 μ) (hg : MeasureTheory.MemLp g 2 μ) (hFf : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), (F n x - f x) ^ 2 ∂μ) Filter.atTop (nhds 0)) (hGg : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), (G n x - g x) ^ 2 ∂μ) Filter.atTop (nhds 0)) : Filter.Tendsto (fun (n : ℕ) => ∫ (x : α), F n x * G n x ∂μ) Filter.atTop (nhds (∫ (x : α), f x * g x ∂μ))

Convergence of the pairing of two L²-convergent sequences.

theorem ESS.LPS.lpsCurve_energy_identity {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) {P Q : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hP : MeasureTheory.MemLp P 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (hQ : MeasureTheory.MemLp Q 2 (MeasureTheory.volume.restrict (CKN.vlSlab a b))) (c : ℝ) (hpair : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a b), ∫ (x : CKN.Foundation.Parabolic.Vec3), CKN.vlConvT k w x s * CKN.vlConvT k r x s = c * ∫ (x : CKN.Foundation.Parabolic.Vec3), P (x, s) * Q (x, s)) {s t : ℝ} (hs : s ∈ Set.Icc a b) (ht : t ∈ Set.Icc a b) (hst : s ≤ t) : ‖lpsCurve a b k w r t ⋯‖ ^ 2 - ‖lpsCurve a b k w r s ⋯‖ ^ 2 = 2 * c * ∫ (z : CKN.Foundation.Parabolic.Vec3 × ℝ) in CKN.vlSlab s t, P z * Q z

The energy identity of a mollified curve, expressed through the dual pair.