The heat convolution solves the heat equation #
Let g be a measurable, essentially bounded function on a finite-dimensional real inner product
space E, with values in a real normed space (a Banach space for the Laplacian, the heat
equation and the Hölder bounds). The candidate solution of the Cauchy problem ∂ₜu = Δu,
u(0, ·) = g, is
u(t, x) = (K_t ⋆ g)(x), where K_t is the heat kernel. The initial condition holds pointwise
at every point x₀ where g is continuous (for F a Banach space): u(t, x) → g(x₀) as
(t, x) → (0⁺, x₀), which is TauCeti.tendsto_heatKernel_convolution. At points where g is
discontinuous no such limit is asserted. This file proves the equation:
u(t, ·)is smooth for everyt > 0, however roughgis, and its derivatives areD^m u(t, ·) = D^m K_t ⋆ g, bounded by‖D^m K_t‖_{L¹}times the bound ofg; form ≥ 1, since∫ D^m K_t = 0, anα-Hölder datum gives the sharper boundH ∫ ‖D^m K_t(z)‖ ‖z‖^α dz, and similarly the difference of these derivatives at two timesa, bis at mostH ∫ ‖D^m K_b(z) - D^m K_a(z)‖ ‖z‖^α dz;Δu(t, ·) = ΔK_t ⋆ g, and∂ₜu(t, x) = (ΔK_t ⋆ g)(x), so∂ₜu = Δufort > 0.
Both derivatives are taken under the integral sign. In space, every derivative of K_t is
dominated, uniformly on unit translates, by a multiple of K_{4t}
(TauCeti.exists_integrable_norm_iteratedFDeriv_heatKernel_add_le), and this feeds the general
smoothness theorem MeasureTheory.contDiff_convolution_left_of_dominated. In time,
∂ₜK_s = ΔK_s is dominated for s near t by a multiple of K_{4t}.
Main declarations #
TauCeti.contDiff_heatKernel_convolution:K_t ⋆ gis smooth fort > 0.TauCeti.iteratedFDeriv_heatKernel_convolution,TauCeti.iteratedFDeriv_heatKernel_convolution_eq_integral_sub:D^m (K_t ⋆ g) = D^m K_t ⋆ g, with the value at the base point subtracted form ≥ 1.TauCeti.iteratedFDeriv_heatKernel_convolution_eq_smul_integral: the parabolic scalingD^m (K_t ⋆ g)(x) = (√t)⁻¹ ^ m ∫ D^m K_1(y) ⊗ g(x - √t • y) dy.TauCeti.norm_iteratedFDeriv_heatKernel_convolution_le,TauCeti.norm_iteratedFDeriv_heatKernel_convolution_le_of_holderWith: bounds on these derivatives for bounded and for Hölder data.TauCeti.exists_norm_laplacian_heatKernel_convolution_le: the bound‖Δ (K_t ⋆ g)(x)‖ ≤ C H t^((α - 2)/2)for boundedα-Hölder data.TauCeti.norm_iteratedFDeriv_heatKernel_convolution_sub_le_of_holderWith: the corresponding bound on their differences between two times, for Hölder data.TauCeti.laplacian_heatKernel_convolution:Δ (K_t ⋆ g) = ΔK_t ⋆ g.TauCeti.hasDerivAt_heatKernel_convolution: the heat equation∂ₜ (K_t ⋆ g)(x) = Δ (K_t ⋆ g)(x)fort > 0.TauCeti.hasDerivAt_heatKernel_convolution_of_hasCompactSupport: the heat equation in the form∂ₜ (K_t ⋆ φ) = K_t ⋆ Δ φforC²dataφwith compact support.TauCeti.heatKernel_convolution_sub_eq_integral: Duhamel's formula(K_t ⋆ φ)(x) - φ(x) = ∫₀ᵗ (K_s ⋆ Δ φ)(x) dsfor suchφ.TauCeti.stronglyMeasurable_heatKernel_convolution:(t, x) ↦ (K_t ⋆ g)(x)is strongly measurable for continuousg.
References #
- L. C. Evans, Partial Differential Equations, Section 2.3.1, Theorem 1.
Smoothing by the heat kernel. For t > 0 and g measurable and essentially bounded,
K_t ⋆ g is smooth.
Derivatives of a heat convolution. For t > 0 and g measurable and essentially
bounded, every derivative of K_t ⋆ g is computed on the kernel:
D^m (K_t ⋆ g)(x) = ∫ D^m K_t(z) ⊗ g(x - z) dz, where A ⊗ b is the multilinear map
v ↦ A v • b.
Bounds on the derivatives of a heat convolution. If ‖g‖ ≤ M almost everywhere, then
‖D^m (K_t ⋆ g)(x)‖ ≤ ‖D^m K_t‖_{L¹} M for t > 0.
Parabolic scaling of the derivatives of a heat convolution. For t > 0 and g measurable
and essentially bounded,
D^m (K_t ⋆ g)(x) = (√t)⁻¹ ^ m ∫ D^m K_1(y) ⊗ g(x - √t • y) dy, where A ⊗ b is the
multilinear map v ↦ A v • b.
Cancellation in the derivatives of a heat convolution. Since ∫ D^m K_t = 0 for m ≥ 1,
the value of g at the base point can be subtracted under the integral:
D^m (K_t ⋆ g)(x) = ∫ D^m K_t(z) ⊗ (g(x - z) - g(x)) dz.
Hölder bounds on the derivatives of a heat convolution. If g is bounded and α-Hölder
with constant H, then for m ≥ 1 and t > 0,
‖D^m (K_t ⋆ g)(x)‖ ≤ H ∫ ‖D^m K_t(z)‖ ‖z‖^α dz. By
TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_mul_rpow_le the right side is
O(H t^((α - m) / 2)), which for m = 2 is integrable in time near t = 0 when α > 0.
Hölder bound on the Laplacian of a heat convolution. The Laplacian of the heat convolution
of a bounded α-Hölder function with constant H is O(H τ^((α - 2)/2)), uniformly in the
function.
Time differences of the derivatives of a heat convolution. If g is bounded and
α-Hölder with constant H, then for m ≥ 1 and times a, b > 0,
‖D^m (K_b ⋆ g)(x) - D^m (K_a ⋆ g)(x)‖ ≤ H ∫ ‖D^m K_b(z) - D^m K_a(z)‖ ‖z‖^α dz. By
TauCeti.exists_integral_norm_iteratedFDeriv_heatKernel_sub_mul_rpow_le the right side is
O(H (b - a) a^((α - m - 2) / 2)) when a ≤ b ≤ 2a.
The Laplacian of a heat convolution. For t > 0 and g measurable and essentially
bounded, Δ (K_t ⋆ g) = ΔK_t ⋆ g.
The heat equation. For t > 0 and g measurable and essentially bounded, the function
u(s, x) = (K_s ⋆ g)(x) satisfies ∂ₜu(t, x) = Δu(t, x).
The heat equation for C² data with compact support. For t > 0, the function
s ↦ (K_s ⋆ φ)(x) has derivative (K_t ⋆ Δ φ)(x) at t: the Laplacian of the solution is the
heat convolution of the Laplacian of the datum.
Duhamel's formula for the heat equation. For φ of class C² with compact support and
t > 0, (K_t ⋆ φ)(x) - φ(x) = ∫₀ᵗ (K_s ⋆ Δ φ)(x) ds at every point x.
The heat convolution of a continuous function is jointly strongly measurable in time and space.