The initial time derivative of the Duhamel heat potential

For bounded measurable forcing that is uniformly α-Hölder in space and approaches its initial slice at rate t^(α/2), the Duhamel potential satisfies

‖w(t, x) - t • f(0, x)‖ ≤ (H M_α + L) t^(1 + α/2).

Here H is the spatial Hölder constant, L controls the approach to the initial slice, and M_α is the moment TauCeti.heatKernelMoment. In particular, w(t, ·) / t converges uniformly to f(0, ·), and the right time derivative at zero is f(0, x). Only almost-everywhere bounds on positive-time slices are needed. These endpoint identities are needed when extending the inhomogeneous heat equation to a closed time slab; the interior time derivative is a separate statement.

The estimate combines the spatial approximate-identity bound for the Cauchy potential with the temporal modulus of the forcing, before integrating in time.

References

• A. Friedman, Partial Differential Equations of Parabolic Type, Chapter 1, Section 3 (the volume potential).
• A. Lunardi, Linear and nonlinear diffusion problems, Cortona lecture notes, 2004, Chapter 4 (closed-slab heat potentials).

theorem TauCeti.norm_heatDuhamelPotential_sub_smul_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E → F} {M t : ℝ} {H L α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (hfM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ∀ᵐ (y : E), ‖f s y‖ ≤ M) (hH : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), HolderWith H α (f s)) (hL : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 t), ∀ (x : E), ‖f s x - f 0 x‖ ≤ ↑L * s ^ (↑α / 2)) (hα : 0 < α) (ht : 0 ≤ t) (x : E) : ‖heatDuhamelPotential f t x - t • f 0 x‖ ≤ (↑H * ↑(heatKernelMoment E α) + ↑L) * t ^ (1 + ↑α / 2)

The Duhamel potential has first-order expansion t • f(0, x), uniformly in space, with remainder of order t^(1 + α/2). The forcing need only approach its initial slice at the parabolic Hölder rate; no time derivative of the forcing is assumed.

theorem TauCeti.tendstoUniformly_inv_smul_heatDuhamelPotential {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E → F} {M T : ℝ} {H L α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (hfM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (y : E), ‖f s y‖ ≤ M) (hH : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), HolderWith H α (f s)) (hL : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (x : E), ‖f s x - f 0 x‖ ≤ ↑L * s ^ (↑α / 2)) (hα : 0 < α) (hT : 0 < T) : TendstoUniformly (fun (t : ℝ) (x : E) => t⁻¹ • heatDuhamelPotential f t x) (f 0) (nhdsWithin 0 (Set.Ioi 0))

For bounded forcing uniformly Hölder in space and approaching its initial slice at rate t^(α/2) on a positive time horizon, w(t, ·) / t converges uniformly to f(0, ·).

theorem TauCeti.hasDerivWithinAt_heatDuhamelPotential_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E → F} {M T : ℝ} {H L α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (hfM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (y : E), ‖f s y‖ ≤ M) (hH : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), HolderWith H α (f s)) (hL : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ (x : E), ‖f s x - f 0 x‖ ≤ ↑L * s ^ (↑α / 2)) (hα : 0 < α) (hT : 0 < T) (x : E) : HasDerivWithinAt (fun (t : ℝ) => heatDuhamelPotential f t x) (f 0 x) (Set.Ici 0) 0

At time zero, the right time derivative of the Duhamel potential is the initial forcing. Together with its zero initial value this gives the initial endpoint identity for the inhomogeneous heat equation.

theorem TauCeti.hasDerivWithinAt_heatDuhamelPotential_zero_of_holderOnWith {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {f : ℝ → E → F} {M T : ℝ} {H α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (hfM : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (y : E), ‖f s y‖ ≤ M) (hpar : HolderOnWith H α (fun (p : ParabolicSpaceTime E) => f p.time p.space) (ParabolicSpaceTime.slab 0 T)) (hα : 0 < α) (hT : 0 < T) (x : E) : HasDerivWithinAt (fun (t : ℝ) => heatDuhamelPotential f t x) (f 0 x) (Set.Icc 0 T) 0

Parabolic Hölder forcing on a closed slab gives the initial time derivative f(0, x) of the Duhamel potential within that slab.