Parabolic Hölder continuity of the Duhamel potential

For jointly measurable forcing with uniformly bounded, spatially Hölder slices, the Duhamel heat potential is Hölder on each closed parabolic slab, including the initial slice. No time regularity of the forcing is required. This supplies the value-field estimate for constructing the bounded classical solution operator of the inhomogeneous heat equation.

The estimate separates the common integration interval, where the Cauchy potential's parabolic Hölder estimate TauCeti.holderWith_heatCauchyPotential applies, from the remaining interval, whose length bounds its contribution. For 0 < α < 1, the spatial Hessian also satisfies a joint parabolic Hölder estimate, obtained from its separate spatial and temporal estimates.

References

• A. Friedman, Partial Differential Equations of Parabolic Type, Chapter 1, Section 3.
• A. Lunardi, Linear and nonlinear diffusion problems, Cortona lecture notes, 2004, Chapter 4.

theorem TauCeti.intervalIntegrable_heatDuhamelPotential_integrand {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → E → F} {T M : ℝ} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) (hM : ∀ r ∈ Set.Icc 0 T, ∀ (y : E), ‖f r y‖ ≤ M) {s : ℝ} (hs : s ∈ Set.Icc 0 T) (t : ℝ) (x : E) : IntervalIntegrable (fun (r : ℝ) => heatCauchyPotential (f r) (t - r) x) MeasureTheory.volume 0 s

The Cauchy-potential integrand of the Duhamel potential is integrable on [0, s] for every s ∈ [0, T], even when its elapsed-time argument is nonpositive.

theorem TauCeti.heatDuhamelPotential_eq_integral_heatCauchyPotential {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → E → F} {t : ℝ} (ht : 0 ≤ t) (x : E) : heatDuhamelPotential f t x = ∫ (r : ℝ) in 0..t, heatCauchyPotential (f r) (t - r) x

On nonnegative time slices the Duhamel potential can be integrated using the Cauchy potential, whose extension to nonpositive elapsed times does not affect the integral.

theorem TauCeti.holderWith_heatDuhamelPotential {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {f : ℝ → E → F} {H α : NNReal} (hf : MeasureTheory.StronglyMeasurable (Function.uncurry f)) {T M : NNReal} (hM : ∀ r ∈ Set.Icc 0 ↑T, ∀ (y : E), ‖f r y‖ ≤ ↑M) (hH : ∀ r ∈ Set.Icc 0 ↑T, HolderWith H α (f r)) (hα : 0 < α) (hα₂ : α ≤ 2) : HolderWith (T * H * (1 + heatKernelMoment E α) + M * max 1 T) α fun (p : ↑(ParabolicSpaceTime.slab 0 ↑T)) => heatDuhamelPotential f (↑p).time (↑p).space

The value-field parabolic Hölder estimate for the Duhamel potential. If the forcing is jointly measurable and its spatial slices on [0,T] are bounded by M and α-Hölder with constant H, where 0 < α ≤ 2, then its Duhamel potential is parabolically α-Hölder on the closed slab, with constant T H (1 + M_α) + M max(1,T). Here M_α is the heat-kernel moment. No temporal continuity of the forcing is assumed.

theorem TauCeti.exists_holderWith_iteratedFDeriv_two_heatDuhamelPotential_slab {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {α : NNReal} [CompleteSpace F] (hα : 0 < α) (hα₁ : α < 1) : ∃ (C : NNReal), ∀ {f : ℝ → E → F} {M T : ℝ} {H : NNReal}, MeasureTheory.StronglyMeasurable (Function.uncurry f) → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), ∀ᵐ (y : E), ‖f s y‖ ≤ M) → (∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioo 0 T), HolderWith H α (f s)) → HolderWith (C * H) α fun (p : ↑(ParabolicSpaceTime.slab 0 T)) => iteratedFDeriv ℝ 2 (heatDuhamelPotential f (↑p).time) (↑p).space

The Hessian of the Duhamel potential is jointly parabolically α-Hölder on the closed slab, for 0 < α < 1. The constant is independent of the horizon and the bound on the forcing; only its uniform spatial Hölder constant enters. No temporal regularity is required.