Gluing strong solutions across an intermediate time

Two strong solutions on [a, b] and [b, c] with the same slice at time b form a strong solution on [a, c] (lem:lps-continuation). The weak time derivative across b comes from the boundary-term lemma; the equation follows by a time cutoff around b, since it involves no time derivative of the test field once the weak time derivative is available.

theorem ESS.lps_slab_restrict_le_add (a b c : ℝ) : MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a c)) ≤ MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)) + MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c))

The slab (a, c) is covered by the slabs (a, b) and (b, c) up to the null slice t = b.

theorem ESS.lps_slab_integral_split {a b c : ℝ} (hab : a ≤ b) (hbc : b ≤ c) {f : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hf : MeasureTheory.Integrable (fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => f (CKN.Foundation.Parabolic.parabolicHomeomorph.symm q)) (MeasureTheory.volume.prod (MeasureTheory.volume.restrict (Set.Ioo a c)))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), f z = (∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), f z) + ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), f z

Integrals over adjacent slabs add, for a field whose coordinate representative is integrable for the product slab measure.

theorem ESS.lps_memLp_slab_glue {a b c : ℝ} {E : Type} [NormedAddCommGroup E] {F F₁ F₂ : CKN.Foundation.Parabolic.ParabolicPoint → E} (h₁ : MeasureTheory.MemLp F₁ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (h₂ : MeasureTheory.MemLp F₂ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c)))) (hF₁ : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → F z = F₁ z) (hF₂ : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → F z = F₂ z) : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a c)))

Square integrability on two adjacent slabs gives square integrability on the union slab.

theorem ESS.lps_glue_l2_continuity {a b c : ℝ} (hab : a < b) (hbc : b < c) {E : Type} [NormedAddCommGroup E] {F F₁ F₂ : CKN.Foundation.Parabolic.ParabolicPoint → E} (hF₁ : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → F z = F₁ z) (hF₂ : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → F z = F₂ z) (h₁ : ∀ t ∈ Set.Icc a b, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, s) - F₁ (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a b)) (nhds 0)) (h₂ : ∀ t ∈ Set.Icc b c, Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, s) - F₂ (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc b c)) (nhds 0)) (htrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, b)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, b)) (t : ℝ) : t ∈ Set.Icc a c → Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s) - F (x, t)) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc a c)) (nhds 0)

Strong L² continuity in time passes to the glued field: on each side from the corresponding piece, and at the junction because the two slices agree almost everywhere.

theorem ESS.lps_spatialPartial_cont_compact {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) (j : Fin 3) : (Continuous fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ j q) ∧ HasCompactSupport fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.spatialPartial φ j q

The spatial derivative of a test field is continuous with compact support.

theorem ESS.lps_timePartial_cont_compact {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : ContDiff ℝ (↑⊤) φ) (hφc : HasCompactSupport φ) : (Continuous fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial φ q) ∧ HasCompactSupport fun (q : CKN.Foundation.Parabolic.Vec3 × ℝ) => CKN.timePartial φ q

The time derivative of a test function is continuous with compact support.

theorem ESS.lps_slab_spatial_weak_of_slices {a c : ℝ} {F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a c)))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a c)))) (j : Fin 3) (hslice : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo a c), CKN.HasWeakPartialDerivOn Set.univ j (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, t)) fun (x : CKN.Foundation.Parabolic.Vec3) => G (x, t)) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), F z * CKN.spatialPartial φ j z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), G z * φ z

Slice-wise weak derivatives give the space-time spatial weak derivative identity for test fields.

theorem ESS.lps_time_weak_boundary_right {a b c : ℝ} (hab : a < b) {F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hw : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G z * φ z) (hcont : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s) - F (x, b)) 2 MeasureTheory.volume) (nhdsWithin b (Set.Icc a b)) (nhds 0)) (hFb : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, b)) 2 MeasureTheory.volume) (hFs : ∀ s ∈ Set.Icc a b, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s)) 2 MeasureTheory.volume) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.timePartial φ z + G z * φ z = ∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, b) * φ (x, b)

Boundary term for the weak time derivative at the right end of a slab.

theorem ESS.lps_time_weak_boundary_left {a b a₀ : ℝ} (hab : a < b) {F G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF : MeasureTheory.MemLp F 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hG : MeasureTheory.MemLp G 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hw : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G z * φ z) (hcont : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s) - F (x, a)) 2 MeasureTheory.volume) (nhdsWithin a (Set.Icc a b)) (nhds 0)) (hFb : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, a)) 2 MeasureTheory.volume) (hFs : ∀ s ∈ Set.Icc a b, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F (x, s)) 2 MeasureTheory.volume) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a₀ b)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F z * CKN.timePartial φ z + G z * φ z = -∫ (x : CKN.Foundation.Parabolic.Vec3), F (x, a) * φ (x, a)

Boundary term for the weak time derivative at the left end of a slab.

theorem ESS.lps_time_weak_glue {a b c : ℝ} (hab : a < b) (hbc : b < c) {F₁ F₂ F G₁ G₂ G : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hF₁ : MeasureTheory.MemLp F₁ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hG₁ : MeasureTheory.MemLp G₁ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo a b)))) (hF₂ : MeasureTheory.MemLp F₂ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c)))) (hG₂ : MeasureTheory.MemLp G₂ 2 (MeasureTheory.volume.restrict (CKN.spaceTimeSet Set.univ (Set.Ioo b c)))) (hw₁ : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a b), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), F₁ z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a b), G₁ z * φ z) (hw₂ : ∀ φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo b c), ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), F₂ z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo b c), G₂ z * φ z) (hcont₁ : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, s) - F₁ (x, b)) 2 MeasureTheory.volume) (nhdsWithin b (Set.Icc a b)) (nhds 0)) (hcont₂ : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, s) - F₂ (x, b)) 2 MeasureTheory.volume) (nhdsWithin b (Set.Icc b c)) (nhds 0)) (hFb₁ : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, b)) 2 MeasureTheory.volume) (hFs₁ : ∀ s ∈ Set.Icc a b, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, s)) 2 MeasureTheory.volume) (hFb₂ : MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, b)) 2 MeasureTheory.volume) (hFs₂ : ∀ s ∈ Set.Icc b c, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, s)) 2 MeasureTheory.volume) (htrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => F₂ (x, b)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => F₁ (x, b)) (hF : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → F z = F₁ z) (hF' : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → F z = F₂ z) (hG : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), z.2 ≤ b → G z = G₁ z) (hG' : ∀ (z : CKN.Foundation.Parabolic.ParabolicPoint), b < z.2 → G z = G₂ z) {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ} (hφ : φ ∈ CKN.spaceTimeTestFunction Set.univ (Set.Ioo a c)) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), F z * CKN.timePartial φ z = -∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Set.univ (Set.Ioo a c), G z * φ z

The weak time derivative passes across the gluing time: if the two pieces have weak time derivatives, are strongly L²-continuous up to the junction and agree there, the glued field has the glued weak time derivative.