Differentiation of the actual heat Duhamel integral in L² from finite Sobolev forcing.

theorem EulerDuhamelDifferentiation.heatFlow_joint_continuous (period : ℝ) [Fact (0 < period)] (q : ℕ) (ν : ℝ) : Continuous fun (p : ℝ × ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) => (EulerSobolevHeatGenerator.heatFlow period q ν p.1) p.2

The actual Sobolev heat flow is jointly continuous in real time and its initial field.

theorem EulerDuhamelDifferentiation.heatFlow_nonpositive (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) (t : ℝ) (ht : t ≤ 0) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) : (EulerSobolevHeatGenerator.heatFlow period q ν t) u = u

The chosen real-time extension is exactly the identity at nonpositive times.

theorem EulerDuhamelDifferentiation.heatFlow_value_hasDerivAt_negative (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν : ℝ) (hν : 0 < ν) (u : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)) (t : ℝ) (ht : t < 0) : HasDerivAt (fun (s : ℝ) => EulerCylinderSobolevSpace.value period ((EulerSobolevHeatGenerator.heatFlow period q ν s) u)) 0 t

At negative times the actual clamped heat orbit has zero L² derivative.

theorem EulerDuhamelDifferentiation.shiftedHeat_continuous (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : Continuous fun (s : ℝ) => (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)

The full fixed-interval heat integrand is continuous, with the source path extended by clamping.

noncomputable def EulerDuhamelDifferentiation.duhamel (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

The ordinary, actual Sobolev heat Duhamel integral.

Equations

• EulerDuhamelDifferentiation.duhamel period ν T hT f t = ∫ (s : ℝ) in 0..t, (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)

noncomputable def EulerDuhamelDifferentiation.fullDuhamel (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : ↥(EulerCylinderSobolevSpace.SobolevSpace period q)

A fixed-interval heat integral whose L² derivative can be taken under the integral sign.

Equations

• EulerDuhamelDifferentiation.fullDuhamel period ν T hT f t = ∫ (s : ℝ) in 0..T, (EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s)

theorem EulerDuhamelDifferentiation.fullDuhamel_value (period : ℝ) [Fact (0 < period)] {q : ℕ} (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : EulerCylinderSobolevSpace.value period (fullDuhamel period ν T hT f t) = ∫ (s : ℝ) in Set.Ioc 0 T, EulerCylinderSobolevSpace.value period ((EulerSobolevHeatGenerator.heatFlow period q ν (t - s)) (EulerVolterraConvolution.extendPath T hT f s))

The underlying L² full integral is the genuine Bochner integral of the underlying heat fields.

noncomputable def EulerDuhamelDifferentiation.derivativeIntegrand (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t s : ℝ) : ↥(EulerLiftedGradientSpace.LiftL2 period)

The actual parameter derivative of the full heat integrand away from its measure-zero diagonal.

Equations

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

theorem EulerDuhamelDifferentiation.derivativeIntegrand_measurable (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : MeasureTheory.AEStronglyMeasurable (derivativeIntegrand period hq ν T hT f t) (MeasureTheory.volume.restrict (Set.Ioc 0 T))

The actual parameter derivative is measurable despite its jump across the time diagonal.

theorem EulerDuhamelDifferentiation.shiftedHeat_value_lipschitz (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (r : ℝ) : LipschitzWith (Real.nnabs (4 * ν * ‖f‖)) fun (t : ℝ) => EulerCylinderSobolevSpace.value period ((EulerSobolevHeatGenerator.heatFlow period q ν (t - r)) (EulerVolterraConvolution.extendPath T hT f r))

The full integrand is uniformly Lipschitz in time in L², using two genuine source derivatives.

theorem EulerDuhamelDifferentiation.shiftedHeat_value_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t s : ℝ) (hst : s ≠ t) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period ((EulerSobolevHeatGenerator.heatFlow period q ν (r - s)) (EulerVolterraConvolution.extendPath T hT f s))) (derivativeIntegrand period hq ν T hT f t s) t

The actual off-diagonal parameter derivative is the positive-time heat Laplacian and zero before the source time.

theorem EulerDuhamelDifferentiation.fullDuhamel_value_hasDerivAt (period : ℝ) [Fact (0 < period)] {q : ℕ} (hq : 2 ≤ q) (ν : ℝ) (hν : 0 < ν) (T : ℝ) (hT : 0 ≤ T) (f : C(↑(Set.Icc 0 T), ↥(EulerCylinderSobolevSpace.SobolevSpace period q))) (t : ℝ) : HasDerivAt (fun (r : ℝ) => EulerCylinderSobolevSpace.value period (fullDuhamel period ν T hT f r)) (∫ (s : ℝ) in Set.Ioc 0 T, derivativeIntegrand period hq ν T hT f t s) t

Differentiation under the actual Bochner integral gives the L² derivative of the fixed-interval heat convolution.