Exact pasting of genuine heat-Duhamel solutions on adjacent time intervals.
Exact restart identities for the genuine cylinder heat and Bochner Duhamel integrals.
theorem
EulerHeatRestart.heatFlow_semigroup
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(s t : ℝ)
(hs : 0 ≤ s)
(ht : 0 ≤ t)
(u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
:
(EulerSobolevHeatGenerator.heatFlow period q ν s) ((EulerSobolevHeatGenerator.heatFlow period q ν t) u) = (EulerSobolevHeatGenerator.heatFlow period q ν (s + t)) u
Actual viscous heat obeys the semigroup law at nonnegative physical times.
theorem
EulerHeatRestart.heatFlow_duhamel_history
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(a t : ℝ)
(ha : 0 ≤ a)
(hat : a ≤ t)
:
(EulerSobolevHeatGenerator.heatFlow period q ν (t - a)) (EulerDuhamelDifferentiation.duhamel period ν T hT f a) = ∫ (s : ℝ) in 0..a, (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)
Heat propagates the earlier Duhamel history exactly to a later time.
theorem
EulerHeatRestart.duhamel_restart
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(a t : ℝ)
(ha : 0 ≤ a)
(hat : a ≤ t)
:
EulerDuhamelDifferentiation.duhamel period ν T hT f t = (EulerSobolevHeatGenerator.heatFlow period q ν (t - a)) (EulerDuhamelDifferentiation.duhamel period ν T hT f a) + ∫ (s : ℝ) in a..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)
The actual Bochner Duhamel integral splits into propagated history and forcing after the restart time.
theorem
EulerHeatRestart.inhomogeneous_heat_restart
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(a t : ℝ)
(ha : 0 ≤ a)
(hat : a ≤ t)
:
(EulerSobolevHeatGenerator.heatFlow period q ν t) u₀ + EulerDuhamelDifferentiation.duhamel period ν T hT f t = (EulerSobolevHeatGenerator.heatFlow period q ν (t - a))
((EulerSobolevHeatGenerator.heatFlow period q ν a) u₀ + EulerDuhamelDifferentiation.duhamel period ν T hT f a) + ∫ (s : ℝ) in a..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)
The full genuine inhomogeneous heat solution restarts from its attained state.
theorem
EulerHeatRestart.duhamel_restart_shifted
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(a t : ℝ)
(ha : 0 ≤ a)
(ht : 0 ≤ t)
:
EulerDuhamelDifferentiation.duhamel period ν T hT f (a + t) = (EulerSobolevHeatGenerator.heatFlow period q ν t) (EulerDuhamelDifferentiation.duhamel period ν T hT f a) + ∫ (r : ℝ) in 0..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - r)) (EulerVolterraConvolution.extendPath T hT f (a + r))
The old-history and new-source identity written in elapsed time after the restart.
theorem
EulerDuhamelPasting.duhamel_congr_initial
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν T1 T2 : ℝ)
(hT1 : 0 ≤ T1)
(hT2 : 0 ≤ T2)
(f1 : C(↑(Set.Icc 0 T1), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(f2 : C(↑(Set.Icc 0 T2), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : 0 ≤ t)
(hf :
∀ r ∈ Set.Icc 0 t, EulerVolterraConvolution.extendPath T1 hT1 f1 r = EulerVolterraConvolution.extendPath T2 hT2 f2 r)
:
EulerDuhamelDifferentiation.duhamel period ν T1 hT1 f1 t = EulerDuhamelDifferentiation.duhamel period ν T2 hT2 f2 t
Actual Duhamel integrals agree whenever their source fields agree on the integration interval.
theorem
EulerDuhamelPasting.inhomogeneous_restart_shifted
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν : ℝ)
(hν : 0 ≤ ν)
(T : ℝ)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period q))
(a t : ℝ)
(ha : 0 ≤ a)
(ht : 0 ≤ t)
:
(EulerSobolevHeatGenerator.heatFlow period q ν (a + t)) u₀ + EulerDuhamelDifferentiation.duhamel period ν T hT f (a + t) = (EulerSobolevHeatGenerator.heatFlow period q ν t)
((EulerSobolevHeatGenerator.heatFlow period q ν a) u₀ + EulerDuhamelDifferentiation.duhamel period ν T hT f a) + ∫ (r : ℝ) in 0..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - r)) (EulerVolterraConvolution.extendPath T hT f (a + r))
The exact inhomogeneous heat restart identity in elapsed time.
theorem
EulerDuhamelPasting.shifted_source_integral
(period : ℝ)
[Fact (0 < period)]
{q : ℕ}
(ν a b T : ℝ)
(hb : 0 ≤ b)
(hT : 0 ≤ T)
(f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(g : C(↑(Set.Icc 0 b), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(t : ℝ)
(ht : t ∈ Set.Icc 0 b)
(hfg :
∀ r ∈ Set.Icc 0 b, EulerVolterraConvolution.extendPath T hT f (a + r) = EulerVolterraConvolution.extendPath b hb g r)
:
∫ (r : ℝ) in 0..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - r)) (EulerVolterraConvolution.extendPath T hT f (a + r)) = EulerDuhamelDifferentiation.duhamel period ν b hb g t
The elapsed-time part of a genuine Duhamel integral is the restarted source integral.
theorem
EulerDuhamelPasting.glue_ordinary_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)))
(v : C(↑(Set.Icc 0 b), ↥(EulerCylinderSobolevSpace.SobolevSpace period q)))
(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))
(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 = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) u₀ + EulerDuhamelDifferentiation.duhamel period ν a ha f1 ↑t)
(hsolv :
∀ (t : ↑(Set.Icc 0 b)),
v t = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) (u ⟨a, ⋯⟩) + EulerDuhamelDifferentiation.duhamel period ν b hb f2 ↑t)
(t : ↑(Set.Icc 0 (a + b)))
:
(EulerTimePathGluing.gluePath a b ha hb u v hmatch) t = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) u₀ + EulerDuhamelDifferentiation.duhamel period ν (a + b) ⋯ f ↑t
The literal pasting of two actual mild solutions solves the complete Duhamel equation on their union.