Exact continuation-by-pasting for the actual projected quadratic viscous equation.

Actual nonlinear source paths commute with restriction and adjacent-interval solution pasting.

A uniform positive restart time for bounded data in the actual viscous Sobolev equation.

def EulerUniformHeatLocal.timeWindow {S : ℝ} (a T : ℝ) (ha : 0 ≤ a) (haT : a + T ≤ S) : C(↑(Set.Icc 0 T), ↑(Set.Icc 0 S))

A translated compact time window inside the prescribed coefficient interval.

Equations

• EulerUniformHeatLocal.timeWindow a T ha haT = { toFun := fun (t : ↑(Set.Icc 0 T)) => ⟨a + ↑t, ⋯⟩, continuous_toFun := ⋯ }

theorem EulerUniformHeatLocal.parabolic_mass_mono (ν s t : ℝ) (hst : s ≤ t) : s + 2 * EulerSobolevHeat.parabolicConstant ν * √s ≤ t + 2 * EulerSobolevHeat.parabolicConstant ν * √t

The mass of the actual parabolic kernel bound is monotone in nonnegative time.

theorem EulerUniformHeatLocal.exists_uniform_restart_time (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (S : ℝ) (hS : 0 < S) (R : ℝ) (hR : 0 ≤ R) (C : EulerQuadraticSource.Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : ∃ (δ : ℝ), 0 < δ ∧ δ ≤ S ∧ ∀ (a T : ℝ) (ha : 0 ≤ a) (hT : 0 ≤ T) (haT : a + T ≤ S), T ≤ δ → ∀ (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))), ‖u₀‖ ≤ R → ∃ (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))), ‖u‖ ≤ R + 1 ∧ u ⟨0, ⋯⟩ = u₀ ∧ ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (C.apply ((timeWindow a T ha haT) (Set.projIcc 0 T hT (↑t - r))) (u (Set.projIcc 0 T hT (↑t - r))))

Uniformly bounded initial Sobolev data have genuine local solutions on every time window of one fixed positive length. The length depends only on the compact coefficient bounds and the data bound, not on the restart time or state.

noncomputable def EulerWindowSource.windowSource {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 S)) X Y) (a T : ℝ) (ha : 0 ≤ a) (haT : a + T ≤ S) (u : C(↑(Set.Icc 0 T), X)) : C(↑(Set.Icc 0 T), Y)

The actual nonlinear forcing evaluated along a solution on a translated compact time window.

Equations

• EulerWindowSource.windowSource C a T ha haT u = { toFun := fun (t : ↑(Set.Icc 0 T)) => C.apply ((EulerUniformHeatLocal.timeWindow a T ha haT) t) (u t), continuous_toFun := ⋯ }

theorem EulerWindowSource.windowSource_extend {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 S)) X Y) (a T : ℝ) (ha : 0 ≤ a) (hT : 0 ≤ T) (haT : a + T ≤ S) (u : C(↑(Set.Icc 0 T), X)) (r : ℝ) (hr : r ∈ Set.Icc 0 T) : EulerVolterraConvolution.extendPath T hT (windowSource C a T ha haT u) r = C.apply ((EulerUniformHeatLocal.timeWindow a T ha haT) ⟨r, hr⟩) (EulerVolterraConvolution.extendPath T hT u r)

The clamped source has its literal nonlinear value at every time inside its actual window.

theorem EulerWindowSource.windowSource_zero {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S T : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 S)) X Y) (hT : 0 ≤ T) (hTS : T ≤ S) (u : C(↑(Set.Icc 0 T), X)) (r : ℝ) : EulerVolterraConvolution.extendPath T hT (windowSource C 0 T ⋯ ⋯ u) r = C.apply ((EulerQuadraticSource.timeInclusion hTS) (Set.projIcc 0 T hT r)) (EulerVolterraConvolution.extendPath T hT u r)

At zero offset the actual source path is exactly the initial-interval source used by the local solver.

theorem EulerWindowSource.windowSource_glue_left {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 S)) X Y) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (habS : a + b ≤ S) (u : C(↑(Set.Icc 0 a), X)) (v : C(↑(Set.Icc 0 b), X)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (r : ℝ) (hr : r ∈ Set.Icc 0 a) : EulerVolterraConvolution.extendPath (a + b) ⋯ (windowSource C 0 (a + b) ⋯ ⋯ (EulerTimePathGluing.gluePath a b ha hb u v hmatch)) r = EulerVolterraConvolution.extendPath a ha (windowSource C 0 a ⋯ ⋯ u) r

Before the restart, the literal nonlinear source of the pasted solution is the old source.

theorem EulerWindowSource.windowSource_glue_right {X : Type u_1} {Y : Type u_2} [NormedAddCommGroup X] [NormedSpace ℝ X] [NormedAddCommGroup Y] [NormedSpace ℝ Y] {S : ℝ} (C : EulerQuadraticSource.Coefficients (↑(Set.Icc 0 S)) X Y) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (habS : a + b ≤ S) (u : C(↑(Set.Icc 0 a), X)) (v : C(↑(Set.Icc 0 b), X)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (r : ℝ) (hr : r ∈ Set.Icc 0 b) : EulerVolterraConvolution.extendPath (a + b) ⋯ (windowSource C 0 (a + b) ⋯ ⋯ (EulerTimePathGluing.gluePath a b ha hb u v hmatch)) (a + r) = EulerVolterraConvolution.extendPath b hb (windowSource C a b ha habS v) r

After the restart, the literal nonlinear source of the pasted solution is the translated new source.

Pasting actual high-order viscous mild solutions preserves the derivative-gaining Duhamel formula.

theorem EulerGainedMildPasting.gluePath_map_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] (A : E →L[ℝ] F) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), E)) (v : C(↑(Set.Icc 0 b), E)) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (t : ↑(Set.Icc 0 (a + b))) : A ((EulerTimePathGluing.gluePath a b ha hb u v hmatch) t) = (EulerTimePathGluing.gluePath a b ha hb ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 a)) A) u) ((ContinuousLinearMap.compLeftContinuous ℝ (↑(Set.Icc 0 b)) A) v) ⋯) t

Applying an actual bounded spatial map commutes with matching-endpoint time pasting.

theorem EulerGainedMildPasting.glue_gained_mild (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (u : C(↑(Set.Icc 0 a), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (v : C(↑(Set.Icc 0 b), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (f : C(↑(Set.Icc 0 (a + b)), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (f1 : C(↑(Set.Icc 0 a), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (f2 : C(↑(Set.Icc 0 b), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hF1 : ∀ r ∈ Set.Icc 0 a, EulerVolterraConvolution.extendPath (a + b) ⋯ f r = EulerVolterraConvolution.extendPath a ha f1 r) (hF2 : ∀ r ∈ Set.Icc 0 b, EulerVolterraConvolution.extendPath (a + b) ⋯ f (a + r) = EulerVolterraConvolution.extendPath b hb f2 r) (hsolu : ∀ (t : ↑(Set.Icc 0 a)), u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath a ha f1 (↑t - r))) (hsolv : ∀ (t : ↑(Set.Icc 0 b)), v t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) (u ⟨a, ⋯⟩) + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath b hb f2 (↑t - r))) (t : ↑(Set.Icc 0 (a + b))) : (EulerTimePathGluing.gluePath a b ha hb u v hmatch) t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath (a + b) ⋯ f (↑t - r))

Matching actual solutions on adjacent intervals give a genuine gained-derivative mild solution on the union.

theorem EulerQuadraticMildPasting.quadratic_mild_window_iff (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) {S T : ℝ} (hT : 0 ≤ T) (hTS : T ≤ S) (C : EulerQuadraticSource.Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : (∀ (t : ↑(Set.Icc 0 T)), u t = EulerQuadraticSource.quadraticDuhamel period ν hν hT hTS C u₀ u t) ↔ ∀ (t : ↑(Set.Icc 0 T)), u t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT (EulerWindowSource.windowSource C 0 T ⋯ ⋯ u) (↑t - r))

The local solver's actual quadratic Duhamel formula is exactly the literal zero-offset nonlinear source formula.

theorem EulerQuadraticMildPasting.glue_quadratic_mild (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) {S : ℝ} (C : EulerQuadraticSource.Coefficients ↑(Set.Icc 0 S) ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)) ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (a b : ℝ) (ha : 0 ≤ a) (hb : 0 ≤ b) (haS : a ≤ S) (habS : a + b ≤ S) (u : C(↑(Set.Icc 0 a), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (v : C(↑(Set.Icc 0 b), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) (hmatch : u ⟨a, ⋯⟩ = v ⟨0, ⋯⟩) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (hsolu : ∀ (t : ↑(Set.Icc 0 a)), u t = EulerQuadraticSource.quadraticDuhamel period ν hν ha haS C u₀ u t) (hsolv : ∀ (t : ↑(Set.Icc 0 b)), v t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) (u ⟨a, ⋯⟩) + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (C.apply ((EulerUniformHeatLocal.timeWindow a b ha habS) (Set.projIcc 0 b hb (↑t - r))) (v (Set.projIcc 0 b hb (↑t - r))))) (t : ↑(Set.Icc 0 (a + b))) : (EulerTimePathGluing.gluePath a b ha hb u v hmatch) t = EulerQuadraticSource.quadraticDuhamel period ν hν ⋯ habS C u₀ (EulerTimePathGluing.gluePath a b ha hb u v hmatch) t

The actual projected quadratic mild equation is preserved when a genuine local restart is appended.