Heat regularization of bounded continuous data

TauCeti.heatCauchyPotentialBCF bundles the Cauchy heat potential as a contraction on bounded continuous functions. At positive times its spatial derivatives of every order are bounded, and it is Lipschitz even when the initial datum is only bounded and continuous. For complete targets it acts as the identity at nonpositive times.

The analytic inputs are the Cauchy potential estimates and the derivative bounds for heat convolutions in TauCeti.Analysis.PDE.HeatKernel.HeatEquation.

References

• A. Lunardi, Linear and nonlinear diffusion problems, Cortona lecture notes (2004), Chapter 4.
• 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.heatCauchyPotentialBCF {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) : BoundedContinuousFunction E F →L[ℝ] BoundedContinuousFunction E F

The Cauchy heat potential as a bounded operator on bounded continuous functions. For complete targets, negative times, like time zero, act as the identity.

@[simp]

theorem TauCeti.heatCauchyPotentialBCF_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) (g : BoundedContinuousFunction E F) (x : E) : ((heatCauchyPotentialBCF t) g) x = heatCauchyPotential (⇑g) t x

Pointwise evaluation of the bounded heat regularization.

theorem TauCeti.norm_heatCauchyPotentialBCF_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] (t : ℝ) : ‖heatCauchyPotentialBCF t‖ ≤ 1

Heat regularization does not increase the supremum norm.

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

At positive times the bounded heat regularization is convolution with the heat kernel.

theorem TauCeti.norm_iteratedFDeriv_heatCauchyPotentialBCF_le {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {t : ℝ} (ht : 0 < t) (g : BoundedContinuousFunction E F) (m : ℕ) (x : E) : ‖iteratedFDeriv ℝ m (⇑((heatCauchyPotentialBCF t) g)) x‖ ≤ (∫ (z : E), ‖iteratedFDeriv ℝ m (heatKernel t) z‖) * ‖g‖

A positive-time heat regularization has bounded spatial derivatives of every order.

theorem TauCeti.lipschitzWith_heatCauchyPotentialBCF {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {t : ℝ} (ht : 0 < t) (g : BoundedContinuousFunction E F) : LipschitzWith ⟨(∫ (z : E), ‖iteratedFDeriv ℝ 1 (heatKernel t) z‖) * ‖g‖, ⋯⟩ ⇑((heatCauchyPotentialBCF t) g)

Heat regularization at positive time is Lipschitz, even for merely bounded continuous data. The explicit constant is the L¹ norm of the kernel's first derivative times the data norm.

@[simp]

theorem TauCeti.heatCauchyPotentialBCF_of_nonpos {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 : ℝ} (ht : t ≤ 0) : heatCauchyPotentialBCF t = ContinuousLinearMap.id ℝ (BoundedContinuousFunction E F)

At nonpositive times the bounded heat regularization is the identity.

theorem TauCeti.heatCauchyPotentialBCF_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] [CompleteSpace F] {s t : ℝ} (hs : 0 ≤ s) (ht : 0 ≤ t) : heatCauchyPotentialBCF (s + t) = heatCauchyPotentialBCF s ∘SL heatCauchyPotentialBCF t

The heat operators on bounded continuous functions satisfy the semigroup law at nonnegative times. Strong continuity at zero requires uniformly continuous data.