The heat semigroup on bounded uniformly continuous functions

Convolution with the heat kernel defines a strongly continuous contraction semigroup on the closed subspace BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F of bounded uniformly continuous functions. Its time-zero value is the identity. This is the supremum-norm setting for the heat Cauchy problem with uniformly continuous initial data, rather than the Lᵖ setting.

heatSemigroupBUC bundles the heat regularizations heatCauchyPotentialBUC in the semigroup interface. The semigroup law follows from convolution associativity and the heat-kernel identity; strong continuity follows from uniform attainment of the initial trace. The general semigroup API then gives continuity of the orbit at every time, generators and Laplace resolvents.

References

• K.-J. Engel and R. Nagel, One-Parameter Semigroups for Linear Evolution Equations, Chapter II, 2.12 (diffusion on bounded uniformly continuous functions).

noncomputable def TauCeti.heatSemigroupBUC {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] : Semigroups.ContractionSemigroup ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)

The heat semigroup on bounded uniformly continuous functions, with the supremum norm. At positive times it is convolution with the heat kernel, and at zero it is the identity.

@[simp]

theorem TauCeti.heatSemigroupBUC_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : NNReal) : heatSemigroupBUC t = heatCauchyPotentialBUC ↑t

The nonnegative-time semigroup operator is the existing bounded heat regularization.

@[simp]

theorem TauCeti.heatSemigroupBUC_realOperator {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] (t : ℝ) : heatSemigroupBUC.realOperator t = heatCauchyPotentialBUC t

The real-time extension of the semigroup agrees with heat regularization, also at negative times, where both act as the identity.

theorem TauCeti.coe_heatSemigroupBUC_of_pos {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {t : NNReal} (ht : 0 < t) (g : ↥(BoundedContinuousFunction.uniformContinuousSubmodule ℝ E F)) : ⇑↑((heatSemigroupBUC t) g) = MeasureTheory.convolution (heatKernel ↑t) (⇑↑g) (ContinuousLinearMap.lsmul ℝ ℝ) MeasureTheory.volume

At positive time the semigroup is pointwise convolution with the heat kernel.