Equivalence between genuine gained-derivative and ordinary heat-Duhamel solution formulas.

theorem EulerGainedMildFormula.truncate_injective (period : ℝ) [Fact (0 < period)] (q : ℕ) : Function.Injective ⇑(EulerCylinderSobolevSpace.truncateOperator period q)

Forgetting a top derivative is injective on the actual compatible Sobolev arrays.

noncomputable def EulerGainedMildFormula.mildPath (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))

The genuine heat-plus-gained-Duhamel construction as an actual continuous Sobolev path.

Equations

• One or more equations did not get rendered due to their size.

theorem EulerGainedMildFormula.mildPath_apply (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) : (mildPath period q ν hν T hT u₀ f) t = (EulerSobolevHeat.heatOperator period (q + 1) (2 * ν * ↑t).toNNReal) u₀ + ∫ (r : ℝ) in 0..↑t, (EulerSobolevHeat.heatKernel period q ν hν r) (EulerVolterraConvolution.extendPath T hT f (↑t - r))

The actual gained mild path has the original singular-kernel integral formula.

theorem EulerGainedMildFormula.mildPath_truncate (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ↑(Set.Icc 0 T)) : (EulerCylinderSobolevSpace.truncateOperator period q) ((mildPath period q ν hν T hT u₀ f) t) = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) ((EulerCylinderSobolevSpace.truncateOperator period q) u₀) + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t

The lower Sobolev restriction of the genuine gained path is precisely ordinary Duhamel evolution.

theorem EulerGainedMildFormula.gained_mild_iff (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (u₀ : ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1))) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (u : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period (q + 1)))) : (∀ (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 f (↑t - r))) ↔ ∀ (t : ↑(Set.Icc 0 T)), (EulerCylinderSobolevSpace.truncateOperator period q) (u t) = (EulerSobolevHeatGenerator.heatFlow period q ν ↑t) ((EulerCylinderSobolevSpace.truncateOperator period q) u₀) + EulerDuhamelDifferentiation.duhamel period ν T hT f ↑t

The actual complete high-order path satisfies the singular mild formula exactly when its restriction satisfies ordinary Duhamel.