Gluing strong solutions

Two strong solutions on [a, b] and [b, c] whose slices at b agree, together with their gradients, glue to a strong solution on [a, c] (lem:lps-continuation). The spatial weak derivatives glue by a time cutoff, the weak time derivative and the momentum equation through the boundary terms at the junction, which cancel because the two slices agree.

noncomputable def ESS.lpsGlue {α : Type} (b : ℝ) (f g : CKN.Foundation.Parabolic.ParabolicPoint → α) (z : CKN.Foundation.Parabolic.ParabolicPoint) : α

The field equal to f up to and including time b and to g afterwards.

Equations

• ESS.lpsGlue b f g z = if z.2 ≤ b then f z else g z

theorem ESS.lpsGlue_of_le {α : Type} {b : ℝ} {f g : CKN.Foundation.Parabolic.ParabolicPoint → α} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : z.2 ≤ b) : lpsGlue b f g z = f z

theorem ESS.lpsGlue_of_gt {α : Type} {b : ℝ} {f g : CKN.Foundation.Parabolic.ParabolicPoint → α} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : b < z.2) : lpsGlue b f g z = g z

theorem ESS.lpsEqIntegrand_glue_of_le {b : ℝ} {U W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU DW : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pU pW : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : z.2 ≤ b) : lpsEqIntegrand (lpsGlue b U W) (lpsGlue b DU DW) (lpsGlue b pU pW) φ z = lpsEqIntegrand U DU pU φ z

theorem ESS.lpsEqIntegrand_glue_of_gt {b : ℝ} {U W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU DW : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pU pW : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} {φ : CKN.Foundation.Parabolic.Vec3 × ℝ → CKN.Foundation.Parabolic.Vec3} {z : CKN.Foundation.Parabolic.ParabolicPoint} (h : b < z.2) : lpsEqIntegrand (lpsGlue b U W) (lpsGlue b DU DW) (lpsGlue b pU pW) φ z = lpsEqIntegrand W DW pW φ z

theorem ESS.lps_strong_component_slice_facts {t₀ T : ℝ} {u : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Du : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {p : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsLpsStrongSolution t₀ T u Du p) {t : ℝ} (ht : t ∈ Set.Icc t₀ T) (i : Fin 3) : Filter.Tendsto (fun (s : ℝ) => MeasureTheory.eLpNorm (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) i - u (x, t) i) 2 MeasureTheory.volume) (nhdsWithin t (Set.Icc t₀ T)) (nhds 0) ∧ MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, t) i) 2 MeasureTheory.volume ∧ ∀ s ∈ Set.Icc t₀ T, MeasureTheory.MemLp (fun (x : CKN.Foundation.Parabolic.Vec3) => u (x, s) i) 2 MeasureTheory.volume

Componentwise slice facts of a strong solution at a time of its interval.

theorem ESS.lps_strong_solution_glue {a b c : ℝ} {U W : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {DU DW : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {pU pW : CKN.Foundation.Parabolic.ParabolicPoint → ℝ} (hU : IsLpsStrongSolution a b U DU pU) (hW : IsLpsStrongSolution b c W DW pW) (htrace : (fun (x : CKN.Foundation.Parabolic.Vec3) => W (x, b)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => U (x, b)) (hgrad : (fun (x : CKN.Foundation.Parabolic.Vec3) => DW (x, b)) =ᵐ[MeasureTheory.volume] fun (x : CKN.Foundation.Parabolic.Vec3) => DU (x, b)) : IsLpsStrongSolution a c (lpsGlue b U W) (lpsGlue b DU DW) (lpsGlue b pU pW)

Two strong solutions with the same terminal and initial slice glue to a strong solution on the union of the intervals (lem:lps-continuation).